Compare revisions

François Clément · François Clément · François Clément · François Clément · François Clément · François Clément
--- a/Algebra/AffineSpace/AffineSpace_aff_map.v
+++ b/Algebra/AffineSpace/AffineSpace_aff_map.v
@@ -563,7 +563,7 @@ Lemma fct_lm_ms_eq :
  forall {f : E1 -> E2} O1 u1, fct_lm f O1 u1 = f (O1 + u1) - f O1.
 Proof. unfold fct_lm; intros; rewrite ms_vect_eq ms_transl_eq; easy. Qed.

-Lemma fct_lm_ms_eq_ex:
+Lemma fct_lm_ms_eq_ex :
  forall {f lf : E1 -> E2},
    lin_map lf ->
    lf = fct_lm f 0 <-> exists c2, f = lf + (fun=> c2).

--- a/Algebra/Finite_dim/Finite_dim_AS_def.v
+++ b/Algebra/Finite_dim/Finite_dim_AS_def.v
@@ -191,7 +191,7 @@ Lemma has_aff_dim_EX :
  forall PE n, has_aff_dim PE n -> { A : 'E^n.+1 | aff_basis PE A }.
 Proof. move=>> H; apply ex_EX; induction H as [A H]; exists A; easy. Qed.

-Lemma has_aff_dim_ex:
+Lemma has_aff_dim_ex :
  forall PE n, (exists A : 'E^n.+1, aff_basis PE A) -> has_aff_dim PE n.
 Proof. move=>> [A HA]. apply (Aff_dim _ _ A HA). Qed.


--- a/Algebra/ModuleSpace/ModuleSpace_sub.v
+++ b/Algebra/ModuleSpace/ModuleSpace_sub.v
@@ -120,7 +120,7 @@ Definition scalF_rev_closed : Prop :=
 Definition lc_closed : Prop :=
  forall n L (B : 'E^n), inclF B PE -> PE (lin_comb L B).

-Definition compatible_ms : Prop:= compatible_g PE /\ scal_closed.
+Definition compatible_ms : Prop := compatible_g PE /\ scal_closed.

 End Compatible_ModuleSpace_Def.


--- a/Algebra/Monoid/Monoid_FF.v
+++ b/Algebra/Monoid/Monoid_FF.v
@@ -200,9 +200,9 @@ Lemma skipF_itemF_diag :
  forall n i0 (x : G), skipF i0 (itemF n.+1 i0 x) = 0.
 Proof. intros; rewrite skipF_replaceF; easy. Qed.

-Lemma skipF_itemF_0:
-  forall (n : nat) (i0 : 'I_n.+1) (H:i0 <> ord0) (x : G),
-   skipF ord0 (itemF n.+1 i0 x) = itemF n (lower_S H) x.
+Lemma skipF_itemF_0 :
+  forall (n : nat) (i0 : 'I_n.+1) (H : i0 <> ord0) (x : G),
+   skipF0 (itemF n.+1 i0 x) = itemF n (lower_S H) x.
 Proof.
 intros n i0 x H; rewrite skipF_first; unfold liftF_S; extF j.
 case (ord_eq_dec (lift_S j) i0); intros H1.
@@ -501,7 +501,7 @@ Lemma lastF_zero_compat :
    (forall i : 'I_(n1 + n2), (n1 <= i)%coq_nat -> A i = 0) -> lastF A = 0.
 Proof. move=>>; erewrite <- lastF_zero; apply lastF_compat. Qed.

-Lemma splitF_zero_compat:
+Lemma splitF_zero_compat :
  forall {n1 n2} (A : 'G^(n1 + n2)), A = 0 -> firstF A = 0 /\ lastF A = 0.
 Proof. move=>>; apply splitF_compat. Qed.


--- a/Algebra/Monoid/Monoid_morphism.v
+++ b/Algebra/Monoid/Monoid_morphism.v
@@ -293,7 +293,7 @@ Section Monoid_Morphism_Sum_Facts3.
 Context {G1 G2 : AbelianMonoid}.
 Context {T : Type}.

-Lemma sum_compF_r:
+Lemma sum_compF_r :
  forall {n} (u : G1 -> G2) (f : '(T -> G1)^n),
    morphism_m u -> sum (compF_r u f) = u \o sum f.
 Proof.

--- a/Algebra/Monoid/Monoid_sum.v
+++ b/Algebra/Monoid/Monoid_sum.v
@@ -410,7 +410,7 @@ Section Sum_Facts3.
 Context {G : AbelianMonoid}.
 Context {T1 T2 : Type}.

-Lemma sum_compF_l:
+Lemma sum_compF_l :
  forall {n} (u : '(T2 -> G)^n) (f : T1 -> T2), sum (compF_l u f) = sum u \o f.
 Proof.
 intros; fun_ext;

--- a/Algebra/Monoid/Monomial_order.v
+++ b/Algebra/Monoid/Monomial_order.v
@@ -1756,7 +1756,7 @@ Hypothesis HG2 : @plus_is_reg_r G.

 (* The proof depends on the plus regularity hypothesis HG2. *)
 Lemma grlex_S :
-  forall R {n} (x y :'G^n.+1),
+  forall R {n} (x y : 'G^n.+1),
    grlex R x y <->
    sum x <> sum y /\ R (sum x) (sum y) \/
    sum x = sum y /\ x ord0 <> y ord0 /\ R (x ord0) (y ord0) \/
@@ -1770,7 +1770,7 @@ Qed.

 (* The proof depends on the plus regularity hypothesis HG2. *)
 Lemma grcolex_S :
-  forall R {n} (x y :'G^n.+1),
+  forall R {n} (x y : 'G^n.+1),
    grcolex R x y <->
    sum x <> sum y /\ R (sum x) (sum y) \/
    sum x = sum y /\ x ord_max <> y ord_max /\ R (x ord_max) (y ord_max) \/
@@ -1784,7 +1784,7 @@ Qed.

 (* The proof depends on the plus regularity hypothesis HG2. *)
 Lemma grsymlex_S :
-  forall R {n} (x y :'G^n.+1),
+  forall R {n} (x y : 'G^n.+1),
    grsymlex R x y <->
    sum x <> sum y /\ R (sum x) (sum y) \/
    sum x = sum y /\ y ord0 <> x ord0 /\ R (y ord0) (x ord0) \/
@@ -1803,7 +1803,7 @@ Proof. tauto. Qed.
 (* The proof depends on the equality decidability hypothesis HG1,
  and the plus regularity hypothesis HG2. *)
 Lemma grsymlex_S_mo :
-  forall R {n} (x y :'G^n.+1),
+  forall R {n} (x y : 'G^n.+1),
    monomial_order R ->
    grsymlex R x y <->
    sum x <> sum y /\ R (sum x) (sum y) \/
@@ -1826,7 +1826,7 @@ Qed.

 (* The proof depends on the plus regularity hypothesis HG2. *)
 Lemma grevlex_S :
-  forall R {n} (x y :'G^n.+1),
+  forall R {n} (x y : 'G^n.+1),
    grevlex R x y <->
    sum x <> sum y /\ R (sum x) (sum y) \/
    sum x = sum y /\ y ord_max <> x ord_max /\ R (y ord_max) (x ord_max) \/
@@ -1841,7 +1841,7 @@ Qed.
 (* The proof depends on the equality decidability hypothesis HG1,
  and the plus regularity hypothesis HG2. *)
 Lemma grevlex_S_mo :
-  forall R {n} (x y :'G^n.+1),
+  forall R {n} (x y : 'G^n.+1),
    monomial_order R ->
    grevlex R x y <->
    sum x <> sum y /\ R (sum x) (sum y) \/

--- a/Algebra/Ring/Ring_sub.v
+++ b/Algebra/Ring/Ring_sub.v
@@ -98,7 +98,7 @@ Definition multF_closed : Prop :=

 Definition one_closed : Prop := PK 1.

-Definition compatible_r : Prop:= compatible_g PK /\ mult_closed /\ one_closed.
+Definition compatible_r : Prop := compatible_g PK /\ mult_closed /\ one_closed.

 End Compatible_Ring_Def.

@@ -308,7 +308,7 @@ Definition sub_mult (x y : PK_g) : PK_g :=

 Definition sub_one : PK_g := mk_sub (cr_one HPK : PK 1).

-Lemma sub_mult_assoc:
+Lemma sub_mult_assoc :
  forall x y z, sub_mult x (sub_mult y z) = sub_mult (sub_mult x y) z.
 Proof. intros; apply val_inj, mult_assoc. Qed.


--- a/FEM/FE_LagP.v
+++ b/FEM/FE_LagP.v
@@ -45,7 +45,7 @@ Close Scope R_scope.
 From Algebra Require Import Algebra_wDep.
 From FEM Require Import multi_index poly_Pdk poly_LagP1k poly_LagPd1_ref.
 From FEM Require Import geom_transf_affine poly_LagPd1.
-From FEM Require Import LagP_node FE FE_transf.
+From FEM Require Import LagP_node_ref LagP_node FE FE_transf.

 Local Open Scope Monoid_scope.
 Local Open Scope Group_scope.
@@ -153,6 +153,33 @@ Qed.

 (** Induction step: unisolvence result for d,k>1. *)

+Lemma unisolvence_inj_Hface :
+  forall {d k}, (0 < d)%coq_nat -> (0 < k)%coq_nat -> PI d k.+1 ->
+    forall i {vtx p}, aff_indep_ms vtx -> Pdk d.+1 k.+1 p ->
+      (forall (idk : [0..(pbinom d.+1 k.+1).+1)),
+        Hface vtx i (node vtx idk) -> p (node vtx idk) = 0) ->
+      forall x, Hface vtx i x -> p x = 0.
+Proof.
+intros d k Hd Hk H i vtx p Hvtx Hp1 Hp2 x Hx.
+assert (HSd : (0 < d.+1)%coq_nat) by apply S_pos.
+assert (HSk : (0 < k.+1)%coq_nat) by apply S_pos.
+rewrite -(f_invS_canS_r (T_geom_Hface_bijS Hvtx i) x)//.
+fold (T_geom_Hface_invS Hvtx i x).
+pose (pi := fun y => p (T_geom_Hface vtx i y));
+  fold (pi (T_geom_Hface_invS Hvtx i x)).
+rewrite (H _ vtx_ref_aff_indep pi)//.
+apply T_geom_Hface_comp; easy.
+extF idk; rewrite gather_eq; unfold Sigma_LagPSdSk, pi; rewrite -node_ref_node.
+destruct (ord_eq_dec i ord0) as [-> | Hi].
+(* i = ord0 *)
+rewrite T_geom_Hface_0_node//; apply Hp2, node_Hface_0; [easy.. |].
+apply Adk_last_layer; [easy.. |]; rewrite Adk_inv_correct_r inj_CSdk_sum//.
+(* i <> ord0 *)
+rewrite T_geom_Hface_S_node//; apply Hp2, (node_Hface_S Hvtx _ Hi HSd HSk).
+rewrite Adk_inv_correct_r;
+    [apply insertF_correct_l; easy | rewrite inj_ASdki_sum; apply Adk_sum].
+Qed.
+
 Lemma unisolvence_inj_ind_LagPSdSk :
  forall {d k}, (0 < d)%coq_nat -> (0 < k)%coq_nat ->
    PI d.+1 k -> PI d k.+1 -> PI d.+1 k.+1.
@@ -300,7 +327,7 @@ Section FE_LagPdk_from_ref.
 Lem 1604 (for k=0), p. 101.#<BR>#
 It is actually directly on the linear forms, rather than on the nodes. *)
 Lemma Sigma_LagPd0_eq_from_ref :
-  forall {d} (vtx :'R^{d.+1,d}) id0 p,
+  forall {d} (vtx : 'R^{d.+1,d}) id0 p,
    Sigma_LagPd0 vtx id0 p =
      Sigma_LagPd0 vtx_ref id0 (p \o (T_geom vtx)).
 Proof.
@@ -314,7 +341,7 @@ Qed.
 Lem 1604 (for k>0), p. 101.#<BR>#
 It is actually directly on the linear forms, rather than on the nodes. *)
 Lemma Sigma_LagPSdSk_eq_from_ref :
-  forall {d} k (vtx :'R^{d.+1,d}) i p,
+  forall {d} k (vtx : 'R^{d.+1,d}) i p,
    Sigma_LagPSdSk k vtx i p =
      Sigma_LagPSdSk k vtx_ref i (p \o (T_geom vtx)).
 Proof.
@@ -323,7 +350,7 @@ rewrite comp_correct -node_ref_node T_geom_node; easy.
 Qed.

 Variable d k : nat.
-Context {vtx :'R^{d.+1,d}}.
+Context {vtx : 'R^{d.+1,d}}.
 Hypothesis Hvtx : aff_indep_ms vtx.

 Definition FE_LagPdk_ref := FE_LagPdk k (@vtx_ref_aff_indep d).
@@ -375,7 +402,7 @@ Section Face_unisolvence.
 Context {d k : nat}.
 Hypothesis Hd : (1 < d)%coq_nat.
 Hypothesis Hk : (0 < k)%coq_nat.
-Context {vtx :'R^{d.+1,d}}.
+Context {vtx : 'R^{d.+1,d}}.
 Hypothesis Hvtx : aff_indep_ms vtx.

 (**
@@ -384,24 +411,24 @@ Hypothesis Hvtx : aff_indep_ms vtx.
 Case i=0. *)
 Lemma Hface_0_unisolvence :
  forall p, Pdk d k p ->
-    (forall idk : 'I_(pbinom d k).+1,
-      ((pbinom d k.-1).+1 <= idk)%coq_nat -> p (node vtx idk) = 0) <->
+    (forall (idk : 'I_(pbinom d k).+1),
+      Hface vtx ord0 (node vtx idk) -> p (node vtx idk) = 0) <->
    (forall x, Hface vtx ord0 x -> p x = 0).
 Proof.
 assert (Hd0 : (0 < d)%coq_nat) by now apply Nat.lt_le_incl.
-intros p Hp; split;
-    [| intros H idk Hidk; apply H, node_Hface_0; easy].
+intros p Hp; split; [| intros H idk Hidk; apply H; easy].
 intros H x Hx; destruct d as [| d1]; [easy |].
 assert (Hd1 : (0 < d1)%coq_nat) by now apply Nat.succ_lt_mono.
 rewrite -(f_invS_canS_r (T_geom_Hface_bijS Hvtx ord0) x)//.
 fold (T_geom_Hface_invS Hvtx ord0 x).
-pose (p0:= fun y => p (T_geom_Hface vtx ord0 y));
+pose (p0 := fun y => p (T_geom_Hface vtx ord0 y));
  fold (p0 (T_geom_Hface_invS Hvtx ord0 x)).
 rewrite (unisolvence_inj_LagPSdSk Hd1 Hk _ vtx_ref_aff_indep p0)//.
 apply T_geom_Hface_comp; easy.
 extF idk; rewrite gather_eq; unfold Sigma_LagPSdSk, p0.
 rewrite -node_ref_node T_geom_Hface_0_node//.
-apply H, Adk_last_layer; [easy.. |]; rewrite Adk_inv_correct_r inj_CSdk_sum//.
+apply H, node_Hface_0; [easy.. |].
+apply Adk_last_layer; [easy.. |]; rewrite Adk_inv_correct_r inj_CSdk_sum//.
 Qed.

 (**
@@ -410,12 +437,12 @@ Qed.
 Case i<>0. *)
 Lemma Hface_S_unisolvence :
  forall {i} (Hi : i <> ord0) p, Pdk d k p ->
-    (forall idk, Adk d k idk (lower_S Hi) = O -> p (node vtx idk) = 0) <->
+    (forall (idk : 'I_(pbinom d k).+1),
+      Hface vtx i (node vtx idk) -> p (node vtx idk) = 0) <->
    (forall x, Hface vtx i x -> p x = 0).
 Proof.
 assert (Hd0 : (0 < d)%coq_nat) by now apply Nat.lt_le_incl.
-intros i Hi p Hp; split;
-    [| move=> H idk /(node_Hface_S Hvtx) Hidk; apply H, Hidk; easy].
+intros i Hi p Hp; split; [| move=> H idk Hidk; apply H; easy].
 intros H x Hx; destruct d as [| d1]; [easy |].
 assert (Hd1 : (0 < d1)%coq_nat) by now apply Nat.succ_lt_mono.
 rewrite -(f_invS_canS_r (T_geom_Hface_bijS Hvtx i) x)//.
@@ -426,7 +453,7 @@ rewrite (unisolvence_inj_LagPSdSk Hd1 Hk _ vtx_ref_aff_indep pi)//.
 apply T_geom_Hface_comp; easy.
 extF idk; rewrite gather_eq; unfold Sigma_LagPSdSk, pi.
 rewrite -node_ref_node T_geom_Hface_S_node//.
-apply H; rewrite Adk_inv_correct_r;
+apply H, (node_Hface_S Hvtx _ Hi Hd0 Hk); rewrite Adk_inv_correct_r;
    [apply insertF_correct_l; easy | rewrite inj_ASdki_sum; apply Adk_sum].
 Qed.


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

 (**

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


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

--- a/FEM/poly_LagPd1.v
+++ b/FEM/poly_LagPd1.v
@@ -295,7 +295,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.
@@ -342,7 +342,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.

 Lemma LagPd1_eq_transpF :
  forall i0 j, LagPd1 Hvtx j =

--- a/Subsets/ord_compl.v
+++ b/Subsets/ord_compl.v
@@ -29,6 +29,7 @@ COPYING file for more details.

 ** Additional notations

+ - <<[0..n)>> is for ['I_n];
 - ['I_{m,n}] is for ['I_m -> 'I_n];
 - ['I_[n]] is for ['I_{n,n}];
 - ['I_{m,n,p}] is for ['I_m -> 'I_{n,p}].

--- a/_CoqProject
+++ b/_CoqProject
@@ -14,6 +14,7 @@
 -arg "-w -ambiguous-paths"

 -docroot .
+# Options for coqdoc: --no-index -toc -g (or -l)

 #
 # Requisite.
No results found