Library Algebra.Finite_dim.Finite_dim_MS_duality_R
This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
Support for duality in finite-dimensional module spaces on the ring of real
numbers.
Let E : ModuleSpace R_Ring.
Let PE : E → Prop.
Let B : 'E^n and B' : '(E → R)^n.
Let HPE : fin_dim PE and PE_ms := sub_ModuleSpace (fin_dim_cms HPE)
(where fin_dim_cms HPE is a proof that compatible_ms PE,
i.e. that PE is closed under linear operations).
This module may be used through the import of
Algebra.Finite_dim.Finite_dim_MS, Algebra.Finite_dim.Finite_dim,
Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.
Brief description
Description
- dual_basis (HB : basis PE B) : '(PE_ms → R)^n is the dual basis of B.
- predual_basis (HB' : bijS PE fullset (gather B')) : 'E^n is the predual basis of B', i.e. such that B' is its dual basis.
Used logic axioms
- ex_EX, an alias for constructive_indefinite_description.
Usage
From Requisite Require Import stdlib_wR ssr_wMC.
From Coquelicot Require Import Hierarchy.
Close Scope R_scope.
From Subsets Require Import Subsets_wDep.
From Algebra Require Import Hierarchy_compl Monoid Group Ring ModuleSpace.
From Algebra Require Import matrix Finite_dim_MS_def Finite_dim_MS_lin_gen.
From Algebra Require Import Finite_dim_MS_lin_indep Finite_dim_MS_basis .
From Algebra Require Import Finite_dim_MS_lin_indep_R Finite_dim_MS_basis_R.
Local Open Scope R_scope.
Local Open Scope Monoid_scope.
Local Open Scope Group_scope.
Local Open Scope Ring_scope.
Local Open Scope ModuleSpace_scope.
Section Dual_family.
Context {E : ModuleSpace R_Ring}.
Context {n : nat}.
Variable B : 'E^n.
Variable B' : '(E → R)^n.
Definition dualF : Prop := ∀ i j, B' i (B j) = kronR i j.
Lemma dualF_lin_indep : dualF → lin_indep B → lin_indep B'.
Proof.
intros H HB L HL; apply extF; intros j.
rewrite zeroF -(fct_zero_eq (B j)).
rewrite -(lc_kron_l_in_r _ L) lc_comm_R.
rewrite -(fun_ext_rev HL (B j)) fct_lc_r_eq.
apply lc_ext_r; intros i; rewrite H; apply kron_sym.
Qed.
Lemma dualF_lin_indep_rev :
(∀ i, lin_map (B' i)) → dualF → lin_indep B' → lin_indep B.
Proof.
intros H0 H HB' L HL; apply extF; intros i.
rewrite zeroF -(lm_zero (H0 i))//.
rewrite -(f_equal (B' i) HL) f_lc_compat_lm//.
rewrite -lc_kron_l_in_r lc_comm_R.
apply lc_ext_l; intros j; rewrite mapF_correct H; easy.
Qed.
Lemma dualF_basis_equiv :
(∀ i, lin_map (B' i)) → dualF →
basis (lin_span B) B ↔ basis (lin_span B') B'.
Proof.
intros H0 H; split; intros [H1 H2]; split;
[| apply (dualF_lin_indep H) | | apply (dualF_lin_indep_rev H0 H)]; easy.
Qed.
End Dual_family.
Section Dual_basis_Def.
Context {E : ModuleSpace R_Ring}.
Context {PE : E → Prop}.
Hypothesis HPE : fin_dim PE.
Let HPE1 := fin_dim_cms HPE.
Let PE_ms := sub_ModuleSpace HPE1.
Context {n : nat}.
Context {B : 'E^n}.
Hypothesis HB : basis PE 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 (lin_span_EX _ _ Hx) i.
End Dual_basis_Def.
Section Dual_basis_Facts0.
Context {E : ModuleSpace R_Ring}.
Context {PE : E → Prop}.
Context {HPE : fin_dim PE}.
Let HPE1 := fin_dim_cms HPE.
Let PE_ms := sub_ModuleSpace HPE1.
Context {n : nat}.
Context {B : 'E^n}.
Context {HB : basis PE B}.
Lemma dual_basis_correct :
∀ {x : PE_ms} L,
val x = lin_comb L B → ∀ i, dual_basis HPE HB i x = L i.
Proof.
intros x L H i; unfold dual_basis;
destruct (lin_span_EX _ _) as [L' HL']; simpl; move: i; apply fun_ext_rev.
apply (lin_indep_uniq_decomp (proj2 HB)); rewrite -HL'; easy.
Qed.
End Dual_basis_Facts0.
Section Dual_basis_Facts1.
Context {E : ModuleSpace R_Ring}.
Context {PE : E → Prop}.
Context {HPE : fin_dim PE}.
Let HPE1 := fin_dim_cms HPE.
Let PE_ms := sub_ModuleSpace HPE1.
Context {n : nat}.
Context {B : 'E^n}.
Context {HB : basis PE B}.
Lemma dual_basis_lm : ∀ i, lin_map (dual_basis HPE HB i).
Proof.
pose (HB1 := proj1 HB); intros i; split; [intros x y | intros l x].
destruct (lin_span_EX B (val x)) as [Lx HLx]; [rewrite -HB1; apply x |].
destruct (lin_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 lc_plus_l -HLx -HLy]; easy.
destruct (lin_span_EX B (val x)) as [Lx HLx]; [rewrite -HB1; apply x |].
rewrite (dual_basis_correct _ HLx) (dual_basis_correct (scal l Lx));
[| rewrite lc_scal_l -HLx]; easy.
Qed.
Let HBa := lin_gen_inclF (proj1 HB).
Let B_ms := fun i ⇒ (mk_sub (HBa i) : PE_ms).
Lemma dual_basis_dualF : dualF B_ms (dual_basis HPE HB).
Proof.
intros i j; rewrite (dual_basis_correct (kronR^~ j));
[| rewrite lc_kron_l_in_l]; easy.
Qed.
Lemma dual_basis_decomp_compat :
∀ {B1 : 'E^n} (HB1 : basis PE B1) M M1,
(∀ i, B1 i = lin_comb (M i) B) → M1 ** flipT M = II →
∀ i, dual_basis HPE HB1 i = lin_comb (M1 i) (dual_basis HPE HB).
Proof.
intros B1 HB1 M M1 H1 HM i; apply fun_ext; intros x; fold HPE1 in x.
destruct (basis_ex_decomp HB1 (val x)) as [L1 HL1]; [apply x |].
rewrite (dual_basis_correct _ HL1).
rewrite (lc2_l_alt_sym H1) in HL1.
rewrite fct_lc_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.
rewrite mapF_correct; 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 : fin_dim PE.
Let HPE1 := fin_dim_cms HPE.
Let PE_ms := sub_ModuleSpace HPE1.
Context {n : nat}.
Context {B : 'E^n}.
Variable HB : basis PE B.
Let HBa := lin_gen_inclF (proj1 HB).
Let B_ms := fun i ⇒ (mk_sub (HBa i) : PE_ms).
Lemma dual_basis_decomp :
∀ {f : PE_ms → R}, lin_map f →
f = lin_comb (mapF f B_ms) (dual_basis HPE HB).
Proof.
pose (HB1 := proj1 HB); intros f Hf; apply fun_ext; intros x.
destruct (lin_span_EX B (val x)) as [L HL]; [rewrite -HB1; apply x |].
rewrite fct_lc_r_eq (fun_ext (dual_basis_correct _ HL)).
rewrite lc_comm_R -f_lc_compat_lm//; f_equal.
apply val_inj; rewrite val_lc; easy.
Qed.
End Dual_basis_Facts2.
Section Predual_basis_Def.
Context {E : ModuleSpace R_Ring}.
Context {PE : E → Prop}.
Context {n : nat}.
Context {B' : '(E → R)^n}.
Hypothesis HB' : bijS PE fullset (gather B').
Definition predual_basis : 'E^n.
Proof.
move: (choiceF (fun (j : 'I_n) x ⇒ PE x ∧
∀ i, B' i x = kronR i j)) ⇒ H.
apply ex_EX in H; [destruct H as [B HB]; apply B | clear H].
intros j; destruct HB' as [f [H1 [H2 [H3 H4]]]];
∃ (f (kronR^~ j)); split; [apply H2; easy |].
intros i; rewrite -(fun_ext_rev (H4 (kronR^~ j) (in_fullset _)) i); easy.
Defined.
End Predual_basis_Def.
Section Predual_basis_Facts0.
Context {E : ModuleSpace R_Ring}.
Context {PE : E → Prop}.
Context {n : nat}.
Context {B' : '(E → R)^n}.
Hypothesis HB' : bijS PE fullset (gather B').
Lemma predual_basis_in_sub : inclF (predual_basis HB') PE.
Proof. intro; unfold predual_basis; destruct (ex_EX _) as [B H]; apply H. Qed.
Lemma predual_basis_dualF : dualF (predual_basis HB') B'.
Proof.
move=>>; unfold predual_basis; destruct (ex_EX _) as [B HB]; apply HB.
Qed.
End Predual_basis_Facts0.
Section Predual_basis_Facts1.
Context {E : ModuleSpace R_Ring}.
Context {PE : E → Prop}.
Context {n : nat}.
Hypothesis HPE : has_dim PE n.
Context {B' : '(E → R)^n}.
Hypothesis HB'1 : ∀ i, lin_map (B' i).
Hypothesis HB' : bijS PE fullset (gather B').
Lemma predual_basis_basis : basis PE (predual_basis HB').
Proof.
apply lin_indep_basis; [easy | apply predual_basis_in_sub |].
apply (dualF_lin_indep_rev _ _ HB'1); [apply predual_basis_dualF |].
eapply (lin_indep_scatter _), bijS_surjS, HB'.
Qed.
End Predual_basis_Facts1.