ModuleSpace_R_compl:

Make some arguments implicit.

Finite_dim_R:
Add many local definitions to ease reading.
Make some arguments implicit.
Rename dual_is_linear_mapping -> dual_lin_map.
Add def bidual_basis, bidual, bidual_nat_isom, predual_basis.
Add and prove dual_has_dim, dual_lin_map_{rev,equiv}.
WIP: bidual_pt_eval, bidual_nat_isom_{correct,lin_map,inj,bij},
     predual_basis_{dualF,is_basis,correct}.

FEM/Algebra/Finite_dim_R.v

@@ -1481,6 +1481,7 @@ Context {E : ModuleSpace R_Ring}.
 Context {PE : E -> Prop}.
 Hypothesis HPE : is_finite_dim PE.
 Let HPE1 := is_finite_dim_compatible_ms HPE.
+Let PE_ms := sub_ms HPE1.
 
 Context {n : nat}.
 Context {B : 'E^n}.
@@ -1488,34 +1489,50 @@ Hypothesis HB : is_basis PE B.
 
 (* Note that 'eq_sym (proj1 HB)' is a proof of 'span B = PE'.
  Thus, 'Hx' is a proof of 'span B (val x)',
- and 'proj1_sig (span_EX _ _ (...))' is an 'L' such that 'val x = comb_lin L B'. *)
-Definition dual_basis : '(sub_ms HPE1 -> R)^n :=
+ and 'proj1_sig (span_EX _ _ (...))' is the 'L' such that 'val x = comb_lin L B'. *)
+Definition dual_basis : '(PE_ms -> R)^n :=
   fun i x =>
     let Hx := eq_ind_r (@^~ (val x)) (in_sub x) (eq_sym (proj1 HB)) in
     proj1_sig (span_EX _ _ Hx) i.
 
+End Dual_basis_Def.
+
+
+Section Dual_basis_Facts0.
+
+Context {E : ModuleSpace R_Ring}.
+Context {PE : E -> Prop}.
+Context {HPE : is_finite_dim PE}.
+Let HPE1 := is_finite_dim_compatible_ms HPE.
+Let PE_ms := sub_ms HPE1.
+
+Context {n : nat}.
+Context {B : 'E^n}.
+Context {HB : is_basis PE B}.
+
 Lemma dual_basis_correct :
-  forall {x : sub_ms HPE1} L,
-    val x = comb_lin L B -> forall i, dual_basis i x = L i.
+  forall {x : PE_ms} L,
+    val x = comb_lin L B -> forall i, dual_basis HPE HB i x = L i.
 Proof.
 intros x L H i; unfold dual_basis;
     destruct (span_EX _ _) as [L' HL']; simpl; move: i; apply fun_ext_rev.
 apply (is_free_uniq_decomp (proj2 HB)); rewrite -HL'; easy.
 Qed.
 
-End Dual_basis_Def.
+End Dual_basis_Facts0.
 
 
-Section Dual_basis_Facts.
+Section Dual_basis_Facts1.
 
 Context {E : ModuleSpace R_Ring}.
 Context {PE : E -> Prop}.
-Hypothesis HPE : is_finite_dim PE.
+Context {HPE : is_finite_dim PE}.
 Let HPE1 := is_finite_dim_compatible_ms HPE.
+Let PE_ms := sub_ms HPE1.
 
 Context {n : nat}.
 Context {B : 'E^n}.
-Hypothesis HB : is_basis PE B.
+Context {HB : is_basis PE B}.
 
 Lemma dual_basis_lin_map : forall i, is_linear_mapping (dual_basis HPE HB i).
 Proof.
@@ -1523,21 +1540,21 @@ pose (HB1 := proj1 HB); intros i; split; [intros x y | intros x l].
 (* *)
 destruct (span_EX B (val x)) as [Lx HLx]; [rewrite -HB1; apply x |].
 destruct (span_EX B (val y)) as [Ly HLy]; [rewrite -HB1; apply y |].
-rewrite (dual_basis_correct _ _ _ HLx) (dual_basis_correct _ _ _ HLy)
-    (dual_basis_correct _ _ (Lx + Ly));
+rewrite (dual_basis_correct _ HLx) (dual_basis_correct _ HLy)
+    (dual_basis_correct (Lx + Ly));
     [| rewrite comb_lin_plus_l -HLx -HLy]; easy.
 (* *)
 destruct (span_EX B (val x)) as [Lx HLx]; [rewrite -HB1; apply x |].
-rewrite (dual_basis_correct _ _ _ HLx) (dual_basis_correct _ _ (scal l Lx));
+rewrite (dual_basis_correct _ HLx) (dual_basis_correct (scal l Lx));
     [| rewrite comb_lin_scal_l -HLx]; easy.
 Qed.
 
 Let HBa := is_generator_inclF (proj1 HB).
-Let B_sub := fun i => (mk_sub_ms (HBa i) : sub_ms HPE1).
+Let B_ms := fun i => (mk_sub_ms (HBa i) : PE_ms).
 
-Lemma dual_basis_dualF : dualF B_sub (dual_basis HPE HB).
+Lemma dual_basis_dualF : dualF B_ms (dual_basis HPE HB).
 Proof.
-intros i j; rewrite (dual_basis_correct _ _ (kronecker^~ j));
+intros i j; rewrite (dual_basis_correct (kronecker^~ j));
     [| rewrite comb_lin_kronecker_in_l]; easy.
 Qed.
 
@@ -1548,26 +1565,43 @@ Lemma dual_basis_decomp_compat :
 Proof.
 intros B1 HB1 M M1 H1 HM i; apply fun_ext; intros x; fold HPE1 in x.
 destruct (is_basis_ex_decomp HB1 (val x)) as [L1 HL1]; [apply x |].
-rewrite (dual_basis_correct _ _ _ HL1).
-rewrite (comb_lin2_alt' _ _ _ _ H1) in HL1.
-rewrite fct_comb_lin_r_eq (fun_ext _ _ (dual_basis_correct _ _ _ HL1))
+rewrite (dual_basis_correct _ HL1).
+rewrite (comb_lin2_alt' H1) in HL1.
+rewrite fct_comb_lin_r_eq (fun_ext _ _ (dual_basis_correct _ HL1))
     -col1T_correct -(mx_mult_one_l (col1T L1)) -HM -mx_mult_assoc mx_mult_eq.
 f_equal; apply extF; intros j; unfold flipT; rewrite mx_mult_eq; unfold flipT.
 f_equal; apply extF; intros k; apply col1T_correct.
 Qed.
 
+End Dual_basis_Facts1.
+
+
+Section Dual_basis_Facts2.
+
+Context {E : ModuleSpace R_Ring}.
+Context {PE : E -> Prop}.
+Variable HPE : is_finite_dim PE.
+Let HPE1 := is_finite_dim_compatible_ms HPE.
+Let PE_ms := sub_ms HPE1.
+
+Context {n : nat}.
+Context {B : 'E^n}.
+Variable HB : is_basis PE B.
+Let HBa := is_generator_inclF (proj1 HB).
+Let B_ms := fun i => (mk_sub_ms (HBa i) : PE_ms).
+
 Lemma dual_basis_decomp :
-  forall (f : sub_ms HPE1 -> R), is_linear_mapping f ->
-    f = comb_lin (mapF f B_sub) (dual_basis HPE HB).
+  forall {f : PE_ms -> R}, is_linear_mapping f ->
+    f = comb_lin (mapF f B_ms) (dual_basis HPE HB).
 Proof.
 pose (HB1 := proj1 HB); intros f Hf; apply fun_ext; intros x.
 destruct (span_EX B (val x)) as [L HL]; [rewrite -HB1; apply x |].
-rewrite fct_comb_lin_r_eq (fun_ext _ _ (dual_basis_correct _ _ _ HL)).
+rewrite fct_comb_lin_r_eq (fun_ext _ _ (dual_basis_correct _ HL)).
 rewrite comb_lin_comm_R -linear_mapping_comb_lin_compat//; f_equal.
 apply val_inj; rewrite val_comb_lin; easy.
 Qed.
 
-End Dual_basis_Facts.
+End Dual_basis_Facts2.
 
 
 Section Dual_subspace.
@@ -1576,18 +1610,13 @@ Context {E : ModuleSpace R_Ring}.
 Context {PE : E -> Prop}.
 Hypothesis HPE : is_finite_dim PE.
 Let HPE1 := is_finite_dim_compatible_ms HPE.
+Let PE_ms := sub_ms HPE1.
 
-Definition dual : (sub_ms HPE1 -> R) -> Prop :=
+Definition dual : (PE_ms -> R) -> Prop :=
   let HPE0 := ex_EX _ (is_finite_dim_has_dim HPE) in
   let HB := proj2_sig (has_dim_EX PE (proj1_sig HPE0) (proj2_sig HPE0)) in
   span (dual_basis HPE HB).
 
-Lemma dual_is_linear_mapping : forall f, dual f -> is_linear_mapping f.
-Proof.
-move=>> [L]; apply comb_lin_linear_mapping_compat_r; intro;
-    apply dual_basis_lin_map.
-Qed.
-
 Lemma dual_uniq :
   forall {n} {B : 'E^n} (HB : is_basis PE B), dual = span (dual_basis HPE HB).
 Proof.
@@ -1601,12 +1630,12 @@ subst; apply span_ext; fold HPE0 n0; intros i; fold Hn0 HB0; apply span_ex.
 (* *)
 destruct (transition_matrix_ex HB HB0) as [M [HM [M1 [_ HM1]]]].
 unfold mult, one in HM1; simpl in HM1.
-exists (flipT M1 i); apply (dual_basis_decomp_compat _ _ _ M _ HM).
+exists (flipT M1 i); apply (dual_basis_decomp_compat _ M _ HM).
 rewrite mx_mult_flipT HM1; apply mx_one_sym.
 (* *)
 destruct (transition_matrix_ex HB0 HB) as [M [HM [M1 [_ HM1]]]].
 unfold mult, one in HM1; simpl in HM1.
-exists (flipT M1 i); apply (dual_basis_decomp_compat _ _ _ M _ HM).
+exists (flipT M1 i); apply (dual_basis_decomp_compat _ M _ HM).
 rewrite mx_mult_flipT HM1; apply mx_one_sym.
 Qed.
 
@@ -1615,21 +1644,39 @@ Lemma dual_basis_is_basis :
     is_basis dual (dual_basis HPE HB).
 Proof.
 intros n B HB; pose (HB1 := proj1 HB).
-pose (B_sub := fun i => (mk_sub_ms (is_generator_inclF HB1 i) : sub_ms HPE1)).
+pose (B_ms := fun i => (mk_sub_ms (is_generator_inclF HB1 i) : sub_ms HPE1)).
 rewrite (dual_uniq HB).
-apply (dualF_is_basis_equiv B_sub (dual_basis HPE HB));
+apply (dualF_is_basis_equiv B_ms (dual_basis HPE HB));
     [apply dual_basis_lin_map | apply dual_basis_dualF |].
 apply is_basis_span_equiv.
-intros L HL; apply HB, trans_eq with (val (comb_lin L B_sub));
+intros L HL; apply HB, trans_eq with (val (comb_lin L B_ms));
     [rewrite val_comb_lin | rewrite HL]; easy.
 Qed.
 
+Lemma dual_has_dim : forall {n} {B : 'E^n}, is_basis PE B -> has_dim dual n.
+Proof. move=>> HB; apply (Dim _ _ _ (dual_basis_is_basis HB)). Qed.
+
 Lemma dual_is_finite_dim : is_finite_dim dual.
 Proof.
 move: (is_finite_dim_has_dim HPE) => [n [B HB]].
-apply (has_dim_is_finite_dim (Dim _ _ _ (dual_basis_is_basis HB))).
+apply (has_dim_is_finite_dim (dual_has_dim HB)).
 Qed.
 
+Lemma dual_lin_map : forall f, dual f -> is_linear_mapping f.
+Proof.
+move=>> [L]; apply comb_lin_linear_mapping_compat_r; intro;
+    apply dual_basis_lin_map.
+Qed.
+
+Lemma dual_lin_map_rev : forall f, is_linear_mapping f -> dual f.
+Proof.
+intros f Hf; destruct (is_finite_dim_has_dim HPE) as [n [B HB]].
+rewrite (dual_uniq HB) (dual_basis_decomp HPE HB Hf); easy.
+Qed.
+
+Lemma dual_lin_map_equiv : forall f, dual f <-> is_linear_mapping f.
+Proof. intros; split; [apply dual_lin_map | apply dual_lin_map_rev]. Qed.
+
 End Dual_subspace.
 
 
@@ -1639,38 +1686,111 @@ Context {E : ModuleSpace R_Ring}.
 Context {PE : E -> Prop}.
 Hypothesis HPE : is_finite_dim PE.
 Let HPE1 := is_finite_dim_compatible_ms HPE.
+Let PE_ms := sub_ms HPE1.
+
+Let PE' := dual HPE.
+Let HPE' := dual_is_finite_dim HPE.
+Let HPE'1 := is_finite_dim_compatible_ms HPE'.
+Let PE'_ms := sub_ms HPE'1.
 
 Context {n : nat}.
 Context {B : 'E^n}.
 Hypothesis HB : is_basis PE B.
 
+Definition bidual_basis : '(PE'_ms -> R)^n :=
+  dual_basis HPE' (dual_basis_is_basis HPE HB).
+
+End Bidual_basis.
+
+
+Section Bidual_subspace.
+
+Context {E : ModuleSpace R_Ring}.
+Context {PE : E -> Prop}.
+Hypothesis HPE : is_finite_dim PE.
+Let HPE1 := is_finite_dim_compatible_ms HPE.
+Let PE_ms := sub_ms HPE1.
+
+Let PE' := dual HPE.
 Let HPE' := dual_is_finite_dim HPE.
 Let HPE'1 := is_finite_dim_compatible_ms HPE'.
+Let PE'_ms := sub_ms HPE'1.
 
-Definition bidual_basis : '(sub_ms HPE'1 -> R)^n :=
-  dual_basis HPE' (dual_basis_is_basis HPE HB).
+Let PE'' := dual HPE'.
+Let HPE'' := dual_is_finite_dim HPE'.
+Let HPE''1 := is_finite_dim_compatible_ms HPE''.
+Let PE''_ms := sub_ms HPE''1.
 
-End Bidual_basis.
+Definition bidual : (PE'_ms -> R) -> Prop := PE''.
+
+Lemma bidual_pt_eval : forall (x : PE_ms), bidual (fun f => val f x).
+Proof.
+Admitted.
+
+(* This is the natural isomorphism between a subspace and its bidual. *)
+Definition bidual_nat_isom (x : PE_ms) : PE''_ms :=
+  mk_sub_ms (bidual_pt_eval x).
+
+Lemma bidual_nat_isom_correct :
+  forall (x : PE_ms) (f : PE'_ms), val (bidual_nat_isom x) f = val f x.
+Proof.
+Admitted.
+
+Lemma bidual_nat_isom_lin_map : is_linear_mapping bidual_nat_isom.
+Proof.
+Admitted.
+
+Lemma bidual_nat_isom_inj : injective bidual_nat_isom.
+Proof.
+Admitted.
+
+Lemma bidual_nat_isom_bij : bijective bidual_nat_isom.
+Proof.
+Admitted.
+
+End Bidual_subspace.
 
 
 Section Predual_basis.
 
 Context {E : ModuleSpace R_Ring}.
-Context {PE' : (E -> R) -> Prop}.
-Context {n : nat}.
+Context {PE : E -> Prop}.
+Hypothesis HPE : is_finite_dim PE.
+Let HPE1 := is_finite_dim_compatible_ms HPE.
+Let PE_ms := sub_ms HPE1.
 
-Variable B' : '(E -> R)^n.
+Let PE' := dual HPE.
+Let HPE' := dual_is_finite_dim HPE.
+Let HPE'1 := is_finite_dim_compatible_ms HPE'.
+Let PE'_ms := sub_ms HPE'1.
+
+Let PE'' := dual HPE'.
+Let HPE'' := dual_is_finite_dim HPE'.
+Let HPE''1 := is_finite_dim_compatible_ms HPE''.
+Let PE''_ms := sub_ms HPE''1.
+
+Context {n : nat}.
+Variable B' : '(PE_ms -> R)^n.
 Hypothesis HB' : is_basis PE' B'.
+Let B'' := dual_basis HPE' HB'.
+Let HB'' := dual_basis_is_basis HPE' HB'.
 
-Let HPE' := is_basis_compatible_ms _ HB'.
+Definition predual_basis (i : 'I_n) : E :=
+  val (f_inv (bidual_nat_isom_bij HPE)
+    (mk_sub_ms (is_basis_inclF HB'' i))).
 
 (*
-Definition predual_basis (*: '(sub_ms HPE -> R)^n*) :=
-  fun j x =>
-    let Hx := eq_ind_r (@^~ (val x)) (in_sub x) (eq_sym (proj1 HB)) in
-    proj1_sig (span_EX _ _ Hx) i.
+Lemma predual_basis_dualF : dualF predual_basis (fun i => ...).
 *)
 
+Lemma predual_basis_is_basis : is_basis PE predual_basis.
+Proof.
+Admitted.
+
+Lemma predual_basis_correct : dual_basis HPE predual_basis_is_basis = B'.
+Proof.
+Admitted.
+
 End Predual_basis.
 
 

FEM/Algebra/ModuleSpace_R_compl.v

@@ -219,7 +219,7 @@ Qed.
 
 (* TODO FC (22/02/2024): rename. *)
 Lemma comb_lin2_alt' :
-  forall {n1 n2} L1 (B1 : 'E^n1) M12 (B2 : 'E^n2),
+  forall {n1 n2} {L1} {B1 : 'E^n1} {M12} {B2 : 'E^n2},
     (forall i1, B1 i1 = comb_lin (M12 i1) B2) ->
     comb_lin L1 B1 = comb_lin (fun i2 => comb_lin (M12^~ i2) L1) B2.
 Proof.