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.

Bibliography

[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.

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}.

[Ern] Eq (3.23), p. 58.
[RR9557v1] Def 1547, p. 82.
Definition T_geom : 'R^d 'R^d := fun x_ref
  lin_comb (fun iLagPd1_ref i x_ref) vtx_cur.

[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 xlin_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.
movei 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.

[RR9557v1] Lem 1548, p. 82.
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.

[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}.

[RR9557v1] Lem 1500, pp. 70-71. Function fd{k,0}.
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).

[RR9557v1] Lem 1501, pp. 71-72. Function fd{k,i}.
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.

[RR9557v1] Lem 1500, pp. 70-71.
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.

[RR9557v1] Lem 1500, pp. 70-71.
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.