Library Algebra.Finite_dim.Finite_dim_MS_lin_gen
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 linear generator finite families in module spaces.
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
Usage
From Requisite Require Import ssr.
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.
Local Open Scope Monoid_scope.
Local Open Scope Group_scope.
Local Open Scope Ring_scope.
Local Open Scope ModuleSpace_scope.
Section Linear_generator_Facts.
Properties of lin_gen (from those of lin_span).
Context {K : Ring}.
Context {E : ModuleSpace K}.
Context {PE : E → Prop}.
Lemma lin_gen_lin_span : ∀ {n} (B : 'E^n), lin_gen (lin_span B) B.
Proof. easy. Qed.
Lemma lin_gen_inclF : ∀ {n} {B : 'E^n}, lin_gen PE B → inclF B PE.
Proof. move=>> HB; rewrite HB; apply lin_span_inclF_diag. Qed.
Lemma lin_gen_nonempty : ∀ {n} (B : 'E^n), lin_gen PE B → nonempty PE.
Proof. move=>> ->; apply lin_span_nonempty. Qed.
Lemma lin_gen_nil : ∀ (B : 'E^0), lin_gen zero_sub_struct B.
Proof. intros; unfold lin_gen; rewrite lin_span_nil; easy. Qed.
Lemma lin_gen_nonzero :
∀ PE {n} {B : 'E^n}, lin_gen PE B → PE ≠ zero_sub_struct → B ≠ 0.
Proof. move=>> HB HPE; contradict HPE; rewrite HB HPE lin_span_zero; easy. Qed.
Lemma lin_gen_1 : ∀ (x0 : E), lin_gen (line x0) (singleF x0).
Proof. easy. Qed.
Lemma lin_gen_2 : ∀ (x0 x1 : E), lin_gen (plane x0 x1) (coupleF x0 x1).
Proof. easy. Qed.
Lemma lin_gen_3 :
∀ (x0 x1 x2 : E), lin_gen (space_3 x0 x1 x2) (tripleF x0 x1 x2).
Proof. easy. Qed.
Lemma lin_gen_coupleF_sym :
∀ (x0 x1 : E), lin_gen PE (coupleF x0 x1) → lin_gen PE (coupleF x1 x0).
Proof.
intros x0 x1; unfold lin_gen; fold (plane x0 x1).
rewrite lin_span_coupleF_sym; easy.
Qed.
Lemma lin_gen_monot :
∀ {n1 n2} (B1 : 'E^n1) {B2 : 'E^n2},
invalF B1 B2 → inclF B2 PE → lin_gen PE B1 → lin_gen PE B2.
Proof.
move=>> HB HB2 HB1; rewrite HB1; apply subset_ext_equiv; split.
apply lin_span_monot; easy. apply lin_span_incl; rewrite -HB1; easy.
Qed.
Lemma lin_gen_equiv :
∀ {n1 n2} (B1 : 'E^n1) (B2 : 'E^n2),
inclF B1 (lin_span B2) → inclF B2 (lin_span B1) →
lin_gen PE B1 ↔ lin_gen PE B2.
Proof. intros; unfold lin_gen; rewrite (lin_span_ext _ B2); easy. Qed.
Lemma lin_gen_castF_equiv :
∀ {n1 n2} (H : n1 = n2) {B1 : 'E^n1},
lin_gen PE (castF H B1) ↔ lin_gen PE B1.
Proof. intros; unfold lin_gen; rewrite lin_span_castF_compat; easy. Qed.
Lemma lin_gen_castF_compat :
∀ {n1 n2} (H : n1 = n2) {B1 : 'E^n1},
lin_gen PE B1 → lin_gen PE (castF H B1).
Proof. move=>>; apply lin_gen_castF_equiv. Qed.
Lemma lin_gen_castF_reg :
∀ {n1 n2} (H : n1 = n2) {B1 : 'E^n1},
lin_gen PE (castF H B1) → lin_gen PE B1.
Proof. move=>>; apply lin_gen_castF_equiv. Qed.
Lemma lin_gen_concatF_sym :
∀ {n1 n2} {B1 : 'E^n1} {B2 : 'E^n2},
lin_gen PE (concatF B1 B2) → lin_gen PE (concatF B2 B1).
Proof. move=>> HB; rewrite HB; apply lin_span_concatF_sym. Qed.
Lemma lin_gen_concatF_compat_l :
∀ {n1 n2} {B1 : 'E^n1} {B2 : 'E^n2},
inclF B2 PE → lin_gen PE B1 → lin_gen PE (concatF B1 B2).
Proof.
move=>> HB2 HB1; rewrite HB1;
apply eq_sym, lin_span_concatF_l; rewrite -HB1; easy.
Qed.
Lemma lin_gen_concatF_compat_r :
∀ {n1 n2} {B1 : 'E^n1} {B2 : 'E^n2},
inclF B1 PE → lin_gen PE B2 → lin_gen PE (concatF B1 B2).
Proof.
move=>> HB1 HB2; rewrite HB2;
apply eq_sym, lin_span_concatF_r; rewrite -HB2; easy.
Qed.
Lemma lin_gen_permutF :
∀ {n} {p} {B : 'E^n},
bijective p → lin_gen PE B → lin_gen PE (permutF p B).
Proof.
move=>> Hp ->; rewrite -(lin_span_permutF_eq Hp); apply lin_gen_lin_span.
Qed.
Lemma lin_gen_permutF_equiv :
∀ {n} {p} {B : 'E^n},
bijective p → lin_gen PE (permutF p B) ↔ lin_gen PE B.
Proof.
intros n p B Hp; split. 2: apply lin_gen_permutF; easy.
rewrite {2}(permutF_f_inv_l Hp B); apply lin_gen_permutF, f_inv_bij.
Qed.
Lemma lin_gen_zero_closed : ∀ {n} (B : 'E^n), lin_gen PE B → PE 0.
Proof. move=>> ->; apply lin_span_zero_closed. Qed.
Lemma lin_gen_plus_closed :
∀ {n} (B : 'E^n), lin_gen PE B → plus_closed PE.
Proof. move=>> ->; apply lin_span_plus_closed. Qed.
Lemma lin_gen_opp_closed :
∀ {n} (B : 'E^n), lin_gen PE B → opp_closed PE.
Proof. move=>> ->; apply lin_span_opp_closed. Qed.
Lemma lin_gen_minus_closed :
∀ {n} (B : 'E^n), lin_gen PE B → minus_closed PE.
Proof. move=>> ->; apply lin_span_minus_closed. Qed.
Lemma lin_gen_scal_closed :
∀ {n} (B : 'E^n), lin_gen PE B → scal_closed PE.
Proof. move=>> ->; apply lin_span_scal_closed. Qed.
Lemma lin_gen_cms : ∀ {n} (B : 'E^n), lin_gen PE B → compatible_ms PE.
Proof. move=>> ->; apply lin_span_cms. Qed.
Lemma lin_gen_lc_closed : ∀ {n} (B : 'E^n), lin_gen PE B → lc_closed PE.
Proof. move=>> ->; apply lin_span_lc_closed. Qed.
Lemma lin_gen_ex_decomp : ∀ {n} {B : 'E^n}, lin_gen PE B → lc_surjL PE B.
Proof. move=>> ->; apply lin_span_ex_decomp. Qed.
Lemma lin_gen_ex_decomp_rev :
∀ {n} {B : 'E^n},
compatible_ms PE → inclF B PE → lc_surjL PE B → lin_gen PE B.
Proof.
move=>> HB1 HB2 HB3; apply subset_ext_equiv; split.
intros x Hx; destruct (HB3 _ Hx) as [L HL]; rewrite HL; easy.
intros _ [L]; apply cms_lc; easy.
Qed.
Lemma lin_gen_uniq_decomp_rev :
∀ {n} {B : 'E^n},
compatible_ms PE → inclF B PE → lc_bijL PE B → lin_gen PE B.
Proof.
intros; apply lin_gen_ex_decomp_rev; try apply lc_bijL_surjL; easy.
Qed.
End Linear_generator_Facts.
Section Linear_generator_sub_Facts1a.
Properties of lin_gen on sub-module spaces.
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 i ⇒ mk_sub (HB i).
Lemma lin_gen_sub : lin_gen PE B → lin_gen fullset B_ms.
Proof.
intros HB1; apply subset_ext_equiv; split; try easy.
intros [x Hx] _; destruct (lin_gen_ex_decomp HB1 x Hx) as [L HL].
apply lin_span_ex; ∃ L; apply val_inj; rewrite val_lc; easy.
Qed.
Lemma lin_gen_sub_rev : lin_gen fullset B_ms → lin_gen PE B.
Proof.
intros HB1; apply subset_ext_equiv; split; intros x Hx.
destruct (lin_gen_ex_decomp HB1 (mk_sub Hx)) as [L HL]; [easy |].
apply lin_span_ex; ∃ L; move: HL;
move⇒ /(f_equal val); rewrite val_lc; easy.
induction Hx as [L]; apply (cms_lc HPE); easy.
Qed.
Lemma lin_gen_sub_equiv : lin_gen fullset B_ms ↔ lin_gen PE B.
Proof. intros; split; [apply lin_gen_sub_rev | apply lin_gen_sub]. Qed.
End Linear_generator_sub_Facts1a.
Section Linear_generator_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}.
Context {B : 'E^n}.
Hypothesis HB : lin_gen PE B.
Let HPE := lin_gen_cms _ HB.
Let PE_ms := sub_ModuleSpace HPE.
Let B_ms : 'PE_ms^n := fun i ⇒ mk_sub (lin_gen_inclF HB i).
Lemma lin_gen_sub_alt : lin_gen fullset B_ms.
Proof. apply lin_gen_sub; easy. Qed.
End Linear_generator_sub_Facts1b.
Section Linear_generator_sub_Facts1c.
More properties of lin_gen on sub-module spaces.
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}.
Variable B_ms : 'PE_ms^n.
Let B := mapF val B_ms.
Lemma lin_gen_val : lin_gen fullset B_ms → lin_gen PE B.
Proof.
rewrite -(lin_gen_sub_equiv HPE (in_subF B_ms)) -(mk_subF_eq B_ms); easy.
Qed.
Lemma lin_gen_val_rev : lin_gen PE B → lin_gen fullset B_ms.
Proof. rewrite (mk_subF_eq B_ms) (lin_gen_sub_equiv HPE); easy. Qed.
Lemma lin_gen_val_equiv : lin_gen PE B ↔ lin_gen fullset B_ms.
Proof. split; [apply lin_gen_val_rev | apply lin_gen_val]. Qed.
End Linear_generator_sub_Facts1c.
Section Linear_generator_sub_Facts2.
More properties of lin_gen on sub-module spaces.
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 lin_gen_preimage_val :
∀ {n} {B : 'E^n} (HB : lin_gen PEa B),
lin_gen PEa' (fun i ⇒ mk_sub (HPEa _ (lin_gen_inclF HB i))).
Proof.
intros n B HB; apply lin_gen_ex_decomp_rev.
apply preimage_val_cms, (lin_gen_cms _ HB).
apply (lin_gen_inclF HB).
intros x Hx; destruct (lin_gen_ex_decomp HB (val x)) as [L HL]; [easy |].
∃ L; apply val_inj; rewrite val_lc; easy.
Qed.
Lemma lin_gen_preimage_val_rev :
∀ {n} {B' : 'PE_ms^n}, lin_gen PEa' B' → lin_gen PEa (mapF val B').
Proof.
intros n B' HB'; apply lin_gen_ex_decomp_rev.
apply (preimage_val_cms_rev HPEa HPE), (lin_gen_cms _ HB').
apply (lin_gen_inclF HB').
intros x Hx; destruct (lin_gen_ex_decomp HB' (mk_sub (HPEa _ Hx)))
as [L HL]; [easy |].
∃ L; move: HL ⇒ /(f_equal val); rewrite val_lc; easy.
Qed.
End Linear_generator_sub_Facts2.
Section Linear_generator_sub_Facts3.
More properties of lin_gen on sub-module spaces.
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 incl_RgS_val : incl PEa PE.
Proof. intros _ [x Hx]; apply in_sub. Qed.
Lemma lin_gen_RgS_val :
∀ {n} {B' : 'PE_ms^n}, lin_gen PEa' B' → lin_gen PEa (mapF val B').
Proof.
move=>>; rewrite -(preimage_image_val PEa');
apply lin_gen_preimage_val_rev, incl_RgS_val.
Qed.
Lemma lin_gen_RgS_val_rev :
∀ {n} {B : 'E^n} (HB : lin_gen PEa B),
lin_gen PEa' (fun i ⇒ mk_sub (incl_RgS_val _ (lin_gen_inclF HB i))).
Proof.
intros; rewrite -(preimage_image_val PEa'); apply lin_gen_preimage_val.
Qed.
End Linear_generator_sub_Facts3.
Section Finite_dimension_Facts.
Properties of fin_dim (from those of lin_gen).
Context {K : Ring}.
Context {E : ModuleSpace K}.
Context {PE : E → Prop}.
Lemma fin_dim_lin_span : ∀ {n} (B : 'E^n), fin_dim (lin_span B).
Proof. intros n B; ∃ n, B; apply lin_gen_lin_span. Qed.
Lemma fin_dim_nonempty : fin_dim PE → nonempty PE.
Proof. intros [n [B HB]]; move: HB; apply lin_gen_nonempty. Qed.
Lemma fin_dim_0 : fin_dim (@zero_sub_struct E).
Proof. ∃ 0, (fun _ ⇒ 0); apply lin_gen_nil. Qed.
Lemma fin_dim_1 : ∀ (x0 : E), fin_dim (line x0).
Proof. intros x0; ∃ 1%nat, (singleF x0); apply lin_gen_1. Qed.
Lemma fin_dim_2 : ∀ (x0 x1 : E), fin_dim (plane x0 x1).
Proof. intros x0 x1; ∃ 2%nat, (coupleF x0 x1); apply lin_gen_2. Qed.
Lemma fin_dim_3 : ∀ (x0 x1 x2 : E), fin_dim (space_3 x0 x1 x2).
Proof. intros x0 x1 x2; ∃ 3%nat, (tripleF x0 x1 x2); apply lin_gen_3. Qed.
Lemma fin_dim_zero_closed : fin_dim PE → zero_closed PE.
Proof. intros [n [B HB]]; move: HB; apply lin_gen_zero_closed. Qed.
Lemma fin_dim_plus_closed : fin_dim PE → plus_closed PE.
Proof. intros [n [B HB]]; move: HB; apply lin_gen_plus_closed. Qed.
Lemma fin_dim_opp_closed : fin_dim PE → opp_closed PE.
Proof. intros [n [B HB]]; move: HB; apply lin_gen_opp_closed. Qed.
Lemma fin_dim_minus_closed : fin_dim PE → minus_closed PE.
Proof. intros [n [B HB]]; move: HB; apply lin_gen_minus_closed. Qed.
Lemma fin_dim_scal_closed : fin_dim PE → scal_closed PE.
Proof. intros [n [B HB]]; move: HB; apply lin_gen_scal_closed. Qed.
Lemma fin_dim_cms : fin_dim PE → compatible_ms PE.
Proof. intros [n [B HB]]; move: HB; apply lin_gen_cms. Qed.
Lemma fin_dim_lc_closed : fin_dim PE → lc_closed PE.
Proof. intros [n [B HB]]; move: HB; apply lin_gen_lc_closed. Qed.
Lemma fin_dim_ex_decomp_rev :
∀ {n} (B : 'E^n),
compatible_ms PE → inclF B PE → lc_surjL PE B → fin_dim PE.
Proof. intros n B; intros; ∃ n, B; apply lin_gen_ex_decomp_rev; easy. Qed.
Lemma fin_dim_uniq_decomp_rev :
∀ {n} (B : 'E^n),
compatible_ms PE → inclF B PE → lc_bijL PE B → fin_dim PE.
Proof.
intros n B; intros; ∃ n, B; apply lin_gen_uniq_decomp_rev; easy.
Qed.
End Finite_dimension_Facts.
Section Finite_dimension_sub_Facts1a.
Properties of fin_dim on sub-module spaces (from those of lin_gen).
Context {K : Ring}.
Context {E : ModuleSpace K}.
Context {PE : E → Prop}.
Hypothesis HPE : compatible_ms PE.
Let PE_ms := sub_ModuleSpace HPE.
Lemma fin_dim_sub : fin_dim PE → fin_dim (@fullset PE_ms).
Proof.
intros [n [B HB1]]; move: (lin_gen_inclF HB1) ⇒ HB2.
∃ n, (fun i ⇒ mk_sub (HB2 i)).
apply lin_gen_sub; easy.
Qed.
Lemma fin_dim_sub_rev : fin_dim (@fullset PE_ms) → fin_dim PE.
Proof.
intros [n [B_ms HB1]]. move: (lin_gen_inclF HB1) ⇒ HB2.
∃ n, (mapF val B_ms); apply lin_gen_val; easy.
Qed.
Lemma fin_dim_sub_equiv : fin_dim (@fullset PE_ms) ↔ fin_dim PE.
Proof. intros; split; [apply fin_dim_sub_rev | apply fin_dim_sub]. Qed.
End Finite_dimension_sub_Facts1a.
Section Finite_dimension_sub_Facts1b.
More properties of fin_dim on sub-module spaces (from those of lin_gen).
Context {K : Ring}.
Context {E : ModuleSpace K}.
Context {PE : E → Prop}.
Hypothesis HPE : fin_dim PE.
Let HPE1 := fin_dim_cms HPE.
Let PE_ms := sub_ModuleSpace HPE1.
Lemma fin_dim_sub_alt : fin_dim (@fullset PE_ms).
Proof. apply fin_dim_sub; easy. Qed.
End Finite_dimension_sub_Facts1b.
Section Finite_dimension_sub_Facts2.
More properties of fin_dim on sub-module spaces (from those of lin_gen).
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 fin_dim_preimage_val : fin_dim PEa → fin_dim PEa'.
Proof.
intros [n [B HB]]; ∃ n, (fun i ⇒ mk_sub (HPEa _ (lin_gen_inclF HB i))).
apply lin_gen_preimage_val.
Qed.
Lemma fin_dim_preimage_val_rev : fin_dim PEa' → fin_dim PEa.
Proof.
intros [n [B' HB']]; ∃ n, (mapF val B');
apply (lin_gen_preimage_val_rev HPEa); easy.
Qed.
Lemma fin_dim_preimage_val_equiv : fin_dim PEa' ↔ fin_dim PEa.
Proof.
split; [apply fin_dim_preimage_val_rev | apply fin_dim_preimage_val].
Qed.
End Finite_dimension_sub_Facts2.
Section Finite_dimension_sub_Facts3.
More properties of fin_dim on sub-module spaces (from those of lin_gen).
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 fin_dim_RgS_val : fin_dim PEa' → fin_dim PEa.
Proof.
intros [n [B' HB']]; ∃ n, (mapF val B'); apply lin_gen_RgS_val; easy.
Qed.
Lemma fin_dim_RgS_val_rev : fin_dim PEa → fin_dim PEa'.
Proof.
intros [n [B HB]];
∃ n, (fun i ⇒ mk_sub (incl_RgS_val _ _ _ (lin_gen_inclF HB i))).
apply lin_gen_RgS_val_rev.
Qed.
Lemma fin_dim_RgS_val_equiv : fin_dim PEa ↔ fin_dim PEa'.
Proof. split; [apply fin_dim_RgS_val_rev | apply fin_dim_RgS_val]. Qed.
End Finite_dimension_sub_Facts3.