Prove is_linear_mapping_sigma_cur_aux lemma

Work on other proofs of T_geom.

FEM/finite_element.v

@@ -77,7 +77,7 @@ Canonical Pol_MS2 :=
 Definition Pval : Pol -> F := fun (p : Pol) => val p.
 Coercion Pval : Pol >-> F.
 
-(** Livre d_refAlexandre Ern: Def (4.1) P.76*)
+(** Livre Alexandre Ern: Def (4.1) P.76*)
 Definition is_unisolvant : (F -> 'R^n) -> Prop :=
   fun sigma => forall alpha : 'R^n, 
      exists! p : Pol, sigma p = alpha.
@@ -170,7 +170,7 @@ Section FE_Local_Def2.
 
 (* HM: dof are not defined yet ? *)
 
-(** Livre d_refAlexandre Ern: Def(4.1) P.75*)
+(** Livre Alexandre Ern: Def(4.1) P.75*)
 Record FE : Type := mk_FE {
   d : nat ; (* space dimension eg 1, 2, 3 *)
   ndof : nat ; (* nb of degrees of freedom - eg number of nodes for Lagrange. *)
@@ -261,7 +261,7 @@ rewrite gather_is_linear_mapping_compat in sigma_is_linear0.
 easy.
 Qed.
 
-(** Livre d_refAlexandre Ern: Def(4.4) P.78*)
+(** Livre Alexandre Ern: Def(4.4) P.78*)
 Definition interp_op_local  : F (d fe) -> F (d fe) := 
   fun v => comb_lin (fun i => sigma fe i v) theta.
 
@@ -305,7 +305,7 @@ apply theta_correct.
 apply comb_lin_kronecker_in_l.
 Qed.
 
-(** Livre d_refAlexandre Ern: Def (3.2) P.47 - Def (4.4) P.78*)
+(** Livre Alexandre Ern: Def (3.2) P.47 - Def (4.4) P.78*)
 Lemma interp_op_local_proj : forall p : F (d fe),
   (P_approx fe) p -> interp_op_local p = p.
 Proof.
@@ -319,7 +319,7 @@ apply interp_op_local_theta.
 apply interp_op_local_is_linear_mapping.
 Qed.
 
-(** Livre d_refAlexandre Ern: Def (3.2) P.47 - Def (4.4) P.78*)
+(** Livre Alexandre Ern: Def (3.2) P.47 - Def (4.4) P.78*)
 (* idempotence *)
 Lemma interp_op_local_idem : forall v : F (d fe),
   interp_op_local (interp_op_local v) =
@@ -394,7 +394,7 @@ Local Definition FE_is_unisolvant_ref := FE_is_unisolvant FE_ref.
   and on the degree. *)
 Variable Lag_P1_ref : '('R^dd -> R)^nnvtx.
 
-(* HM : nndof or nnvtx ? verify all thetas (def or var) and their types *)
+(* HM : Verify all thetas (def or var) and their types *)
 Local Definition theta_ref : '(F dd)^nndof := theta FE_ref.
 
 Hypothesis H_Lag_P1_ref : forall i j,
@@ -403,8 +403,6 @@ Hypothesis H_Lag_P1_ref : forall i j,
 Definition interp_op_local_ref : F dd -> F dd := 
   fun v => interp_op_local FE_ref v.
 
-(** construct the FE_current *)
-
 Variable vtx_cur : '('R^dd)^nnvtx. (*vertices of current geometrical element*)
 
 (* HM: Verify if the type of this definition is correct *)
@@ -428,9 +426,13 @@ Admitted.
 Definition T_geom_inv : 'R^dd -> 'R^dd := fun x =>
   epsilon is_domain_inhabited (fun y => T_geom y = x).
 
-Lemma T_geom_inv_correct1 : forall x : 'R^dd, 
-  (*identity P_approx_ref T_geom T_geom_inv.*)
-  T_geom (T_geom_inv x) = x.
+Lemma T_geom_inv_is_bij_id :
+  is_bij_id K_geom_ref (convex_envelop nnvtx vtx_cur) T_geom T_geom_inv.
+Proof.
+Admitted.
+
+Lemma T_geom_inv_correct1 :
+  forall x : 'R^dd, T_geom (T_geom_inv x) = x.
 Proof.
 unfold T_geom_inv, epsilon.
 intros x; destruct (classical_indefinite_description _); simpl.
@@ -446,13 +448,20 @@ intros x; destruct (classical_indefinite_description _); simpl.
 admit. (* T_geom injective *)
 Admitted.
 
-Lemma T_geom_inv_is_bij_id :
-  is_bij_id K_geom_ref (convex_envelop nnvtx vtx_cur) T_geom T_geom_inv.
+Lemma T_geom_inv_correct2_aux :
+  identity K_geom_ref T_geom T_geom_inv.
 Proof.
+unfold identity, T_geom_inv, epsilon.
+intros x Hx; destruct (classical_indefinite_description _); simpl.
+eapply is_bij_id_is_inj.
+apply T_geom_inv_is_bij_id.
+2 : try easy.
+2 : apply e.
+unfold K_geom_ref, K_geom.
+admit.
+exists x; easy.
 Admitted.
 
-(* Dans FD y'a pas le lemme de bij <-> inj /\ surj ? *)
-
 (* TODO: could have been:
  Definition vtx_ref : nat -> E := fun i 
     => T_geom_inv (vtx_cur i). *) 
@@ -494,7 +503,7 @@ Definition P_approx_cur : F dd -> Prop :=
 (* HM : P_approx_cur est un sev de F de dimension finie ? *)
 Lemma P_compat_fin_cur : has_dim P_approx_cur nndof.
 Proof.
-(*P_compat_fin.*)
+unfold P_approx_cur, cur_to_ref.
 Admitted.
 
 Definition sigma_cur : '(F dd -> R)^(nndof) := 
@@ -510,18 +519,23 @@ apply sigma_is_linear; easy.
 apply sigma_is_linear; easy.
 Qed.
 
+Lemma is_linear_mapping_sigma_cur_aux :
+  is_linear_mapping (gather nndof sigma_cur).
+Proof.
+unfold is_linear_mapping; split; intros y; unfold sigma_cur.
+intros z.
+apply functional_extensionality; intros i.
+apply sigma_is_linear; easy.
+intros l; apply functional_extensionality; intros i.
+apply sigma_is_linear; easy.
+Qed.
+
 (* TODO: Next lemma needs properties on T_geom (eg C1-diffeomorphism) which should be automatically obtained from properties of the input vtx_cur. Then unisolvance of the current FE is deduced from that of the reference FE. *)
 
-(* HM: J'ai ajouté gather *)
 Lemma FE_cur_is_unisolvant : 
   is_unisolvant dd nndof P_approx_cur (gather nndof sigma_cur).
 Proof.
-eapply is_unisolvant_equiv.
-(*apply is_linear_mapping_sigma_cur.*)
-admit.
-intros p Hp.
-(*apply is_unisolvant_is_free.*)
-admit.
+(*apply FE_is_unisolvant.*)
 Admitted.
 
 Definition FE_cur :=
@@ -538,13 +552,7 @@ Definition K_cur : 'R^d_cur -> Prop := K_geom FE_cur.
 Lemma K_cur_correct : image T_geom K_geom_ref = K_cur.
 Proof.
 unfold T_geom.
-Admitted.
-
-Variable U1 U2 : Type.
-Variable PU1 : U1 -> Prop.
-
-Lemma toto : forall x (f : U1 -> U2),
-  image f PU1 (f x) -> PU1 x.
+(* image de type inductive *)
 Admitted.
 
 Lemma K_cur_correct_idem : forall x_ref : 'R^dd, 
@@ -554,8 +562,6 @@ intros x_ref.
 split; intros H1.
 (* => *)
 rewrite <- K_cur_correct in H1.
-(*apply toto.*)
-
 admit.
 (* <= *)
 rewrite <- K_cur_correct.
@@ -564,8 +570,6 @@ Admitted.
 Definition cur_to_ref_inv : F dd -> F dd := fun x =>
   epsilon is_domain_inhabited (fun y => cur_to_ref y = x).
 
-(* HM : these two lemmas should be also collected in one
-  that says cur_to_ref est bijective then it is inversible*)
 Lemma is_bijective1_cur_to_ref : forall v : F dd,
   cur_to_ref (cur_to_ref_inv v) = v.
 Proof.
@@ -585,6 +589,10 @@ Definition theta_cur : '(F d_cur)^ndof_cur := theta FE_cur.
 
 Lemma theta_cur_correct : forall i : 'I_(ndof FE_cur), 
   theta_ref i = cur_to_ref (theta_cur i).
+Proof.
+intros i.
+unfold cur_to_ref.
+apply functional_extensionality; intros x_ref.
 Admitted.
 
 Lemma theta_cur_correct_inv : forall i : 'I_(ndof FE_cur), 
@@ -606,8 +614,7 @@ intros v.
 unfold interp_op_local_ref, interp_op_local_cur, interp_op_local.
 rewrite linear_mapping_comb_lin_compat; try easy.
 apply comb_lin_ext; intros i.
-f_equal.
-apply theta_cur_correct.
+f_equal; apply theta_cur_correct.
 Qed.
 
 End FE_Current_Def.
@@ -642,10 +649,6 @@ Hypothesis nvtx_lagrange_pos : (0 < nvtx_lagrange)%nat.
 (* This was defined as 
 Variable P_approx_lagrange : @FiniteDim (@fct_ModuleSpace E R_ModuleSpace).*)
 
-(* HM: TODO: Soit 
-  - P_approx_lagrange est un espace de poly ou sev de fct de dim finie et on le met en définition,
-  - on met P_approx_lagrange en variable et on ajoute les hypothèses dont on a besoin. *)
-
 (* MM : comment on définit les polynômes de P_approx_lag ? *)
 (* FC: ceci doit être une definition a partir de k_lagrange *)
 Variable P_approx_lagrange : F dl -> Prop. (*:= P_approx fe_lag*)
@@ -653,7 +656,6 @@ Variable P_approx_lagrange : F dl -> Prop. (*:= P_approx fe_lag*)
 Lemma P_compat_fin_lagrange : 
   has_dim P_approx_lagrange ndof_lagrange.
 Proof.
-(*P_compat_fin.*)
 Admitted.
 
 (*Variable dimE : nat.
@@ -685,20 +687,9 @@ Lemma FE_lagrange_is_unisolvant :
   is_unisolvant dl nnode_lagrange P_approx_lagrange
     (gather nnode_lagrange sigma_lagrange).
 Proof.
-(*
-apply is_unisolvant_equiv.
-intros p; split.
-admit. (* dim=card*)
-intros H1.
-admit. (* libre ? *)
-*)
+(*eapply FE_is_unisolvant.*)
 Admitted.
 
-(* HM: I have created 
-    - dl 
-    - dl_pos, ndof_lagrange_pos, nvtx_lagrange_pos as hypotheses !!
-    - P_approx_lagrange as a subspace of F with finite dimension
-*)
 Definition FE_lagrange := 
   mk_FE dl ndof_lagrange nvtx_lagrange dl_pos ndof_lagrange_pos nvtx_lagrange_pos vtx_lagrange P_approx_lagrange P_compat_fin_lagrange 
 sigma_lagrange sigma_lagrange_is_linear FE_lagrange_is_unisolvant.