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

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.
 

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.
 

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.
 

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.

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;

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) \/

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.
 

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.
 

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

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.
 

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

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 =

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

_CoqProject

@@ -14,6 +14,7 @@
 -arg "-w -ambiguous-paths"
 
 -docroot .
+# Options for coqdoc: --no-index -toc -g (or -l)
 
 #
 # Requisite.