Des preuves dans comb_lin + un peu sur is_basis

FEM/Finite_dim.v

@@ -50,6 +50,35 @@ Definition is_basis := fun B =>
   (forall i, PE (B i)) /\
   (forall x, PE x <-> exists! L : 'R^n, x = comb_lin L B).
 
+
+Lemma is_basis_has_zero : forall B, is_generator B ->
+    PE zero.
+Proof.
+intros B [H1 H2].
+apply H2.
+exists (fun _ => zero).
+apply sym_eq, comb_lin_0_l; easy.
+Qed.
+
+
+Lemma is_basis_is_scal_stable : forall B lambda x, 
+   is_generator B -> PE x -> PE (scal lambda x).
+Proof.
+  intros  B la x [H1 H2] Hx.
+  case (Req_dec la 0); intros Hla.
+  rewrite Hla; replace 0 with (@zero R_Ring) by easy.
+  rewrite scal_zero_l.
+  apply is_basis_has_zero with B; easy.
+  apply H2.
+  destruct (proj1 (H2 x) Hx) as [L HL].
+  exists (fun i => (la * (L i))).
+  rewrite HL, comb_lin_scal.
+  apply comb_lin_ext_l; easy.
+Qed.
+
+
+
+
 Lemma is_basis_is_generator : forall (B:'E^n), 
    is_basis B -> is_generator B.
 Proof.
@@ -86,6 +115,7 @@ Variable PE : E -> Prop.
 Definition compatible_finite := fun n =>
     exists B : 'E^n, is_basis PE B.
 
+
 Lemma is_free_finite_is_basis : forall n, 
   compatible_finite n -> forall B : 'E^n,
   forall i, PE (B i) -> is_free B -> is_basis PE B.

FEM/comb_lin.v

-From Coq Require Import Lia Reals Lra.
+From Coq Require Import Lia Reals Lra FunctionalExtensionality.
+
 
 From Coquelicot Require Import Coquelicot.
 
@@ -103,6 +104,22 @@ Section Comb_lin1.
 Context {E : ModuleSpace R_Ring}.
 Context {n : nat}.
 
+
+Lemma bigop_zero: forall (x : 'E^n),
+    (forall i: 'I_n, x i = zero) ->
+   \big[plus/zero]_(i < n) x i = zero.
+Proof.
+intros x H.
+apply trans_eq with (\big[plus/zero]_(i < n) zero).
+f_equal.
+apply functional_extensionality.
+intros j; rewrite H; easy.
+rewrite big_const_ord.
+clear; induction n; simpl; try easy.
+rewrite IHn0 plus_zero_l; easy.
+Qed.
+
+
 Definition comb_lin :=
   fun (L : 'R^n) (B : 'E^n) => \big[plus/zero]_(i < n) scal (L i) (B i).
 
@@ -124,25 +141,43 @@ Lemma comb_lin_ext :
     comb_lin L B = comb_lin M C.
 Proof.
 intros L M B C H.
-Admitted.
+unfold comb_lin.
+f_equal.
+apply functional_extensionality.
+intros i; rewrite H; easy.
+Qed.
 
 Lemma comb_lin_0_l : forall (L : 'R^n) B, L = zero -> comb_lin L B = zero.
 Proof.
 intros L B HL; rewrite HL.
-unfold comb_lin.
-
-Admitted.
+unfold comb_lin; apply bigop_zero.
+intros i; simpl; apply scal_zero_l.
+Qed.
 
 Lemma comb_lin_0_r : forall L (B : 'E^n), B = zero -> comb_lin L B = zero.
 Proof.
-intros L B HB; rewrite HB.
-unfold comb_lin.
-apply trans_eq with (\big[plus/zero]_(i < n) zero).
-apply bigop_ext.
-intros; apply scal_zero_r.
-rewrite big_const_ord.
+intros L B HL; rewrite HL.
+unfold comb_lin; apply bigop_zero.
+intros i; simpl; apply scal_zero_r.
+Qed.
+
+Lemma comb_lin_scal : forall x L B,
+   scal x (comb_lin L B) = comb_lin (scal x L) B.
+Proof.
+intros x L B; unfold comb_lin.
+induction n.
+rewrite 2!big_ord0.
+apply scal_zero_r.
+rewrite 2!big_ord_recl.
+specialize (IHn0 (fun i => (L (lift ord0 i))) 
+     (fun i => (B (lift ord0 i)))).
+simpl in IHn0.
+rewrite scal_distr_l.
+rewrite IHn0.
+f_equal; try easy.
+rewrite scal_assoc; easy.
+Qed.
 
-Admitted.
 
 End Comb_lin1.