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.

Brief description

Support for duality in finite-dimensional module spaces on the ring of real numbers.

Description

Let E : ModuleSpace R_Ring. Let PE : E Prop. Let B : 'E^n and B' : '(E R)^n.
  • dualF B B' is the predicate stating that fun i j B' i (B j) is the Kronecker delta function.
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).

Used logic axioms

Usage

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.

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) xPE 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.