Define comb_lin and state properties.

File should be renamed comb_lin.v.

FEM/bigop_compl.v

@@ -9,11 +9,15 @@ From mathcomp Require Import seq path ssralg div tuple finfun.
 Add LoadPath "../LM" as LM.
 From LM Require Import linear_map.
 
+
+(* TODO: rename this file as Comb_lin.v. *)
+
 Section bigop_compl.
 
-Lemma bigop_ext : forall {A : Type} (idx : A) (op : A -> A -> A) n F G,
-  (forall i : 'I_n, F i = G i) ->
-  \big[op/idx]_(i < n) F i = \big[op/idx]_(i < n) G i.
+Lemma bigop_ext :
+  forall {A : Type} (idx : A) (op : A -> A -> A) n (F G : 'I_n -> A),
+    (forall i : 'I_n, F i = G i) ->
+    \big[op/idx]_(i < n) F i = \big[op/idx]_(i < n) G i.
 Proof.
 Admitted.
 
@@ -52,6 +56,7 @@ Admitted.
 
 End bigop_compl.
 
+
 Section Linearity.
 
 Context {E F : ModuleSpace R_Ring}.
@@ -89,4 +94,124 @@ rewrite sum_pn_Sn; easy.
 Qed.
 *)
 End Linearity.
+
+
+Notation "''' E ^ n" := ('I_n -> E)
+  (at level 8, E at level 2, n at level 2, format "''' E ^ n").
+
+
+Section Comb_lin1.
+
+Context {E : ModuleSpace R_Ring}.
+Context {n : nat}.
+
+Definition comb_lin :=
+  fun (L : 'R^n) (B : 'E^n) => \big[plus/zero]_(i < n) scal (L i) (B i).
+
+Lemma comb_lin_ext_l :
+  forall (L M : 'R^n) B, L = M -> comb_lin L B = comb_lin M B.
+Proof.
+intros L M B H; rewrite H; easy.
+Qed.
+
+Lemma comb_lin_ext_r :
+  forall L (B C : 'E^n), B = C -> comb_lin L B = comb_lin L C.
+Proof.
+intros L B C H; rewrite H; easy.
+Qed.
+
+Lemma comb_lin_ext :
+  forall (L M : 'R^n) (B C : 'E^n),
+    (forall i, scal (L i) (B i) = scal (M i) (C i)) ->
+    comb_lin L B = comb_lin M C.
+Proof.
+intros L M B C H.
+Admitted.
+
+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.
+
+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.
+
+Admitted.
+
+End Comb_lin1.
+
+
+Section Comb_lin2.
+
+Context {E F : ModuleSpace R_Ring}.
+Context {n : nat}.
+
+Lemma comb_lin_fun_compat :
+  forall (L : 'R^n) (f : '(E -> F)^n) x,
+    (comb_lin L f) x = comb_lin L (fun i => f i x).
+Proof.
+Admitted.
+
+Lemma linear_mapping_comb_lin_compat :
+  forall (f : E -> F) (L : 'R^n) (B : 'E^n),
+    is_linear_mapping f ->
+    f (comb_lin L B) = comb_lin L (fun i => f (B i)).
+Proof.
+Admitted.
+
+Lemma comb_lin_linear_mapping_compat :
+  forall (L : 'R^n) (f : '(E -> F)^n),
+    (forall i, is_linear_mapping (f i)) ->
+    is_linear_mapping (comb_lin L f).
+Proof.
+Admitted.
+
+End Comb_lin2.
+
+
+Section Comb_lin3.
+
+Context {E F : ModuleSpace R_Ring}.
+Context {n p : nat}.
+
+Lemma comb_lin_comb_lin :
+  forall (L : 'R^n) (f : '(E -> F)^n) (M : 'R^p) (B : 'E^p),
+    (forall i, is_linear_mapping (f i)) ->
+    (comb_lin L f) (comb_lin M B) =
+    comb_lin M (fun i : 'I_p => comb_lin L f (B i)).
+Proof.
+intros L f M B Hf.
+rewrite linear_mapping_comb_lin_compat; try easy.
+apply comb_lin_linear_mapping_compat; easy.
+Qed.
+
+End Comb_lin3.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+