State all results for the module space E (ie with scal and not mult)

FEM/kronecker.v

@@ -11,8 +11,14 @@ From mathcomp Require Import seq path.
 
 Add LoadPath "../LM" as LM.
 
+Add LoadPath "../Lebesgue" as Lebesgue.
+
 Require Import sum_pn bigop_compl.
 
+Notation "''' E ^ n" := ('I_n -> E)
+  (at level 8, E at level 2, n at level 2, format "''' E ^ n").
+
+
 Section kronecker.
 (* on peut le définir dans un anneau générique K *)
 
@@ -82,18 +88,25 @@ Qed.
 
 End kronecker.
 
-Section kronecker_sum_pn.
+Section kronecker_bigop.
 
 Context {E : ModuleSpace R_Ring}.
 
-Lemma kronecker_sum_scal_in_l : forall j n (a : nat -> E), 
-  (j < n)%nat -> sum_pn (fun i => scal (kronecker i j) (a i)) n = a j.
+Lemma kronecker_bigop_scal_in_l : forall n (j : 'I_n) (a : 'E^n),
+  (* (j < n)%nat -> *)
+  \big[plus/zero]_(i < n) scal (kronecker i j) (a i) = a j.
 Proof.
-Admitted.
+intros n j a.
+induction n.
+erewrite <- big_pred0_eq.
+(*
+rewrite bigop_plus_0; easy.
+(* *)
+rewrite bigop_plus_Sn.
+case (lt_dec j n); intros Hn.*)
 
-Lemma kronecker_sum_mult_in_l : forall j n a, 
-  (j < n)%nat -> sum_pn (fun i => mult (a i) (kronecker i j)) n = a j.
-Proof.
+
+(* old try *)
 intros j n a H.
 induction n; try easy.
 (* *)
@@ -124,17 +137,11 @@ case (eq_nat_dec i j); try lia.
 intro; erewrite Rmult_0_r; easy.
 Admitted.
 
-(*
-Lemma kronecker_sum_scal_in_l : forall j n a, 
-  (j < n)%nat -> 
-  sum_pn (fun i => mult (a i) (kronecker i j)) n = a j.
-Proof.
-Admitted.
-
-Lemma kronecker_sum_scal_out_l : forall j n a, 
+Lemma kronecker_bigop_scal_out_l : forall n j (a : 'E^n), 
   ~(j < n)%nat -> 
-  sum_pn (fun i => mult (a i) (kronecker i j)) n = zero.
+  \big[plus%R/zero]_(i < n) scal (kronecker i j) (a i) = zero.
 Proof.
+(* old try *)
 intros j n a H1.
 induction n; try easy.
 rewrite sum_pn_Sn.
@@ -157,10 +164,11 @@ intro; rewrite Rmult_0_r; easy.
 Qed.*)
 Admitted.
 
-Lemma kronecker_sum_scal_in_r : forall i n a, 
-  (i < n)%nat -> 
-  sum_pn (fun j => mult (a j) (kronecker i j)) n = a i.
+Lemma kronecker_bigop_scal_in_r : forall n (i : 'I_n) (a : 'E^n), 
+  (* (i < n)%nat -> *)  
+  \big[plus/zero]_(j < n) scal (kronecker i j) (a j) = a i.
 Proof.
+(* old try *)
 intros i n a H.
 replace (fun j : nat => mult (a j) (kronecker i j)) with
   (fun j : nat => mult (a j) (kronecker j i)).
@@ -169,9 +177,12 @@ apply functional_extensionality.
 intros j; f_equal; apply kronecker_sym.
 Qed.
 
-Lemma kronecker_sum_scal_out_r : forall i n a, 
-  ~(i < n)%nat -> sum_pn (fun j => mult (a j) (kronecker i j)) n = 0.
+
+Lemma kronecker_bigop_scal_out_r : forall i n (a : 'E^n), 
+  ~(i < n)%nat -> 
+  \big[plus%R/zero]_(j < n) scal (kronecker i j) (a j) = zero.
 Proof.
+(* old try *)
 intros i n a H1.
 replace (fun j : nat => mult (a j) (kronecker i j)) with
   (fun j : nat => mult (a j) (kronecker j i)).
@@ -180,90 +191,23 @@ apply functional_extensionality.
 intros j; f_equal; apply kronecker_sym.
 Qed.
 
-Lemma kronecker_sum_l : forall j n,
-  (j < n)%nat -> sum_pn (fun i => kronecker i j) n = 1.
+Lemma kronecker_bigop_l : forall n (j : 'I_n),
+  (*(j < n)%nat -> *)
+  \big[plus%R/zero]_(i < n) (kronecker i j) = 1.
 Proof.
+(* old try *)
 intros j n H1.
 replace (sum_pn (fun i : nat => kronecker i j) n) with
   (sum_pn (fun i : nat => mult (one) (kronecker i j)) n).
 apply kronecker_sum_scal_in_l; easy.
 f_equal; apply functional_extensionality.
 intros i; rewrite mult_one_l; easy.
-Qed.
 
-Lemma kronecker_sum_r : forall i n, 
-  (i < n)%nat -> sum_pn (fun j => kronecker i j) n = 1.
-Proof.
-intros i n H1.
-replace (fun j : nat => kronecker i j) with
-  (fun j : nat => kronecker j i).
-apply kronecker_sum_l; easy.
-apply functional_extensionality.
-intros j; apply kronecker_sym.
-Qed.
-
-Lemma kronecker_sum_prod : forall i j n, 
-  (i < n)%nat -> (j < n)%nat ->
-  sum_pn (fun k => mult (kronecker i k) (kronecker k j)) n = kronecker i j.
-Proof.
-intros i j n H1 H2.
-induction n; try easy.
-rewrite sum_pn_Sn.
-destruct (lt_dec i n) as [Hi | Hi], (lt_dec j n) as [Hj | Hj].
-rewrite IHn; try easy.
-replace (mult _ _) with (@zero R_Ring).
-apply plus_zero_r.
-rewrite kronecker_is_0; try lia.
-(*rewrite mult_zero_l. *)
-admit. 
-Admitted.
-*)
-
-End kronecker_sum_pn.
-
-
-Section kronecker_bigop.
-
-Context {E : ModuleSpace R_Ring}.
-
-(* TODO: state all results for the module space E (ie with scal and not mult). *)
-
-Lemma kronecker_bigop_scal_in_l : forall n (j : 'I_n) (a : 'I_n -> E),
-    \big[plus/zero]_(i < n) scal (kronecker i j) (a i) = a j.
-Proof.
-intros n j a.
-induction n.
-(*
-rewrite bigop_plus_0; easy.
-(* *)
-rewrite bigop_plus_Sn.
-case (lt_dec j n); intros Hn.*)
-Admitted.
-
-Lemma kronecker_bigop_scal_out_l : forall n j a, 
-  ~(j < n)%nat -> 
-  \big[plus%R/0]_(i < n) scal (a i) (kronecker i j) = zero.
-Proof.
-Admitted.
-
-Lemma kronecker_bigop_scal_in_r : forall n (i : 'I_n) (a : 'I_n -> E), 
-  \big[plus/zero]_(j < n) scal (kronecker i j) (a j) = a i.
-Proof.
-Admitted.
-
-Lemma kronecker_bigop_scal_out_r : forall i n a, 
-  ~(i < n)%nat -> 
-  \big[plus%R/0]_(j < n) mult (a j) (kronecker i j) = 0.
-Proof.
-Admitted.
-
-Lemma kronecker_bigop_l : forall n (j : 'I_n),
-  \big[plus%R/0]_(i < n) (kronecker i j) = 1.
-Proof.
 Admitted.
 
 Lemma kronecker_bigop_r : forall n (i : 'I_n),
-  \big[plus%R/0]_(j < n) (kronecker i j) = 1.
+  (*(i < n)%nat -> *)
+  \big[plus%R/zero]_(j < n) (kronecker i j) = 1.
 Proof.
 (*intros i n H1.
 replace (fun j : nat => kronecker i j) with
@@ -271,22 +215,33 @@ replace (fun j : nat => kronecker i j) with
 apply kronecker_sum_l; easy.
 apply functional_extensionality.
 intros j; apply kronecker_sym.*)
+
+(* old try *)
+intros i n H1.
+replace (fun j : nat => kronecker i j) with
+  (fun j : nat => kronecker j i).
+apply kronecker_sum_l; easy.
+apply functional_extensionality.
+intros j; apply kronecker_sym.
+Qed.
 Admitted.
 
-Lemma kronecker_bigop_prod : forall i j n, 
+Lemma kronecker_bigop_prod : forall n (i j : 'I_n), 
   (i < n)%nat -> (j < n)%nat ->
-  sum_pn (fun k => mult (kronecker i k) (kronecker k j)) n = kronecker i j.
+  \big[plus%R/zero]_(k < n) scal (kronecker i k) (kronecker k j) = kronecker i j.
 Proof.
 intros i j n H1 H2.
 induction n; try easy.
-rewrite sum_pn_Sn.
+(*rewrite sum_pn_Sn.
 destruct (lt_dec i n) as [Hi | Hi], (lt_dec j n) as [Hj | Hj].
 rewrite IHn; try easy.
 replace (mult _ _) with (@zero R_Ring).
 apply plus_zero_r.
-rewrite kronecker_is_0; try lia.
+rewrite kronecker_is_0; try lia.*)
 (*rewrite mult_zero_l. *)
 admit. 
+
 Admitted.
 
+
 End kronecker_bigop.
\ No newline at end of file