From 62024fa835fbfa10526b140e39cbde44b98abcea Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Sun, 9 Mar 2025 23:56:59 +0100
Subject: [PATCH] Mv stuff around. Modify node_ref_CSdk, node_ref_ASdki. Add
 T_geom_inj_l, T_geom_comm. WIP: T_geom_sym.

---
 FEM/LagP_node.v          |   3 +-
 FEM/LagP_node_ref.v      |  35 ++++++------
 FEM/geom_transf_affine.v | 112 ++++++++++++++++++++++++---------------
 3 files changed, 87 insertions(+), 63 deletions(-)

diff --git a/FEM/LagP_node.v b/FEM/LagP_node.v
index a7266a7c..a8684972 100644
--- a/FEM/LagP_node.v
+++ b/FEM/LagP_node.v
@@ -173,6 +173,7 @@ Variable vtx : 'R^{d.+1,d}.
  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.
@@ -262,7 +263,7 @@ Variable vtx : 'R^{d.+1,d}.
 Lemma T_geom_sub_nodeF :
   mapF (T_geom vtx) (sub_node k vtx_ref) = sub_node k vtx.
 Proof.
-rewrite !sub_nodeF -mapF_comp T_geom_assoc -sub_vtx_refF sub_vtxF; easy.
+rewrite !sub_nodeF -mapF_comp T_geom_comp -sub_vtx_refF sub_vtxF; easy.
 Qed.
 
 (**
diff --git a/FEM/LagP_node_ref.v b/FEM/LagP_node_ref.v
index 405d0181..11d33cac 100644
--- a/FEM/LagP_node_ref.v
+++ b/FEM/LagP_node_ref.v
@@ -60,8 +60,19 @@ Lemma node_ref_eqF :
   forall idk, node_ref idk = scal (/ INR k) (mapF INR (Adk d k idk)).
 Proof. intros; unfold node_ref; extF; rewrite div_eq mult_comm_R; easy. Qed.
 
+Lemma node_ref_inj : injective node_ref.
+Proof.
+case (Nat.eq_dec k 0); intros Hk.
+(* *)
+intros [i Hi] [j Hj] _; subst; apply ord_inj; simpl.
+rewrite pbinom_0_r in Hi, Hj; move: Hi => /ltP Hi; move: Hj => /ltP Hj; lia.
+(* *)
+intros idk jdk; rewrite !node_ref_eqF;
+    move=> /(scal_reg_r_R _ (INR_inv_n0 Hk)) /(mapF_inj INR_eq) /Adk_inj; easy.
+Qed.
+
 Lemma node_ref_CSdk :
-  forall idk, (0 < d)%coq_nat -> (0 < k)%coq_nat ->
+  forall (idk : 'I_(pbinom d k).+1), (0 < d)%coq_nat -> (0 < k)%coq_nat ->
     sum (node_ref idk) = 1 <-> ((pbinom d k.-1).+1 <= idk)%coq_nat.
 Proof.
 move=>> Hd Hk; rewrite -Adk_last_layer// node_ref_eqF -scal_sum_r sum_INR.
@@ -70,32 +81,20 @@ rewrite scal_eq_K mult_comm_R div_one_equiv// INR_eq_equiv; easy.
 Qed.
 
 Lemma node_ref_ASdki :
-  forall idk j, (0 < k)%coq_nat ->
-    node_ref idk j = 0 <-> Adk d k idk j = 0%nat.
+  forall idk i, (0 < k)%coq_nat -> node_ref idk i = 0 <-> Adk d k idk i = 0.
 Proof.
 move=>> /INR_n0 /invertible_equiv_R Hk.
-unfold node_ref; rewrite div_zero_equiv//; apply INR_0_equiv.
-Qed.
-
-Lemma node_ref_inj : injective node_ref.
-Proof.
-case (Nat.eq_dec k 0); intros Hk.
-(* *)
-intros [i Hi] [j Hj] _; subst; apply ord_inj; simpl.
-rewrite pbinom_0_r in Hi, Hj; move: Hi => /ltP Hi; move: Hj => /ltP Hj; lia.
-(* *)
-intros idk jdk; rewrite !node_ref_eqF;
-    move=> /(scal_reg_r_R _ (INR_inv_n0 Hk)) /(mapF_inj INR_eq) /Adk_inj; easy.
+unfold node_ref; rewrite div_zero_equiv// INR_0_equiv; easy.
 Qed.
 
 (**
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
  Lem 1605 (for [vtx_ref]), Eq (9.95), p. 101. #<BR>#
- \hat{a}_alpha \in \hat{Hface}_0 <-> alpha \in CSdk. *)
+ \hat{a}_alpha \in \hat{Hface}_0 <-> alpha \in CSdk, ie \sum alpha = k. *)
 Lemma node_ref_Hface_ref_0 :
   forall (idk : 'I_((pbinom d k).+1)), (0 < d)%coq_nat -> (0 < k)%coq_nat ->
     Hface_ref ord0 (node_ref idk) <-> ((pbinom d k.-1).+1 <= idk)%coq_nat.
-Proof. intros; rewrite Hface_ref_0_eq//; apply node_ref_CSdk; easy. Qed.
+Proof. intros; rewrite Hface_ref_0_eq// node_ref_CSdk; easy. Qed.
 
 (**
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
@@ -106,7 +105,7 @@ Lemma node_ref_Hface_ref_S :
   forall (idk : 'I_((pbinom d k).+1)) {i : 'I_d.+1} (Hi : i <> ord0),
     (0 < d)%coq_nat -> (0 < k)%coq_nat ->
     Hface_ref i (node_ref idk) <-> Adk d k idk (lower_S Hi) = O.
-Proof. intros; rewrite Hface_ref_S_eq; apply node_ref_ASdki; easy. Qed.
+Proof. intros; rewrite Hface_ref_S_eq node_ref_ASdki; easy. Qed.
 
 End Node_ref_Facts1.
 
diff --git a/FEM/geom_transf_affine.v b/FEM/geom_transf_affine.v
index 9f3c6384..baf7503e 100644
--- a/FEM/geom_transf_affine.v
+++ b/FEM/geom_transf_affine.v
@@ -98,20 +98,71 @@ Qed.
 End T_geom_Facts1.
 
 
-Section T_geom_Facts2.
+Section T_geom_ref_Facts.
 
 Context {d : nat}.
-Variable vtx1 vtx2 : 'R^{d.+1,d}.
 
-Lemma T_geom_assoc :
-  T_geom vtx1 \o T_geom vtx2 = T_geom (mapF (T_geom vtx1) vtx2).
+(**
+ #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
+ Lem 1549, p. 82. *)
+Lemma T_geom_ref :
+  forall vtx, vtx = vtx_ref -> T_geom vtx = (id : 'R^d -> 'R^d).
 Proof.
-apply: (am_ext_gen_full_ms _ _ vtx_ref);
+intros; subst; fun_ext x; destruct (aff_indep_aff_gen_R _
+    has_dim_Rn vtx_ref_aff_indep x) as [L [HL ->]].
+apply T_geom_baryc; easy.
+Qed.
+
+Lemma T_geom_scal_ref :
+  forall a vtx, invertible a -> vtx = vtx_ref ->
+    @T_geom d (mapF (scal a) vtx) = scal a.
+Proof.
+intros; fun_ext; rewrite T_geom_lc lc_scal_r -T_geom_lc T_geom_ref; easy.
+Qed.
+
+End T_geom_ref_Facts.
+
+
+Section T_geom_f_Facts2.
+
+Context {d : nat}.
+
+Lemma T_geom_inj_l : injective (@T_geom d).
+Proof. move=> v1 v2 H; extF; rewrite -(T_geom_vtx v1) H T_geom_vtx; easy. Qed.
+
+Lemma T_geom_comp :
+  forall( vtx1 vtx2 : 'R^{d.+1,d}),
+    T_geom vtx1 \o T_geom vtx2 = T_geom (mapF (T_geom vtx1) vtx2).
+Proof.
+intros; apply: (am_ext_gen_full_ms _ _ vtx_ref);
     [apply am_comp_ms |..]; [apply T_geom_am.. | apply vtx_ref_aff_gen |].
 intro; rewrite comp_correct !T_geom_vtx; easy.
 Qed.
 
-End T_geom_Facts2.
+Lemma T_geom_sym :
+  forall( vtx1 vtx2 : 'R^{d.+1,d}),
+    mapF (T_geom vtx1) vtx2 = mapF (T_geom vtx2) vtx1.
+Proof.
+intros; extF; rewrite !mapF_correct; unfold T_geom.
+assert (H : forall i, vtx1 i = barycenter_ms (LagPd1_ref^~ (vtx1 i)) vtx_ref)
+    by now intro; rewrite LagPd1_ref_barycF.
+apply extF in H; rewrite H.
+
+
+
+(*
+LagPd1_ref_barycF : barycenter_ms (LagPd1_ref^~ x_ref) vtx_ref = x_ref
+
+baryc_comm_r_R : barycenter L2 (barycenter L1 A) = barycenter L1 (mapF (barycenter L2) A)
+*)
+Admitted.
+
+Lemma T_geom_comm :
+  forall( vtx1 vtx2 : 'R^{d.+1,d}),
+    T_geom vtx1 \o T_geom vtx2 = T_geom vtx2 \o T_geom vtx1.
+Proof. intros; rewrite !T_geom_comp T_geom_sym; easy. Qed.
+
+End T_geom_f_Facts2.
 
 
 Section T_geom_inv_Facts.
@@ -174,16 +225,7 @@ Proof.
 intros; apply T_geom_inj; rewrite T_geom_inv_can_r T_geom_baryc; easy.
 Qed.
 
-End T_geom_inv_Facts.
-
-
-Section T_geom_K_geom_Facts.
-
-(* TODO FC (05/03/2025): is this section useful? *)
-
-Context {d : nat}.
-Context {vtx : 'R^{d.+1,d}}.
-Hypothesis Hvtx : aff_indep_ms vtx.
+(* TODO FC (05/03/2025): is the following useful? *)
 
 Let K_geom_ref : 'R^d -> Prop := convex_envelop vtx_ref.
 Let K_geom : 'R^d -> Prop := convex_envelop vtx.
@@ -193,7 +235,7 @@ Proof.
 move=>> [L HL1 HL2]; unfold K_geom, preimage; rewrite T_geom_baryc; easy.
 Qed.
 
-Lemma T_geom_inv_K_geom_incl : incl K_geom (preimage (T_geom_inv Hvtx) K_geom_ref).
+Lemma T_geom_inv_K_geom_incl : incl K_geom (preimage T_geom_inv K_geom_ref).
 Proof.
 move=>> [L HL1 HL2]; unfold K_geom, preimage; rewrite T_geom_inv_baryc; easy.
 Qed.
@@ -204,45 +246,27 @@ Qed.
 Lemma T_geom_K_geom_eq : image (T_geom vtx) K_geom_ref = K_geom.
 Proof.
 apply subset_ext_equiv; split; [apply image_incl_equiv, T_geom_K_geom_incl |
-    rewrite -(f_inv_preimage (T_geom_bij Hvtx)); apply T_geom_inv_K_geom_incl].
+    rewrite -(f_inv_preimage T_geom_bij); apply T_geom_inv_K_geom_incl].
 Qed.
 
-Lemma T_geom_inv_K_geom_eq : image (T_geom_inv Hvtx) (K_geom) = K_geom_ref.
+Lemma T_geom_inv_K_geom_eq : image T_geom_inv (K_geom) = K_geom_ref.
 Proof.
 rewrite -T_geom_K_geom_eq -image_comp T_geom_inv_id_l image_id; easy.
 Qed.
 
-End T_geom_K_geom_Facts.
+End T_geom_inv_Facts.
 
 
-Section T_geom_ref_Facts.
+Section T_geom_inv_ref_Facts.
 
 Context {d : nat}.
 
-(**
- #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
- Lem 1549, p. 82. *)
-Lemma T_geom_ref :
-  forall vtx, vtx = vtx_ref -> T_geom vtx = (id : 'R^d -> 'R^d).
-Proof.
-intros; subst; fun_ext x; destruct (aff_indep_aff_gen_R _
-    has_dim_Rn vtx_ref_aff_indep x) as [L [HL ->]].
-apply T_geom_baryc; easy.
-Qed.
-
 Lemma T_geom_inv_ref :
   forall vtx (H : aff_indep_ms vtx),
-    vtx = vtx_ref -> T_geom_inv H =(id : 'R^d -> 'R^d).
+    vtx = vtx_ref -> T_geom_inv H = (id : 'R^d -> 'R^d).
 Proof. intros; subst; apply f_inv_is_id, T_geom_ref; easy. Qed.
 
-Lemma T_geom_scal_ref :
-  forall a vtx, invertible a -> vtx = vtx_ref ->
-    @T_geom d (mapF (scal a) vtx) = scal a.
-Proof.
-intros; fun_ext; rewrite T_geom_lc lc_scal_r -T_geom_lc T_geom_ref; easy.
-Qed.
-
-End T_geom_ref_Facts.
+End T_geom_inv_ref_Facts.
 
 
 Section T_geom_permutF_Def.
@@ -250,7 +274,7 @@ Section T_geom_permutF_Def.
 Context {d : nat}.
 Variable vtx : 'R^{d.+1,d}.
 
-(** [pi_d] is a permutation of [0..d].
+(** [pi_d] is a permutation of [0..d.+1).
  The intention is to switch vertices. *)
 Variable pi_d : 'I_[d.+1].
 
@@ -267,7 +291,7 @@ Section T_geom_permutF_Facts.
 
 Context {d : nat}.
 Context {vtx : 'R^{d.+1,d}}.
-Hypothesis Hvtx: aff_indep_ms vtx.
+Hypothesis Hvtx : aff_indep_ms vtx.
 
 Context {pi_d : 'I_[d.+1]}.
 Hypothesis Hpi_d : injective pi_d.
@@ -350,7 +374,7 @@ Section T_geom_transpF_Facts.
 
 Context {d : nat}.
 Context {vtx : 'R^{d.+1,d}}.
-Hypothesis Hvtx: aff_indep_ms vtx.
+Hypothesis Hvtx : aff_indep_ms vtx.
 
 Definition T_geom_transpF_inv (i0 : 'I_d.+1) : 'R^d -> 'R^d :=
   T_geom_permutF_inv Hvtx (transp_ord_inj ord_max i0).
-- 
GitLab