Library Algebra.Finite_dim.Finite_dim_MS_basis

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 basis finite families in module spaces.

Description

For results that are only valid when the ring of scalars is commutative, or being ordered, see Algebra.Finite_dim.Finite_dim_MS_basis_R where they are only stated in the case of the ring of real numbers R_Ring.

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 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 Finite_dim_MS_def Finite_dim_MS_lin_span.
From Algebra Require Import Finite_dim_MS_lin_gen Finite_dim_MS_lin_indep.

Local Open Scope Monoid_scope.
Local Open Scope Group_scope.
Local Open Scope Ring_scope.
Local Open Scope ModuleSpace_scope.

Section Basis_Facts1.

Properties of basis (from those of lin_gen and lin_indep).

Context {K : Ring}.
Hypothesis HK : nonzero_struct K.
Context {E : ModuleSpace K}.
Context {PE : E Prop}.

Lemma basis_lin_gen : {PE} {n} {B : 'E^n}, basis PE B lin_gen PE B.
Proof. move=>> [HB _]; easy. Qed.

Lemma basis_lin_indep : PE {n} {B : 'E^n}, basis PE B lin_indep B.
Proof. move=>> [_ HB]; easy. Qed.

Lemma basis_lin_span_equiv :
   {n} {B : 'E^n}, basis (lin_span B) B lin_indep B.
Proof.
assert (H : P Q : Prop, P P Q Q) by tauto.
intros; apply H; easy.
Qed.

Lemma basis_inclF : {n} {B : 'E^n}, basis PE B inclF B PE.
Proof. move=>> /basis_lin_gen; apply lin_gen_inclF. Qed.

Lemma basis_nonempty : {n} (B : 'E^n), basis PE B nonempty PE.
Proof. move=>> /basis_lin_gen; apply lin_gen_nonempty. Qed.

Lemma basis_nil : (B : 'E^0), basis zero_sub_struct B.
Proof. intros; split; [apply lin_gen_nil | apply lin_indep_nil]. Qed.

Lemma basis_without_zero : PE {n} {B : 'E^n}, basis PE B ¬ inF 0 B.
Proof. move=>> /basis_lin_indep; apply (lin_indep_without_zero HK). Qed.

Lemma basis_zero_rev : PE {n}, basis PE (0 : 'E^n) n = O.
Proof. move=>> /basis_lin_indep; apply (lin_indep_zero_rev HK). Qed.

Lemma basis_nil_or_nonzero :
   PE {n} (B : 'E^n), basis PE B n = O B 0.
Proof. move=>> /basis_lin_indep; apply (lin_indep_nil_or_nonzero HK). Qed.

Lemma basis_nonnil_or_zero :
   PE {n} (B : 'E^n), basis PE B (0 < n)%coq_nat B = 0.
Proof. move=>> /basis_lin_indep; apply lin_indep_nonnil_or_zero. Qed.

Lemma basis_nonzero :
   PE {n} (B : 'E^n), basis PE B PE zero_sub_struct B 0.
Proof. move=>> /basis_lin_gen; apply lin_gen_nonzero. Qed.

Lemma basis_S_nonzero : PE {n} (B : 'E^n.+1), basis PE B B 0.
Proof. move=>> /basis_lin_indep; apply (lin_indep_S_nonzero HK). Qed.

Lemma basis_nonzero_rev :
   PE {n} (B : 'E^n), basis PE B B 0 (0 < n)%coq_nat.
Proof. move=>> /basis_lin_indep; apply lin_indep_nonnil. Qed.

Lemma basis_nonzero_equiv :
   PE {n} (B : 'E^n), basis PE B B 0 (0 < n)%coq_nat.
Proof.
intros PE' n B HB; split; [apply (basis_nonzero_rev PE'); easy |].
intros; destruct n as [| n]; [| apply (basis_S_nonzero PE')]; easy.
Qed.

Lemma basis_nonnil :
   PE {n} (B : 'E^n), basis PE B B 0 (0 < n)%coq_nat.
Proof. move=>> /basis_lin_indep; apply lin_indep_nonnil. Qed.

Lemma basis_nonnil_nonzero_equiv :
   PE {n} (B : 'E^n), basis PE B (0 < n)%coq_nat B 0.
Proof.
move=>> /basis_lin_indep; apply (lin_indep_nonnil_nonzero_equiv HK).
Qed.

Lemma basis_nil_zero_equiv :
   PE {n} (B : 'E^n), basis PE B n = O B = 0.
Proof. move=>> /basis_lin_indep; apply (lin_indep_nil_zero_equiv HK). Qed.

Lemma basis_injF : PE {n} {B : 'E^n}, basis PE B injective B.
Proof. move=>> /basis_lin_indep; apply (lin_indep_injF HK). Qed.

Lemma basis_coupleF_sym :
   (x0 x1 : E), basis PE (coupleF x0 x1) basis PE (coupleF x1 x0).
Proof.
move=>> [/lin_gen_coupleF_sym H1 /lin_indep_coupleF_sym H2]; split; easy.
Qed.

Lemma basis_castF_equiv :
   {n1 n2} (H : n1 = n2) {B1 : 'E^n1},
    basis PE (castF H B1) basis PE B1.
Proof.
intros; unfold basis; rewrite lin_gen_castF_equiv lin_indep_castF_equiv; easy.
Qed.

Lemma basis_castF_compat :
   {n1 n2} (H : n1 = n2) {B1 : 'E^n1},
    basis PE B1 basis PE (castF H B1).
Proof. move=>>; apply basis_castF_equiv. Qed.

Lemma basis_castF_reg :
   {n1 n2} (H : n1 = n2) {B1 : 'E^n1},
    basis PE (castF H B1) basis PE B1.
Proof. move=>>; apply basis_castF_equiv. Qed.

Lemma basis_concatF_sym :
   {n1 n2} {B1 : 'E^n1} {B2 : 'E^n2},
    basis PE (concatF B1 B2) basis PE (concatF B2 B1).
Proof.
move=>> [/lin_gen_concatF_sym H1 /lin_indep_concatF_sym H2]; split; easy.
Qed.

Lemma basis_permutF :
   {n} {p} {B : 'E^n},
    bijective p basis PE B basis PE (permutF p B).
Proof.
assert (H : P1 P2 Q1 Q2 : Prop,
    (P1 P2) (Q1 Q2) P1 Q1 P2 Q2) by tauto.
move=>> Hp; apply H; [apply lin_gen_permutF | apply lin_indep_permutF]; easy.
Qed.

Lemma basis_permutF_equiv :
   {n} {p} {B : 'E^n},
    bijective p basis PE (permutF p B) basis PE B.
Proof.
assert (H : P1 P2 Q1 Q2 : Prop,
    (P1 P2) (Q1 Q2) P1 Q1 P2 Q2) by tauto.
move=>> Hp; apply H;
    [apply lin_gen_permutF_equiv | apply lin_indep_permutF_equiv]; easy.
Qed.

Lemma basis_zero_closed : {n} (B : 'E^n), basis PE B PE 0.
Proof. move=>> /basis_lin_gen; apply lin_gen_zero_closed. Qed.

Lemma basis_plus_closed : {n} (B : 'E^n), basis PE B plus_closed PE.
Proof. move=>> /basis_lin_gen; apply lin_gen_plus_closed. Qed.

Lemma basis_opp_closed : {n} (B : 'E^n), basis PE B opp_closed PE.
Proof. move=>> /basis_lin_gen; apply lin_gen_opp_closed. Qed.

Lemma basis_minus_closed :
   {n} (B : 'E^n), basis PE B minus_closed PE.
Proof. move=>> /basis_lin_gen; apply lin_gen_minus_closed. Qed.

Lemma basis_scal_closed : {n} (B : 'E^n), basis PE B scal_closed PE.
Proof. move=>> /basis_lin_gen; apply lin_gen_scal_closed. Qed.

Lemma basis_cms : {n} (B : 'E^n), basis PE B compatible_ms PE.
Proof. move=>> /basis_lin_gen; apply lin_gen_cms. Qed.

Lemma basis_lc_closed : {n} (B : 'E^n), basis PE B lc_closed PE.
Proof. move=>> /basis_lin_gen; apply lin_gen_lc_closed. Qed.

Lemma basis_ex_decomp : {n} {B : 'E^n}, basis PE B lc_surjL PE B.
Proof. move=>> /basis_lin_gen; apply lin_gen_ex_decomp. Qed.

Lemma basis_uniq_decomp : PE {n} {B : 'E^n}, basis PE B lc_injL B.
Proof. move=>> /basis_lin_indep; apply lin_indep_uniq_decomp. Qed.

Lemma basis_ex_uniq_decomp : {n} {B : 'E^n}, basis PE B lc_bijL PE B.
Proof.
move=>> HB; apply lc_surjL_injL_bijL;
    [apply basis_ex_decomp | apply (basis_uniq_decomp PE)]; easy.
Qed.

Lemma basis_ex_uniq_decomp_rev :
   {n} {B : 'E^n},
    compatible_ms PE inclF B PE lc_bijL PE B basis PE B.
Proof.
move=>> HPE HB1 HB2; split.
apply lin_gen_uniq_decomp_rev; easy.
apply lin_indep_uniq_decomp_rev, (lc_bijL_injL PE); easy.
Qed.

Lemma basis_ex_uniq_decomp_equiv :
   {n} {B : 'E^n},
    compatible_ms PE inclF B PE basis PE B lc_bijL PE B.
Proof.
intros; split. apply basis_ex_uniq_decomp.
apply basis_ex_uniq_decomp_rev; easy.
Qed.

End Basis_Facts1.

Section Basis_Facts2.

More properties of basis (from those of lin_gen and lin_indep).

Context {K : Ring}.
Hypothesis HK : nonzero_struct K.
Context {E : ModuleSpace K}.
Variable PE : E Prop.

Lemma basis_nonzero_sub_struct :
   {PE} {n} (B : 'E^n.+1), basis PE B PE zero_sub_struct.
Proof.
movePE' n B [/lin_gen_inclF HB /(lin_indep_S_nonzero HK) /nextF_rev [i Hi]].
apply nonzero_sub_struct_ex; (B i); easy.
Qed.

Lemma basis_nonzero_sub_struct_rev :
   {n} (B : 'E^n), basis PE B PE zero_sub_struct (0 < n)%coq_nat.
Proof.
move=>> HB /nonzero_sub_struct_ex HPE; specialize (HPE (basis_nonempty _ HB)).
apply (basis_nonzero_rev _ _ HB); contradict HPE; rewrite HPE in HB.
intros [x [Hx Hx2]]; contradict Hx2.
destruct (basis_ex_decomp HB x Hx) as [L HL].
rewrite HL lc_zero_r; easy.
Qed.

Lemma basis_nonzero_sub_struct_equiv :
   {n} (B : 'E^n), basis PE B PE zero_sub_struct (0 < n)%coq_nat.
Proof.
intros n B HB; split; [apply (basis_nonzero_sub_struct_rev _ HB) |].
intros; destruct n as [| n]; try apply (basis_nonzero_sub_struct B); easy.
Qed.

End Basis_Facts2.

Section Basis_sub_Facts1a.

Properties of basis on sub-module spaces (from those of lin_gen and lin_indep).

Context {K : Ring}.
Context {E : ModuleSpace K}.
Context {PE : E Prop}.
Hypothesis HPE : compatible_ms PE.
Let PE_ms := sub_ModuleSpace HPE.

Context {n : nat}.
Context {B : 'E^n}.
Hypothesis HB : inclF B PE.
Let B_ms : 'PE_ms^n := fun imk_sub (HB i).

Lemma basis_sub : basis PE B basis fullset B_ms.
Proof.
intros [H1 H2]; split; [apply lin_gen_sub | apply lin_indep_sub]; easy.
Qed.

Lemma basis_sub_rev : basis fullset B_ms basis PE B.
Proof.
intros [H1 H2]; split;
    [apply (lin_gen_sub_rev HPE HB) | apply (lin_indep_sub_rev HPE HB)]; easy.
Qed.

Lemma basis_sub_equiv : basis fullset B_ms basis PE B.
Proof. intros; split; [apply basis_sub_rev | apply basis_sub]. Qed.

End Basis_sub_Facts1a.

Section Basis_sub_Facts1b.

More properties of basis on sub-module spaces (from those of lin_gen and lin_indep).

Context {K : Ring}.
Context {E : ModuleSpace K}.
Context {PE : E Prop}.

Context {n : nat}.
Context {B : 'E^n}.
Hypothesis HB : basis PE B.
Let HPE := basis_cms _ HB.
Let PE_ms := sub_ModuleSpace HPE.
Let B_ms : 'PE_ms^n := fun imk_sub (basis_inclF HB i).

Lemma basis_sub_alt : basis fullset B_ms.
Proof. apply basis_sub; easy. Qed.

End Basis_sub_Facts1b.

Section Basis_sub_Facts1c.

More properties of basis on sub-module spaces (from those of lin_gen and lin_indep).

Context {K : Ring}.
Context {E : ModuleSpace K}.
Context {PE : E Prop}.
Hypothesis HPE : compatible_ms PE.
Let PE_ms := sub_ModuleSpace HPE.

Context {n : nat}.
Context {B_ms : 'PE_ms^n}.
Let B := mapF val B_ms.

Lemma basis_val : basis fullset B_ms basis PE B.
Proof.
intros [H1 H2]; split; [apply lin_gen_val | apply lin_indep_val]; easy.
Qed.

Lemma basis_val_rev : basis PE B basis fullset B_ms.
Proof.
intros [H1 H2]; split; [apply lin_gen_val_rev | apply lin_indep_val_rev]; easy.
Qed.

Lemma basis_val_equiv : basis PE B basis fullset B_ms.
Proof. split; [apply basis_val_rev | apply basis_val]. Qed.

End Basis_sub_Facts1c.

Section Basis_sub_Facts2.

More properties of basis on sub-module spaces (from those of lin_gen and lin_indep).

Context {K : Ring}.
Context {E : ModuleSpace K}.
Context {PEa PE : E Prop}.
Hypothesis HPEa : incl PEa PE.
Hypothesis HPE : compatible_ms PE.
Let PE_ms := sub_ModuleSpace HPE.
Let PEa' : PE_ms Prop := preimage val PEa.

Lemma basis_preimage_val :
   {n} {B : 'E^n} (HB : basis PEa B),
    basis PEa' (fun imk_sub (HPEa _ (basis_inclF HB i))).
Proof.
intros n B [H1 H2]; split.
apply (lin_gen_ext (fun imk_sub (HPEa (B i) (lin_gen_inclF H1 i)))).
apply extF; intros i; apply mk_sub_ext; easy.
apply lin_gen_preimage_val.
apply lin_indep_sub; easy.
Qed.

Lemma basis_preimage_val_rev :
   {n} {B' : 'PE_ms^n}, basis PEa' B' basis PEa (mapF val B').
Proof.
move=>> [H1 H2]; split.
apply lin_gen_preimage_val_rev; easy.
apply (lin_indep_sub_rev HPE (in_subF _)); rewrite -mk_subF_eq; easy.
Qed.

End Basis_sub_Facts2.

Section Basis_sub_Facts3.

More properties of basis on sub-module spaces (from those of lin_gen and lin_indep).

Context {K : Ring}.
Context {E : ModuleSpace K}.
Context {PE : E Prop}.
Hypothesis HPE : compatible_ms PE.
Let PE_ms := sub_ModuleSpace HPE.
Variable PEa' : PE_ms Prop.
Let PEa := RgS PEa' val.

Lemma basis_RgS_val :
   {n} {B' : 'PE_ms^n}, basis PEa' B' basis PEa (mapF val B').
Proof.
move=>> [H1 H2]; split.
apply lin_gen_RgS_val; easy.
apply (lin_indep_sub_rev HPE (in_subF _)); rewrite -mk_subF_eq; easy.
Qed.

Lemma basis_RgS_val_rev :
   {n} {B : 'E^n} (HB : basis PEa B),
    basis PEa' (fun imk_sub (incl_RgS_val _ _ _ (basis_inclF HB i))).
Proof.
intros n B [H1 H2]; split.
apply (lin_gen_ext
    (fun imk_sub (incl_RgS_val _ _ _ (lin_gen_inclF H1 i)))).
apply extF; intros i; apply mk_sub_ext; easy.
apply lin_gen_RgS_val_rev.
apply lin_indep_sub; easy.
Qed.

End Basis_sub_Facts3.

Section Has_dimension_Facts.

Properties of has_dim (from those of basis).

Context {K : Ring}.
Hypothesis HK : nonzero_struct K.
Context {E : ModuleSpace K}.
Context {PE : E Prop}.

Lemma has_dim_fin_dim : n, has_dim PE n fin_dim PE.
Proof. intros n [B [HB _]]; n, B; easy. Qed.

Lemma has_dim_lin_span :
   {n} {B : 'E^n}, lin_indep B has_dim (lin_span B) n.
Proof. intros; apply: Dim; apply basis_lin_span_equiv; easy. Qed.

Lemma has_dim_lin_span_alt :
   {n1 n2} {B1 : 'E^n1},
    n1 = n2 lin_indep B1 has_dim (lin_span B1) n2.
Proof. move=>> H; subst; apply has_dim_lin_span. Qed.

Lemma has_dim_nonempty : n, has_dim PE n nonempty PE.
Proof. move=>> [B HB]; apply (basis_nonempty _ HB). Qed.

Lemma has_dim_0 : has_dim (@zero_sub_struct E) 0.
Proof. apply (Dim _ _ (fun _ : 'I_0 ⇒ 0)), basis_nil. Qed.

Lemma has_dim_0_rev : has_dim PE 0 PE = zero_sub_struct.
Proof. intros [B [HB1 HB2]]; rewrite HB1; apply lin_span_nil. Qed.

Lemma has_dim_0_equiv : has_dim PE 0 PE = zero_sub_struct.
Proof.
split. apply has_dim_0_rev. intros HPE; rewrite HPE; apply has_dim_0.
Qed.

Lemma has_dim_nonzero_sub_struct :
   n, has_dim PE n.+1 PE zero_sub_struct.
Proof. move=>> [B HB]; apply (basis_nonzero_sub_struct HK _ HB). Qed.

Lemma has_dim_nonzero_sub_struct_rev :
   {n}, has_dim PE n PE zero_sub_struct (0 < n)%coq_nat.
Proof. move=>> [B HB]; apply (basis_nonzero_sub_struct_rev _ _ HB). Qed.

Lemma has_dim_nonzero_sub_struct_equiv :
   {n}, has_dim PE n PE zero_sub_struct (0 < n)%coq_nat.
Proof. move=>> [B HB]; apply (basis_nonzero_sub_struct_equiv HK _ _ HB). Qed.

Lemma has_dim_zero_closed : n, has_dim PE n PE 0.
Proof. move=>> [B HB]; apply (basis_zero_closed _ HB). Qed.

Lemma has_dim_plus_closed : n, has_dim PE n plus_closed PE.
Proof. move=>> [B HB]; apply (basis_plus_closed _ HB). Qed.

Lemma has_dim_opp_closed : n, has_dim PE n opp_closed PE.
Proof. move=>> [B HB]; apply (basis_opp_closed _ HB). Qed.

Lemma has_dim_minus_closed : n, has_dim PE n minus_closed PE.
Proof. move=>> [B HB]; apply (basis_minus_closed _ HB). Qed.

Lemma has_dim_scal_closed : n, has_dim PE n scal_closed PE.
Proof. move=>> [B HB]; apply (basis_scal_closed _ HB). Qed.

Lemma has_dim_cms : n, has_dim PE n compatible_ms PE.
Proof. move=>> [B HB]; apply (basis_cms _ HB). Qed.

Lemma has_dim_lc_closed : n, has_dim PE n lc_closed PE.
Proof. move=>> [B HB]; apply (basis_lc_closed _ HB). Qed.

End Has_dimension_Facts.

Section Has_dimension_sub_Facts1a.

Properties of has_dim on sub-module spaces (from those of basis).

Context {K : Ring}.
Context {E : ModuleSpace K}.
Context {PE : E Prop}.
Hypothesis HPE : compatible_ms PE.
Let PE_ms := sub_ModuleSpace HPE.

Context {n : nat}.

Lemma has_dim_sub : has_dim PE n has_dim (@fullset PE_ms) n.
Proof. intros [B HB]; apply: Dim (basis_sub HPE (basis_inclF HB) HB). Qed.

Lemma has_dim_sub_rev : has_dim (@fullset PE_ms) n has_dim PE n.
Proof.
intros [B_ms HB_ms]; apply: Dim; apply (basis_sub_rev HPE (in_subF B_ms)).
rewrite -mk_subF_eq; easy.
Qed.

Lemma has_dim_sub_equiv : has_dim (@fullset PE_ms) n has_dim PE n.
Proof. intros; split; [apply has_dim_sub_rev | apply has_dim_sub]. Qed.

End Has_dimension_sub_Facts1a.

Section Has_dimension_sub_Facts1b.

More properties of lin_gen on sub-module spaces.

Context {K : Ring}.
Context {E : ModuleSpace K}.
Context {PE : E Prop}.

Context {n : nat}.
Hypothesis HPE : has_dim PE n.
Let PE_ms := sub_ModuleSpace (has_dim_cms _ HPE).

Lemma has_dim_sub_alt : has_dim (@fullset PE_ms) n.
Proof. apply has_dim_sub; easy. Qed.

End Has_dimension_sub_Facts1b.

Section Has_dimension_sub_Facts2.

More properties of has_dim on sub-module spaces (from those of basis).

Context {K : Ring}.
Context {E : ModuleSpace K}.
Context {PEa PE : E Prop}.
Hypothesis HPEa : incl PEa PE.
Hypothesis HPE : compatible_ms PE.
Let PE_ms := sub_ModuleSpace HPE.
Let PEa' : PE_ms Prop := preimage val PEa.

Lemma has_dim_preimage_val : {n}, has_dim PEa n has_dim PEa' n.
Proof. move=>> [B HB]; apply: Dim (basis_preimage_val HPEa _ HB). Qed.

Lemma has_dim_preimage_val_rev : {n}, has_dim PEa' n has_dim PEa n.
Proof. move=>> [B' HB']; apply: Dim (basis_preimage_val_rev HPEa _ HB'). Qed.

End Has_dimension_sub_Facts2.

Section Has_dimension_sub_Facts3.

More properties of has_dim on sub-module spaces (from those of basis).

Context {K : Ring}.
Context {E : ModuleSpace K}.
Context {PE : E Prop}.
Hypothesis HPE : compatible_ms PE.
Let PE_ms := sub_ModuleSpace HPE.
Variable PEa' : PE_ms Prop.
Let PEa := RgS PEa' val.

Lemma has_dim_RgS_val : {n}, has_dim PEa' n has_dim PEa n.
Proof. move=>> [B' HB']; apply: Dim (basis_RgS_val _ _ HB'). Qed.

Lemma has_dim_RgS_val_rev : {n}, has_dim PEa n has_dim PEa' n.
Proof. move=>> [B HB]; apply: Dim (basis_RgS_val_rev _ _ HB). Qed.

End Has_dimension_sub_Facts3.