Library FEM.geom_transf_affine
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.
[Ern]
Alexandre Ern, Éléments finis, Aide-mémoire, Dunod/L'Usine Nouvelle, 2005,
https://www.dunod.com/sciences-techniques/aide-memoire-elements-finis.
[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,
https://inria.hal.science/hal-04713897v1.
Bibliography
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 geometry multi_index geom_simplex poly_LagPd1_ref.
Local Open Scope Monoid_scope.
Local Open Scope Group_scope.
Local Open Scope Ring_scope.
Local Open Scope ModuleSpace_scope.
Local Open Scope AffineSpace_scope.
Section T_geom_Facts.
Context {d : nat}.
Variable vtx_cur : 'R^{d.+1,d}.
[RR9557v1]
Def 1550, p. 83.
Lemma T_geom_am : aff_map (T_geom : fct_ModuleSpace → fct_ModuleSpace).
Proof.
apply am_lm_0; unfold T_geom.
apply lm_ext with
(fun x ⇒ lin_comb (LagPd1_ref^~ x - LagPd1_ref^~ 0) vtx_cur);
[intros x; rewrite lc_minus_l; easy |].
apply fct_lc_l_lm; intro; apply: am_lm_0_rev; apply LagPd1_ref_am.
Qed.
Proof.
apply am_lm_0; unfold T_geom.
apply lm_ext with
(fun x ⇒ lin_comb (LagPd1_ref^~ x - LagPd1_ref^~ 0) vtx_cur);
[intros x; rewrite lc_minus_l; easy |].
apply fct_lc_l_lm; intro; apply: am_lm_0_rev; apply LagPd1_ref_am.
Qed.
[RR9557v1]
Def 1550, Eq (9.39), p. 83.
Lemma T_geom_transports_vtx : ∀ i, T_geom (vtx_ref i) = vtx_cur i.
Proof.
intros i; unfold T_geom; rewrite (lc_scalF_compat (kronR i) vtx_cur).
apply lc_kron_l_in_r.
f_equal; apply extF; intro; apply LagPd1_ref_kron_vtx.
Qed.
Lemma T_geom_transports_node :
∀ k (ipk : 'I_(pbinom d k).+1),
T_geom (node_ref ipk) = node_cur vtx_cur ipk.
Proof.
intros; unfold T_geom, node_cur;
rewrite lc_ind_l LagPd1_ref_0// LagPd1_ref_liftF_S node_ref_eq; easy.
Qed.
Lemma T_geom_transports_baryc :
∀ L, sum L = 1 → T_geom (lin_comb L vtx_ref) = lin_comb L vtx_cur.
Proof.
intros L HL; rewrite (am_ac_compat T_geom_am HL);
apply lc_ext_r, T_geom_transports_vtx.
Qed.
End T_geom_Facts.
Section T_geom_inv_Facts.
Context {d : nat}.
Context {vtx_cur : 'R^{d.+1,d}}.
Hypothesis Hvtx : affine_independent vtx_cur.
Lemma T_geom_surj : surjective (T_geom vtx_cur).
Proof.
intros x_cur; destruct (affine_independent_generator _ has_dim_Rn Hvtx x_cur)
as [L HL], (LagPd1_ref_surj L) as [x_ref Hx_ref]; [easy |].
∃ x_ref; unfold T_geom; rewrite Hx_ref; easy.
Qed.
Lemma T_geom_inj : injective (T_geom vtx_cur).
Proof.
intros x_ref y_ref H; apply LagPd1_ref_inj; apply fun_ext_rev.
apply affine_independent_lc in H; [..| rewrite !LagPd1_ref_sum]; easy.
Qed.
Lemma T_geom_bij : bijective (T_geom vtx_cur).
Proof. apply bij_equiv; split; [apply T_geom_inj | apply T_geom_surj]. Qed.
Definition T_geom_inv : 'R^d → 'R^d := f_inv T_geom_bij.
Lemma T_geom_inv_can_r : cancel T_geom_inv (T_geom vtx_cur).
Proof. apply f_inv_can_r. Qed.
Lemma T_geom_inv_can_l : cancel (T_geom vtx_cur) T_geom_inv.
Proof. apply f_inv_can_l. Qed.
Lemma T_geom_inv_am: aff_map (T_geom_inv : fct_ModuleSpace → fct_ModuleSpace).
Proof. apply: am_bij_compat; apply T_geom_am. Qed.
Lemma T_geom_inv_transports_vtx :
∀ i, T_geom_inv (vtx_cur i) = vtx_ref i.
Proof.
intro; rewrite -(T_geom_transports_vtx vtx_cur); apply T_geom_inv_can_l.
Qed.
Lemma T_geom_inv_transports_node :
∀ k (ipk : 'I_(pbinom d k).+1),
T_geom_inv (node_cur vtx_cur ipk) = node_ref ipk.
Proof.
intros; rewrite -(T_geom_transports_node vtx_cur); apply T_geom_inv_can_l.
Qed.
Lemma T_geom_inv_transports_baryc :
∀ L, sum L = 1 → T_geom_inv (lin_comb L vtx_cur) = lin_comb L vtx_ref.
Proof.
intros L HL; rewrite (am_ac_compat T_geom_inv_am HL);
apply lc_ext_r, T_geom_inv_transports_vtx.
Qed.
Let K_geom_ref : 'R^d → Prop := convex_envelop vtx_ref.
Let K_geom_cur : 'R^d → Prop := convex_envelop vtx_cur.
Lemma T_geom_K_geom : incl K_geom_ref (preimage (T_geom vtx_cur) K_geom_cur).
Proof.
move=>> [L HL1 HL2]; unfold K_geom_cur, preimage;
rewrite T_geom_transports_baryc; easy.
Qed.
Lemma T_geom_inv_K_geom : incl K_geom_cur (preimage T_geom_inv K_geom_ref).
Proof.
move=>> [L HL1 HL2]; unfold K_geom_cur, preimage;
rewrite T_geom_inv_transports_baryc; easy.
Qed.
Lemma T_geom_surjS : surjS K_geom_ref K_geom_cur (T_geom vtx_cur).
Proof.
intros x_cur Hx_cur; ∃ (T_geom_inv x_cur); split;
[apply T_geom_inv_K_geom; easy | apply T_geom_inv_can_r].
Qed.
Lemma T_geom_inv_ge_0 :
∀ i, incl K_geom_cur (fun x ⇒ (0 ≤ T_geom_inv x i)%R).
Proof.
move⇒ i x_cur /T_geom_inv_K_geom [L HL1 HL2].
rewrite fct_lc_r_eq; apply (lc_ge_0 _ _ HL1).
intros; apply vtx_ref_ge_0.
Qed.
Lemma T_geom_image : image (T_geom vtx_cur) K_geom_ref = K_geom_cur.
Proof.
apply subset_ext_equiv; split; intros x_cur Hx_cur.
destruct Hx_cur as [x_ref Hx_ref]; apply T_geom_K_geom; easy.
rewrite image_eq; ∃ (T_geom_inv x_cur); split;
[apply T_geom_inv_K_geom; easy | apply eq_sym, T_geom_inv_can_r].
Qed.
Lemma T_geom_inv_image : image T_geom_inv (K_geom_cur) = K_geom_ref.
Proof.
apply subset_ext_equiv; split; intros x_ref Hx_ref.
destruct Hx_ref as [x_cur Hx_cur]; apply T_geom_inv_K_geom; easy.
rewrite image_eq; ∃ (T_geom vtx_cur x_ref); split;
[apply T_geom_K_geom; easy | apply eq_sym, T_geom_inv_can_l].
Qed.
Lemma T_geom_bijS_spec :
bijS_spec (convex_envelop vtx_cur) K_geom_ref T_geom_inv (T_geom vtx_cur).
Proof.
repeat split.
intros _ [x_cur H]; apply T_geom_inv_K_geom; easy.
intros _ [x_ref H]; apply T_geom_K_geom; easy.
intros x_cur _; apply T_geom_inv_can_r.
intros x_ref _; apply T_geom_inv_can_l.
Qed.
Lemma T_geom_inv_bijS_spec :
bijS_spec K_geom_ref (convex_envelop vtx_cur) (T_geom vtx_cur) T_geom_inv.
Proof.
repeat split.
intros _ [x_ref H]; apply T_geom_K_geom; easy.
intros _ [x_cur H]; apply T_geom_inv_K_geom; easy.
intros x_ref _; apply T_geom_inv_can_l.
intros x_cur _; apply T_geom_inv_can_r.
Qed.
Lemma T_geom_inv_bijS : bijS (convex_envelop vtx_cur) K_geom_ref T_geom_inv.
Proof. apply (BijS _ T_geom_bijS_spec). Qed.
End T_geom_inv_Facts.
Section T_geom_ref_Facts.
Context {d : nat}.
Let Hvtx_ref := @vtx_ref_affine_independent d.
Proof.
intros i; unfold T_geom; rewrite (lc_scalF_compat (kronR i) vtx_cur).
apply lc_kron_l_in_r.
f_equal; apply extF; intro; apply LagPd1_ref_kron_vtx.
Qed.
Lemma T_geom_transports_node :
∀ k (ipk : 'I_(pbinom d k).+1),
T_geom (node_ref ipk) = node_cur vtx_cur ipk.
Proof.
intros; unfold T_geom, node_cur;
rewrite lc_ind_l LagPd1_ref_0// LagPd1_ref_liftF_S node_ref_eq; easy.
Qed.
Lemma T_geom_transports_baryc :
∀ L, sum L = 1 → T_geom (lin_comb L vtx_ref) = lin_comb L vtx_cur.
Proof.
intros L HL; rewrite (am_ac_compat T_geom_am HL);
apply lc_ext_r, T_geom_transports_vtx.
Qed.
End T_geom_Facts.
Section T_geom_inv_Facts.
Context {d : nat}.
Context {vtx_cur : 'R^{d.+1,d}}.
Hypothesis Hvtx : affine_independent vtx_cur.
Lemma T_geom_surj : surjective (T_geom vtx_cur).
Proof.
intros x_cur; destruct (affine_independent_generator _ has_dim_Rn Hvtx x_cur)
as [L HL], (LagPd1_ref_surj L) as [x_ref Hx_ref]; [easy |].
∃ x_ref; unfold T_geom; rewrite Hx_ref; easy.
Qed.
Lemma T_geom_inj : injective (T_geom vtx_cur).
Proof.
intros x_ref y_ref H; apply LagPd1_ref_inj; apply fun_ext_rev.
apply affine_independent_lc in H; [..| rewrite !LagPd1_ref_sum]; easy.
Qed.
Lemma T_geom_bij : bijective (T_geom vtx_cur).
Proof. apply bij_equiv; split; [apply T_geom_inj | apply T_geom_surj]. Qed.
Definition T_geom_inv : 'R^d → 'R^d := f_inv T_geom_bij.
Lemma T_geom_inv_can_r : cancel T_geom_inv (T_geom vtx_cur).
Proof. apply f_inv_can_r. Qed.
Lemma T_geom_inv_can_l : cancel (T_geom vtx_cur) T_geom_inv.
Proof. apply f_inv_can_l. Qed.
Lemma T_geom_inv_am: aff_map (T_geom_inv : fct_ModuleSpace → fct_ModuleSpace).
Proof. apply: am_bij_compat; apply T_geom_am. Qed.
Lemma T_geom_inv_transports_vtx :
∀ i, T_geom_inv (vtx_cur i) = vtx_ref i.
Proof.
intro; rewrite -(T_geom_transports_vtx vtx_cur); apply T_geom_inv_can_l.
Qed.
Lemma T_geom_inv_transports_node :
∀ k (ipk : 'I_(pbinom d k).+1),
T_geom_inv (node_cur vtx_cur ipk) = node_ref ipk.
Proof.
intros; rewrite -(T_geom_transports_node vtx_cur); apply T_geom_inv_can_l.
Qed.
Lemma T_geom_inv_transports_baryc :
∀ L, sum L = 1 → T_geom_inv (lin_comb L vtx_cur) = lin_comb L vtx_ref.
Proof.
intros L HL; rewrite (am_ac_compat T_geom_inv_am HL);
apply lc_ext_r, T_geom_inv_transports_vtx.
Qed.
Let K_geom_ref : 'R^d → Prop := convex_envelop vtx_ref.
Let K_geom_cur : 'R^d → Prop := convex_envelop vtx_cur.
Lemma T_geom_K_geom : incl K_geom_ref (preimage (T_geom vtx_cur) K_geom_cur).
Proof.
move=>> [L HL1 HL2]; unfold K_geom_cur, preimage;
rewrite T_geom_transports_baryc; easy.
Qed.
Lemma T_geom_inv_K_geom : incl K_geom_cur (preimage T_geom_inv K_geom_ref).
Proof.
move=>> [L HL1 HL2]; unfold K_geom_cur, preimage;
rewrite T_geom_inv_transports_baryc; easy.
Qed.
Lemma T_geom_surjS : surjS K_geom_ref K_geom_cur (T_geom vtx_cur).
Proof.
intros x_cur Hx_cur; ∃ (T_geom_inv x_cur); split;
[apply T_geom_inv_K_geom; easy | apply T_geom_inv_can_r].
Qed.
Lemma T_geom_inv_ge_0 :
∀ i, incl K_geom_cur (fun x ⇒ (0 ≤ T_geom_inv x i)%R).
Proof.
move⇒ i x_cur /T_geom_inv_K_geom [L HL1 HL2].
rewrite fct_lc_r_eq; apply (lc_ge_0 _ _ HL1).
intros; apply vtx_ref_ge_0.
Qed.
Lemma T_geom_image : image (T_geom vtx_cur) K_geom_ref = K_geom_cur.
Proof.
apply subset_ext_equiv; split; intros x_cur Hx_cur.
destruct Hx_cur as [x_ref Hx_ref]; apply T_geom_K_geom; easy.
rewrite image_eq; ∃ (T_geom_inv x_cur); split;
[apply T_geom_inv_K_geom; easy | apply eq_sym, T_geom_inv_can_r].
Qed.
Lemma T_geom_inv_image : image T_geom_inv (K_geom_cur) = K_geom_ref.
Proof.
apply subset_ext_equiv; split; intros x_ref Hx_ref.
destruct Hx_ref as [x_cur Hx_cur]; apply T_geom_inv_K_geom; easy.
rewrite image_eq; ∃ (T_geom vtx_cur x_ref); split;
[apply T_geom_K_geom; easy | apply eq_sym, T_geom_inv_can_l].
Qed.
Lemma T_geom_bijS_spec :
bijS_spec (convex_envelop vtx_cur) K_geom_ref T_geom_inv (T_geom vtx_cur).
Proof.
repeat split.
intros _ [x_cur H]; apply T_geom_inv_K_geom; easy.
intros _ [x_ref H]; apply T_geom_K_geom; easy.
intros x_cur _; apply T_geom_inv_can_r.
intros x_ref _; apply T_geom_inv_can_l.
Qed.
Lemma T_geom_inv_bijS_spec :
bijS_spec K_geom_ref (convex_envelop vtx_cur) (T_geom vtx_cur) T_geom_inv.
Proof.
repeat split.
intros _ [x_ref H]; apply T_geom_K_geom; easy.
intros _ [x_cur H]; apply T_geom_inv_K_geom; easy.
intros x_ref _; apply T_geom_inv_can_l.
intros x_cur _; apply T_geom_inv_can_r.
Qed.
Lemma T_geom_inv_bijS : bijS (convex_envelop vtx_cur) K_geom_ref T_geom_inv.
Proof. apply (BijS _ T_geom_bijS_spec). Qed.
End T_geom_inv_Facts.
Section T_geom_ref_Facts.
Context {d : nat}.
Let Hvtx_ref := @vtx_ref_affine_independent d.
[RR9557v1]
Lem 1549, p. 82.
Lemma T_geom_ref_id : T_geom vtx_ref = (id : 'R^d → 'R^d).
Proof.
apply fun_ext; intros x; destruct (affine_independent_generator
_ has_dim_Rn Hvtx_ref x) as [L [HL ->]].
apply T_geom_transports_baryc; easy.
Qed.
Lemma T_geom_inv_ref_id : T_geom_inv Hvtx_ref = id.
Proof. apply f_inv_is_id, T_geom_ref_id. Qed.
End T_geom_ref_Facts.
Section T_geom_1k_Facts.
Proof.
apply fun_ext; intros x; destruct (affine_independent_generator
_ has_dim_Rn Hvtx_ref x) as [L [HL ->]].
apply T_geom_transports_baryc; easy.
Qed.
Lemma T_geom_inv_ref_id : T_geom_inv Hvtx_ref = id.
Proof. apply f_inv_is_id, T_geom_ref_id. Qed.
End T_geom_ref_Facts.
Section T_geom_1k_Facts.
[RR9557v1]
Lem 1548, p. 82.
See also Def 1461, p. 60.
See also Def 1461, p. 60.
Lemma T_geom_1k :
∀ (vtx_cur : 'R^{2,1}) x_ref,
T_geom vtx_cur x_ref =
(scal (x_ref ord0) (vtx_cur ord1 - vtx_cur ord0) + vtx_cur ord0).
Proof.
intros vtx_cur x_ref; unfold T_geom; rewrite lc_ind_l.
rewrite LagPd1_ref_0// LagPd1_ref_liftF_S sum_1 lc_1 liftF_S_0.
rewrite scal_minus_l scal_one scal_minus_r.
unfold minus; rewrite -plus_assoc plus_comm; f_equal; apply plus_comm.
Qed.
∀ (vtx_cur : 'R^{2,1}) x_ref,
T_geom vtx_cur x_ref =
(scal (x_ref ord0) (vtx_cur ord1 - vtx_cur ord0) + vtx_cur ord0).
Proof.
intros vtx_cur x_ref; unfold T_geom; rewrite lc_ind_l.
rewrite LagPd1_ref_0// LagPd1_ref_liftF_S sum_1 lc_1 liftF_S_0.
rewrite scal_minus_l scal_one scal_minus_r.
unfold minus; rewrite -plus_assoc plus_comm; f_equal; apply plus_comm.
Qed.
[RR9557v1]
Lem 1462, Eq (8.14), p. 60.
Lemma T_geom_inv_1k :
∀ {vtx_cur : 'R^{2,1}} (Hvtx : affine_independent vtx_cur) x_cur,
T_geom_inv Hvtx x_cur =
scal (/ (vtx_cur ord_max ord0 - vtx_cur ord0 ord0))
(x_cur - vtx_cur ord0).
Proof.
intros vtx_cur Hvtx x_cur; apply (T_geom_inj Hvtx);
rewrite T_geom_inv_can_r T_geom_1k.
apply extF; intro; rewrite I_1_is_unit -ord2_1_max.
rewrite fct_plus_eq !fct_scal_r_eq !fct_minus_eq.
rewrite scal_comm_R scal_assoc mult_inv_r.
rewrite scal_one_l// plus_minus_l; easy.
apply invertible_equiv_R, (minus_zero_reg_contra (vtx_cur_1k_neq Hvtx)).
Qed.
End T_geom_1k_Facts.
Section T_node_face_Facts.
Context {d1 k : nat}.
∀ {vtx_cur : 'R^{2,1}} (Hvtx : affine_independent vtx_cur) x_cur,
T_geom_inv Hvtx x_cur =
scal (/ (vtx_cur ord_max ord0 - vtx_cur ord0 ord0))
(x_cur - vtx_cur ord0).
Proof.
intros vtx_cur Hvtx x_cur; apply (T_geom_inj Hvtx);
rewrite T_geom_inv_can_r T_geom_1k.
apply extF; intro; rewrite I_1_is_unit -ord2_1_max.
rewrite fct_plus_eq !fct_scal_r_eq !fct_minus_eq.
rewrite scal_comm_R scal_assoc mult_inv_r.
rewrite scal_one_l// plus_minus_l; easy.
apply invertible_equiv_R, (minus_zero_reg_contra (vtx_cur_1k_neq Hvtx)).
Qed.
End T_geom_1k_Facts.
Section T_node_face_Facts.
Context {d1 k : nat}.
[RR9557v1]
Lem 1500, pp. 70-71.
Function fd{k,0}.
See also Rem 1499, p. 70.
See also Rem 1499, p. 70.
Definition T_node_face_0 (ipk : 'I_(pbinom d1 k).+1) : 'nat^d1.+1 :=
Slice_op (k - sum (Adk d1 k ipk))%coq_nat (Adk d1 k ipk).
Slice_op (k - sum (Adk d1 k ipk))%coq_nat (Adk d1 k ipk).
[RR9557v1]
Lem 1501, pp. 71-72.
Function fd{k,i}.
See also Rem 1499, p. 70.
See also Rem 1499, p. 70.
Definition T_node_face_S
(i : 'I_d1.+1) (ipk : 'I_(pbinom d1 k).+1) : 'nat^d1.+1 :=
insertF (Adk d1 k ipk) O i.
(i : 'I_d1.+1) (ipk : 'I_(pbinom d1 k).+1) : 'nat^d1.+1 :=
insertF (Adk d1 k ipk) O i.
[RR9557v1]
Lem 1500, pp. 70-71.
T_node_face_0 has image in (sum=k).
T_node_face_0 has image in (sum=k).
Lemma T_node_face_0_sum : ∀ ipk, sum (T_node_face_0 ipk) = k.
Proof.
intros; unfold T_node_face_0; apply Slice_op_sum;
[apply Nat.le_sub_l | rewrite nat_sub2_r//; apply Adk_sum].
Qed.
Proof.
intros; unfold T_node_face_0; apply Slice_op_sum;
[apply Nat.le_sub_l | rewrite nat_sub2_r//; apply Adk_sum].
Qed.
[RR9557v1]
Lem 1500, pp. 70-71.
T_node_face_S preserves sum.
T_node_face_S preserves sum.
Lemma T_node_face_S_sum :
∀ i ipk, sum (T_node_face_S i ipk) = sum (Adk d1 k ipk).
Proof. intros; unfold T_node_face_S; rewrite sum_insertF; easy. Qed.
End T_node_face_Facts.
∀ i ipk, sum (T_node_face_S i ipk) = sum (Adk d1 k ipk).
Proof. intros; unfold T_node_face_S; rewrite sum_insertF; easy. Qed.
End T_node_face_Facts.