Seance de renommage.

FEM/Algebra/Finite_dim_R.v

@@ -2198,3 +2198,15 @@ apply aff_indep_aff_gen; easy.
 Qed.
 
 End ModuleSpace_AffineSpace_R_Facts.
+
+
+Section FRd_Def.
+
+(* FRd est un espace vectoriel de fonctions de dimension infinie *)
+Definition FRd d := 'R^d -> R.
+
+(* TODO: Future work,
+ FIXME: COMMENTS TO BE REMOVED FOR PUBLICATION!
+Definition FRdm d m := 'R^d -> 'R^m.*)
+
+End FRd_Def.

FEM/FE.v

@@ -27,7 +27,7 @@ Set Warnings "notation-overridden".
 
 From Lebesgue Require Import Subset.
 
-From FEM Require Import Compl Algebra geometry poly_Pdk.
+From FEM Require Import Compl Algebra geometry.
 
 
 Local Open Scope R_scope.

FEM/FE_simplex.v

@@ -36,56 +36,58 @@ Local Open Scope R_scope.
 
 Section FE_Current_Simplex.
 
-(* Note du 30/11/23 :
+(* FIXME: COMMENTS TO BE REMOVED FOR PUBLICATION!
+ Note du 30/11/23 :
 à un moment, prouver aff_ind vtx -> existe boule ouverte dans K
  prouver pour elt de ref et en déduire avec Tgeom
  isobarycenter
  intérieur non vide devrait être dans le Record
 *)
 
-(* 20/12/23 : Extract definitions and lemmas that will be applied to both simplex and Quad.
+(* FIXME: COMMENTS TO BE REMOVED FOR PUBLICATION!
+ 20/12/23 : Extract definitions and lemmas that will be applied to both simplex and Quad.
   Do we need modules ? *)
 
 (** Construct a FE_current from a given FE_ref and given current vertices vtx_cur. *)
 
 Variable FE_ref : FE.
 
-(* Local Definition is useful ? *)
-Local Definition dd := d FE_ref.
+(* Let is useful ? *)
+Let dd := d FE_ref.
 
-Local Definition nndof := ndof FE_ref.
+Let nndof := ndof FE_ref.
 
-Local Definition dd_pos := d_pos FE_ref.
+Let dd_pos := d_pos FE_ref.
 
-Local Definition nndof_pos := ndof_pos FE_ref.
+Let nndof_pos := ndof_pos FE_ref.
 
-Local Definition shape_ref := shape FE_ref.
+Let shape_ref := shape FE_ref.
 
 Hypothesis shape_ref_is_Simplex : shape_ref = Simplex.
 
-Local Definition P_approx_ref : FRd dd -> Prop := P_approx FE_ref.
+Let P_approx_ref : FRd dd -> Prop := P_approx FE_ref.
 
-Local Definition P_approx_has_dim_ref := P_approx_has_dim FE_ref.
+Let P_approx_has_dim_ref := P_approx_has_dim FE_ref.
 
-Local Definition Sigma_ref : '(FRd dd -> R)^nndof := Sigma FE_ref.
+Let Sigma_ref : '(FRd dd -> R)^nndof := Sigma FE_ref.
 
-Local Definition Sigma_lm_ref := Sigma_lm FE_ref.
+Let Sigma_lm_ref := Sigma_lm FE_ref.
 
-Local Definition unisolvence_ref := unisolvence FE_ref.
+Let unisolvence_ref := unisolvence FE_ref.
 
-Local Definition shape_fun_ref : '(FRd dd)^nndof := shape_fun FE_ref.
+Let shape_fun_ref : '(FRd dd)^nndof := shape_fun FE_ref.
 
-Local Definition local_interp_ref : FRd dd -> FRd dd :=
+Let local_interp_ref : FRd dd -> FRd dd :=
   fun v => local_interp FE_ref v.
 
-Local Definition nnvtx :=  S dd.
+Let nnvtx :=  S dd.
 
 Lemma nnvtx_eq_S_dd : nvtx FE_ref = S dd.
 Proof.
 apply (nvtx_Simplex FE_ref shape_ref_is_Simplex).
 Qed.
 
-Local Definition vtx_ref : '('R^dd)^nnvtx := castF nnvtx_eq_S_dd (vtx FE_ref).
+Let vtx_ref : '('R^dd)^nnvtx := castF nnvtx_eq_S_dd (vtx FE_ref).
 
 Lemma P_approx_ref_zero : P_approx_ref zero.
 Proof.
@@ -94,7 +96,7 @@ apply: has_dim_compatible_ms.
 apply FE_ref.
 Qed.
 
-Local Definition K_geom_ref : 'R^dd -> Prop := convex_envelop vtx_ref.
+Let K_geom_ref : 'R^dd -> Prop := convex_envelop vtx_ref.
 
 Lemma K_geom_ref_def_correct : K_geom_ref = K_geom FE_ref.
 Proof.
@@ -145,7 +147,7 @@ unfold cur_to_ref in H1.
 apply (fun_ext_rev H1 (T_geom_inv vtx_cur Hvtx x_cur)).
 Qed.
 
-Lemma cur_to_ref_inj_aux : forall v_ref,
+Lemma cur_to_ref_inj_zero : forall v_ref,
   cur_to_ref v_ref = zero -> v_ref = zero.
 Proof.
 intros v_ref H.
@@ -192,7 +194,7 @@ unfold P_approx_cur, preimage in H.
 rewrite -ref_to_cur_comp; try easy.
 Qed.
 
-Lemma cur_to_ref_bij :
+Lemma cur_to_ref_bijS :
   bijS (preimage cur_to_ref P_approx_ref) P_approx_ref cur_to_ref.
 Proof.
 apply bijS_ex; try apply inhabited_ms.
@@ -216,7 +218,7 @@ apply lm_cur_to_ref.
 apply (has_dim_compatible_ms _ (P_approx_has_dim FE_ref)).
 Qed.
 
-Lemma P_approx_cur_compat_fin : has_dim P_approx_cur nndof.
+Lemma P_approx_cur_has_dim : has_dim P_approx_cur nndof.
 Proof.
 assert (H : image cur_to_ref (preimage cur_to_ref P_approx_ref) = P_approx_ref).
 rewrite image_of_preimage.
@@ -236,7 +238,7 @@ apply fun_ext; intro; apply cur_to_ref_comp.
 (* *)
 apply P_approx_cur_compatible.
 (* *)
-rewrite H; apply cur_to_ref_bij.
+rewrite H; apply cur_to_ref_bijS.
 (* *)
 intros i.
 apply P_approx_cur_correct.
@@ -244,7 +246,7 @@ unfold P_approx_ref; rewrite (proj1 (shape_fun_basis FE_ref)).
 rewrite -lc_kronecker_l_in_r; easy.
 Qed.
 
-Definition Sigma_cur : '(FRd dd -> R)^(nndof) :=
+Let Sigma_cur : '(FRd dd -> R)^(nndof) :=
   fun i (p : FRd dd) => Sigma_ref i (cur_to_ref p).
 
 Lemma Sigma_cur_lm : forall i : 'I_(nndof),
@@ -261,13 +263,13 @@ Lemma unisolvence_cur :
 Proof.
 assert (K: compatible_ms P_approx_ref).
 eapply has_dim_compatible_ms; apply FE_ref.
-apply (lmS_bijS_sub_full_equiv _ P_approx_cur_compat_fin _ has_dim_Rn
+apply (lmS_bijS_sub_full_equiv _ P_approx_cur_has_dim _ has_dim_Rn
     (proj1 (gather_lm_compat _) Sigma_cur_lm) eq_refl).
-pose (PC:= (has_dim_compatible_ms _ P_approx_cur_compat_fin)); fold PC.
+pose (PC:= (has_dim_compatible_ms _ P_approx_cur_has_dim)); fold PC.
 pose (PR:= (has_dim_compatible_ms _ (P_approx_has_dim FE_ref))).
 (* *)
 intros [q Hq] H1; simpl in H1.
-apply val_inj, cur_to_ref_inj_aux; try easy; simpl.
+apply val_inj, cur_to_ref_inj_zero; try easy; simpl.
 specialize (P_approx_ref_correct q Hq); try easy; intros H2.
 apply trans_eq with (val (mk_sub_ms_ PR H2)); try easy.
 apply trans_eq with (val (sub_zero (compatible_g_m (compatible_ms_g PR)))); try easy; f_equal.
@@ -280,14 +282,14 @@ Qed.
 Definition FE_cur :=
   mk_FE dd nndof dd_pos nndof_pos shape_ref
   (castF (eq_sym nnvtx_eq_S_dd) vtx_cur)
-  P_approx_cur P_approx_cur_compat_fin Sigma_cur
+  P_approx_cur P_approx_cur_has_dim Sigma_cur
   Sigma_cur_lm unisolvence_cur.
 
-Definition d_cur := d FE_cur.
+Let d_cur := d FE_cur.
 
-Definition ndof_cur := ndof FE_cur.
+Let ndof_cur := ndof FE_cur.
 
-Definition shape_fun_cur : '(FRd d_cur)^ndof_cur := shape_fun FE_cur.
+Let shape_fun_cur : '(FRd d_cur)^ndof_cur := shape_fun FE_cur.
 
 Lemma nvtx_cur_eq : nvtx FE_cur = dd.+1.
 Proof.
@@ -295,11 +297,12 @@ apply nvtx_Simplex.
 unfold FE_cur; easy.
 Qed.
 
-Lemma K_geom_cur_def_correct : K_geom_cur = K_geom FE_cur.
+Lemma K_geom_cur_correct : K_geom_cur = K_geom FE_cur.
 Proof.
 apply (convex_envelop_castF (eq_sym nnvtx_eq_S_dd)); easy.
 Qed.
 
+(* TODO SB (13/05/2024) : essayer de simplifier les deux preuves suivantes. *)
 Lemma P_approx_ref_image :
   image ref_to_cur P_approx_ref = P_approx_cur.
 Proof.
@@ -378,13 +381,13 @@ apply H2.
 Qed.
 
 Lemma shape_fun_cur_correct_rev : forall i : 'I_(ndof FE_cur),
-  shape_fun FE_ref i = cur_to_ref (shape_fun_cur i).
+  shape_fun_ref i = cur_to_ref (shape_fun_cur i).
 Proof.
 intros i; rewrite shape_fun_cur_correct.
 apply cur_to_ref_comp.
 Qed.
 
-Definition local_interp_cur : FRd d_cur -> FRd d_cur :=
+Let local_interp_cur : FRd d_cur -> FRd d_cur :=
   fun v => local_interp FE_cur v.
 
 (* From Aide-memoire EF Alexandre Ern : Eq 4.13 p. 79-80 *)
@@ -402,7 +405,7 @@ Qed.
 End FE_Current_Simplex.
 
 
-(*
+(* FIXME: COMMENTS TO BE REMOVED FOR PUBLICATION!
 Section FE_Current_Quad.
 
 (** FE QUAD *)

FEM/poly_Pdk.v

@@ -95,13 +95,6 @@ ON VEUT
       = \delta p / \delta x_1 ++ \delta_p / \delta x_2 ++ ... d
 *)
 
-(* FRd est un espace vectoriel de fonctions de dimension infinie *)
-Definition FRd d := 'R^d -> R.
-
-(* TODO: Future work,
- FIXME: COMMENTS TO BE REMOVED FOR PUBLICATION!
-Local Definition F := 'R^d -> 'R^m.*)
-
 (* BasisPdk est une base de Pdk, c'est-à-dire une famille de fonctions. *)
 (** "Livre Vincent Definition 1593 - p30." *)
 Definition BasisPdk d k : '(FRd d)^((pbinom d k).+1) :=