(** This file is part of the Coq Numerical Analysis library Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version. This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details. *) (** * Bibliography #<DIV><A NAME="RR9557v1"></A></DIV># [[RR9557v1]] François Clément and Vincent Martin, Finite element method. Detailed proofs to be formalized in Coq, RR-9557, first version, Inria Paris, 2024, #<A HREF="https://inria.hal.science/hal-04713897v1"># https://inria.hal.science/hal-04713897v1#</A>#. *) From Requisite Require Import stdlib_wR ssr_wMC. From Coquelicot Require Import Hierarchy. Close Scope R_scope. From Algebra Require Import Algebra_wDep. From FEM Require Import R_compl multi_index poly_Pdk poly_LagP1k. From FEM Require Import poly_LagPd1_ref LagP_node_ref. From FEM Require Import geom_transf_affine poly_LagPd1. Local Open Scope Monoid_scope. Local Open Scope Group_scope. Local Open Scope Ring_scope. Section Nodes_Facts1. Context {d k : nat}. (** #<A HREF="##RR9557v1">#[[RR9557v1]]#</A># Lem 1604, p. 101. *) Definition node_d0 (vtx : 'R^{d.+1,d}) : 'R^d := T_geom vtx node_ref_d0. (** #<A HREF="##RR9557v1">#[[RR9557v1]]#</A># Def 1588, Eq (9.80), p. 97. *) Lemma node_d0_eq : forall vtx, node_d0 vtx = isobarycenter_ms vtx. Proof. intro; unfold node_d0; rewrite node_ref_d0_eqF T_geom_am; [rewrite T_geom_vtxF | apply invertible_plusn1_R]; easy. Qed. (** #<A HREF="##RR9557v1">#[[RR9557v1]]#</A># Lem 1599, p. 100. *) Lemma node_ref_d0_node : node_ref_d0 = node_d0 vtx_ref. Proof. unfold node_d0; extF; rewrite T_geom_ref; easy. Qed. (** #<A HREF="##RR9557v1">#[[RR9557v1]]#</A># Lem 1604, p. 101. *) Definition node (vtx : 'R^{d.+1,d}) (idk : 'I_(pbinom d k).+1) : 'R^d := T_geom vtx (node_ref idk). Lemma nodeF : forall vtx, node vtx = mapF (T_geom vtx) node_ref. Proof. easy. Qed. (** #<A HREF="##RR9557v1">#[[RR9557v1]]#</A># Lem 1599, p. 100. *) Lemma node_ref_node : node_ref = node vtx_ref. Proof. unfold node; extF; rewrite T_geom_ref; easy. Qed. Context {vtx : 'R^{d.+1,d}}. Hypothesis Hvtx : aff_indep_ms vtx. Lemma node_inj : injective (node vtx). Proof. move=>> /(T_geom_inj Hvtx) /node_ref_inj; easy. Qed. (** #<A HREF="##RR9557v1">#[[RR9557v1]]#</A># Lem 1605, Eq (9.95), p. 101. #<BR># a_alpha \in Hface_0 <-> alpha \in CSdk. *) Lemma node_Hface_0 : forall (idk : 'I_((pbinom d k).+1)), (0 < d)%coq_nat -> (0 < k)%coq_nat -> Hface vtx ord0 (node vtx idk) <-> sum (Adk d k idk) = k. Proof. intros; unfold Hface, node; rewrite Im_equiv; [| apply T_geom_inj; easy]. apply node_ref_Hface_ref_0; easy. Qed. (** #<A HREF="##RR9557v1">#[[RR9557v1]]#</A># Lem 1605, Eq (9.96), p. 101. #<BR># For i between 0 and d-1, we have a_alpha \in Hface_{i+1} iff alpha \in ASdki, ie alpha_i = 0. *) Lemma node_Hface_S : forall (idk : 'I_((pbinom d k).+1)) {i : 'I_d.+1} (Hi : i <> ord0), (0 < d)%coq_nat -> (0 < k)%coq_nat -> Hface vtx i (node vtx idk) <-> Adk d k idk (lower_S Hi) = O. Proof. intros; unfold Hface, node; rewrite Im_equiv; [| apply T_geom_inj; easy]. apply node_ref_Hface_ref_S; easy. Qed. End Nodes_Facts1. Section Nodes_Facts2. (** We need a dimension which is structurally nonzero. We take d = d1.+1 with d1 : nat. *) Context {d1 k : nat}. Let d := d1.+1. Variable vtx : 'R^{d.+1,d}. (** #<A HREF="##RR9557v1">#[[RR9557v1]]#</A># Lem 1607, p. 102, case i=0.#<BR># See also Rem 1606. *) Lemma T_geom_Hface_0_node : forall (idk : 'I_(pbinom d1 k).+1), (0 < k)%coq_nat -> T_geom_Hface vtx ord0 (node_ref idk) = node vtx (Adk_inv d k (inj_CSdk idk)). Proof. intros; unfold T_geom_Hface; rewrite comp_correct inj_Hface_ref_0_node_ref//. Qed. (** #<A HREF="##RR9557v1">#[[RR9557v1]]#</A># Lem 1607, p. 102, case i>0.#<BR># See also Rem 1606. *) Lemma T_geom_Hface_S_node : forall {i} (Hi : i <> ord0) (idk : 'I_(pbinom d1 k).+1), (0 < k)%coq_nat -> T_geom_Hface vtx i (node_ref idk) = node vtx (Adk_inv d k (inj_ASdki (lower_S Hi) idk)). Proof. intros; unfold T_geom_Hface; rewrite comp_correct inj_Hface_ref_S_node_ref//. Qed. End Nodes_Facts2. Section Nodes_d1. Context {d : nat}. Lemma node_vtx_d1 : forall vtx, node vtx = castF (eq_sym (pbinomS_1_r d)) vtx. Proof. intro; extF; unfold node; rewrite node_vtx_ref_d1; unfold castF; rewrite T_geom_vtx; easy. Qed. Context {vtx : 'R^{d.+1,d}}. Hypothesis Hvtx : aff_indep_ms vtx. Lemma LagPd1_decomp_node : forall {p}, Pdk d 1 p -> p = lin_comb (mapF p (node vtx)) (castF (eq_sym (pbinomS_1_r d)) (LagPd1 Hvtx)). Proof. intro; rewrite node_vtx_d1 mapF_castF lc_castF; apply LagPd1_decomp_vtx. Qed. End Nodes_d1. Section Sub_vertices_Def. Context {d : nat}. Variable k : nat. Variable vtx : 'R^{d.+1,d}. (** #<A HREF="##RR9557v1">#[[RR9557v1]]#</A># Def 1594, Eq (9.88), p. 98. sub_vtx 0 = \underline{v}_0 = v_0, sub_vtx i = \underline{v}_i = a_{(k-1)e^i}, for i <> 0. *) Definition sub_vtx (i : 'I_d.+1) : 'R^d := T_geom vtx (sub_vtx_ref k i). (* Could be: sub_vtx i := T_geom (sub_vtx_ref k) vtx. *) Lemma sub_vtxF : sub_vtx = mapF (T_geom vtx) (sub_vtx_ref k). Proof. easy. Qed. End Sub_vertices_Def. Section Sub_vertices_Facts0. Context {d k : nat}. Lemma sub_vtx_refF : @sub_vtx_ref d k = sub_vtx k vtx_ref. Proof. rewrite sub_vtxF T_geom_ref; easy. Qed. End Sub_vertices_Facts0. Section Sub_vertices_Facts1. Context {d k : nat}. Hypothesis Hk : (1 < k)%coq_nat. Context {vtx : 'R^{d.+1,d}}. Hypothesis Hvtx : aff_indep_ms vtx. (** #<A HREF="##RR9557v1">#[[RR9557v1]]#</A># Lem 1597, pp. 99-100. *) Lemma sub_vtx_aff_indep : aff_indep_ms (sub_vtx k vtx). Proof. apply (am_aff_indep (T_geom_am _)); [apply T_geom_inj | apply sub_vtx_ref_aff_indep]; easy. Qed. End Sub_vertices_Facts1. Section Sub_nodes_Def. Context {d : nat}. Variable k : nat. Variable vtx : 'R^{d.+1,d}. (** #<A HREF="##RR9557v1">#[[RR9557v1]]#</A># Lem 1604, p. 101. *) Definition sub_node (idk : [0..(pbinom d k.-1).+1)) : 'R^d := T_geom vtx (sub_node_ref idk). Lemma sub_nodeF : sub_node = mapF (T_geom vtx) sub_node_ref. Proof. easy. Qed. Lemma sub_node_node : sub_node = node (sub_vtx k vtx). Proof. rewrite sub_nodeF nodeF sub_vtxF -T_geom_comp mapF_comp. f_equal. Admitted. End Sub_nodes_Def. Section Sub_nodes_Facts1. Context {d k : nat}. Hypothesis Hk : (1 < k)%coq_nat. Variable vtx : 'R^{d.+1,d}. (** #<A HREF="##RR9557v1">#[[RR9557v1]]#</A># Lem 1598, p. 100. *) Lemma sub_node_eq : sub_node k vtx = widenF (pbinomS_monot_pred d k) (node vtx). Proof. extF; unfold sub_node; rewrite sub_node_ref_eq//. Qed. End Sub_nodes_Facts1. Section Sub_nodes_Facts2. Context {d k : nat}. Hypothesis Hd : (0 < d)%coq_nat. Hypothesis Hk : (1 < k)%coq_nat. Context {vtx : 'R^{d.+1,d}}. Hypothesis Hvtx : aff_indep_ms vtx. (** sub_node \notin Hface_0 *) Lemma sub_node_out_Hface_0 : forall (idk : [0..(pbinom d k.-1).+1)), ~ Hface vtx ord0 (sub_node k vtx idk). Proof. intro; rewrite -T_geom_Hface_eq// sub_nodeF mapF_correct Im_equiv; [apply sub_node_ref_out_Hface_ref_0 | apply T_geom_inj]; easy. Qed. End Sub_nodes_Facts2.