Start using comb_lin, and new def dual_basis.

FEM/finite_element.v

@@ -132,6 +132,13 @@ rewrite sigma_is_inj_equiv; try easy.
 apply is_bij_is_inj with n; easy.
 Qed.
 
+Lemma is_unisolvant_is_free :
+  forall sigma : F -> 'R^n,
+    is_linear_mapping sigma ->
+    is_unisolvant sigma -> is_free n (scatter n sigma).
+Proof.
+Admitted.
+
 End FE_Local_Def1.
 
 Section FE_Local_Def2.
@@ -169,12 +176,17 @@ Definition is_shape_fun_local :=
   (forall i : 'I_(ndof fe),  P_approx fe (theta i)) /\
   (forall i j : 'I_(ndof fe), sigma fe i (theta j) = kronecker i j).
 
-Lemma theta_is_shape_fun_local :
-  {theta : '(F (d fe))^(ndof fe) | is_shape_fun_local theta}.
+(* TODO: define theta in a similar way to dual_basis. *)
+
+Definition theta : '(F (d fe))^(ndof fe).
 Proof.
-unfold is_shape_fun_local.
-apply constructive_indefinite_description.
-destruct (choice (fun (j : 'I_(ndof fe)) p => (P_approx fe p) /\ (forall i : 'I_(ndof fe), (sigma fe) i p = kronecker i j))) as (theta,H).
+generalize (choice (fun (j : 'I_(ndof fe)) p => (P_approx fe p) /\
+                    (forall i : 'I_(ndof fe), (sigma fe) i p = kronecker i j))).
+intros T.
+apply constructive_indefinite_description in T.
+(* *)
+destruct T as [x Hx].
+apply x.
 (* *)
 intros j.
 destruct (FE_is_unisolvant fe (fun i => kronecker i j)) as (p,(Hp1,Hp2)).
@@ -182,65 +194,54 @@ destruct p as (y,Hy).
 exists y.
 split; try easy.
 simpl in Hp1, Hp2.
-intros i.
-replace (sigma fe i y) with (gather (ndof fe) (sigma fe) y i); try easy.
+intros k.
+replace (sigma fe k y) with (gather (ndof fe) (sigma fe) y k); try easy.
 rewrite Hp1; easy.
-(* *)
-exists theta; split.
-intros i; apply H.
-intros i j; apply H.
-Qed. (* TODO: Defined? *)
+Defined.
 
-Definition my_theta := proj1_sig theta_is_shape_fun_local.
-
-Lemma my_theta_is_shape_fun_local : is_shape_fun_local my_theta.
+Lemma theta_correct : is_shape_fun_local theta.
 Proof.
-Admitted.
+unfold theta.
+destruct (constructive_indefinite_description _) as [x Hx].
+split; try apply Hx.
+intros; apply Hx.
+Qed.
 
-(* Just to verify if my_theta works well *)
-Lemma my_theta_is_poly : forall i,
-   P_approx fe (my_theta i).
+(* Just to verify if theta works well *)
+Lemma theta_is_poly : forall i,
+   P_approx fe (theta i).
 Proof.
-intros i.
-unfold my_theta.
-destruct (theta_is_shape_fun_local) as (theta, H); simpl.
-apply H.
+apply theta_correct.
 Qed.
 
 (* TODO : les theta forment une base *)
-Lemma my_theta_is_basis :
-  is_basis (P_approx fe) (ndof fe) my_theta.
+Lemma theta_is_basis :
+  is_basis (P_approx fe) (ndof fe) theta.
 Proof.
 rewrite is_dual_is_basis.
-2: { unfold my_theta.
-  destruct (theta_is_shape_fun_local) as (theta, (H1,H2)); simpl.
-  unfold is_dual_family; apply H2. }
+2: intros i j; apply theta_correct.
 apply span_is_basis.
-(* TODO put the sequel in a result about sigma's. *)
-unfold is_free.
-intros L HL j.
-assert (HLj1: (\big[plus/zero]_(i < ndof fe) scal (L i) (sigma fe i)) (my_theta j) = 0).
-  rewrite HL; easy.
-assert (HLj2: \big[Rplus/0]_(i < ndof fe) ((L i) * (sigma fe i (my_theta j))) = 0).
-  admit. (* Hint: replace zero by some \big then bigop_ext... *)
-unfold my_theta in HLj2.
-destruct (theta_is_shape_fun_local) as (theta, (H1,H2)); simpl in HLj2.
-rewrite (bigop_ext _ _ _ _ (fun i => (kronecker i j) * (L i))) in HLj2.
-rewrite kronecker_bigop_scal_in_l in HLj2; try easy.
-intros i.
-rewrite H2; lra.
-Admitted.
+apply is_unisolvant_is_free with
+    (P := P_approx fe) (P_compatible_finite := P_compat_fin fe).
+apply 0%nat. (* should disappear. *)
+simpl.
+2: apply (FE_is_unisolvant fe).
+destruct fe; simpl.
+rewrite gather_is_linear_mapping_compat in sigma_is_linear0.
+easy.
+Qed.
 
 (** Livre d'Alexandre Ern: Def(4.4) P.78*)
 Definition interp_op_local := fun v => 
-    \big[plus%R/zero]_(i < ndof fe) scal (sigma fe i v) (my_theta i).
+  comb_lin (fun i => sigma fe i v) theta.
+  (* was  \big[plus%R/zero]_(i < ndof fe) scal (sigma fe i v) (theta i). *)
 
 Lemma interp_op_local_is_poly: forall v,
       (P_approx fe) (interp_op_local v).
 Proof.
 intros v; unfold interp_op_local.
-edestruct (is_basis_is_generator (P_approx fe) (ndof fe) my_theta).
-apply my_theta_is_basis.
+edestruct (is_basis_is_generator (P_approx fe) (ndof fe) theta).
+apply theta_is_basis.
 apply H0.
 exists (fun i => sigma fe i v); easy.
 Qed.
@@ -254,7 +255,7 @@ admit.
 intros x l.
 Admitted.
 
-Lemma interp_op_local_my_theta : forall i, interp_op_local (my_theta i) = my_theta i.
+Lemma interp_op_local_theta : forall i, interp_op_local (theta i) = theta i.
 Proof.
 Admitted.
 
@@ -263,14 +264,14 @@ Lemma interp_op_local_proj : forall p,
   (P_approx fe) p -> interp_op_local p = p.
 Proof.
 intros p Hp.
-destruct (is_basis_is_generator (P_approx fe) (ndof fe) my_theta) as (H0,H1).
-apply my_theta_is_basis.
+destruct (is_basis_is_generator (P_approx fe) (ndof fe) theta) as (H0,H1).
+apply theta_is_basis.
 destruct (H1 p) as (H2,_).
 destruct (H2 Hp) as [L HL].
 rewrite HL.
 rewrite bigop_plus_linear.
 apply bigop_ext.
-intros; rewrite interp_op_local_my_theta; easy.
+intros; rewrite interp_op_local_theta; easy.
 apply interp_op_local_is_linear_mapping.
 Qed.
 
@@ -298,7 +299,7 @@ unfold scal; simpl.
 unfold mult; simpl.
 rewrite Rmult_comm.
 f_equal.
-apply my_theta_is_shape_fun_local.
+apply theta_correct.
 Qed.
 
 End FE_Local_Def2.