Library Algebra.Finite_dim.Finite_dim_MS_lin_span
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 finite linear span in module spaces.
[GostiauxT1]
Bernard Gostiaux,
Cours de mathématiques spéciales - 1. Algèbre,
Mathématiques, Presses Universitaires de France, Paris, 1993,
https://www.puf.com/cours-de-mathematiques-speciales-tome-1-algebre.
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
Bibliography
Usage
From Requisite Require Import stdlib 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.
Local Open Scope Monoid_scope.
Local Open Scope Group_scope.
Local Open Scope Ring_scope.
Local Open Scope ModuleSpace_scope.
Section Linear_span_Subset_Facts.
Subset properties of lin_span.
Context {K : Ring}.
Context {E : ModuleSpace K}.
Lemma lin_span_inclF_diag : ∀ {n} (B : 'E^n), inclF B (lin_span B).
Proof. intros n B i; rewrite -lc_kron_l_in_r; easy. Qed.
Lemma lin_span_ub : ∀ {n} (B : 'E^n) A i, A = B i → lin_span B A.
Proof. intros; subst; apply lin_span_inclF_diag. Qed.
Lemma lin_span_nil : ∀ (B : 'E^0), lin_span B = zero_sub_struct.
Proof.
intros B; apply subset_ext_equiv; split.
intros _ [L]; apply lc_nil.
intros x Hx; rewrite Hx -(lc_zero_compat_l 0 B); easy.
Qed.
Lemma lin_span_zero : ∀ {n}, lin_span (0 : 'E^n) = zero_sub_struct.
Proof.
intros; apply subset_ext_equiv; split.
intros _ [L]; apply lc_zero_r.
intros x Hx; rewrite Hx -(lc_zero_compat_r (0 : 'K^n) 0); easy.
Qed.
Lemma lin_span_zero_alt :
∀ {n} {B : 'E^n}, B = 0 → lin_span B = zero_sub_struct.
Proof. move=>> ->; apply lin_span_zero. Qed.
Lemma lin_span_singleF : ∀ (B : 'E^1), lin_span B = line (B ord0).
Proof. intros B; rewrite → (singleF_correct B) at 1; easy. Qed.
Lemma lin_span_coupleF :
∀ (B : 'E^2), lin_span B = plane (B ord0) (B ord_max).
Proof. intros B; rewrite → (coupleF_correct B) at 1; easy. Qed.
Lemma lin_span_tripleF :
∀ (B : 'E^3), lin_span B = space_3 (B ord0) (B ord1) (B ord_max).
Proof. intros B; rewrite → (tripleF_correct B) at 1; easy. Qed.
Lemma lin_span_inclF :
∀ {n1 n2} (B1 : 'E^n1) (B2 : 'E^n2),
invalF B1 B2 → inclF B1 (lin_span B2).
Proof.
move=>> HB i; destruct (HB i) as [i2 Hi2];
rewrite Hi2; apply lin_span_inclF_diag.
Qed.
Lemma lin_spanF_ex :
∀ {n1 n2} (B1 : 'E^n1) (B2 : 'E^n2),
inclF B1 (lin_span B2) ↔
∃ M12, ∀ i1, B1 i1 = lin_comb (M12 i1) B2.
Proof.
intros n1 n2 B1 B2; split; intros HB.
assert (HB' : ∀ i1, ∃ L2, B1 i1 = lin_comb L2 B2).
intros i1; destruct (HB i1) as [L2]; ∃ L2; easy.
apply (choiceF _ HB').
destruct HB as [H HM]; intros i1; rewrite HM; easy.
Qed.
Lemma lin_spanF_ex_flipT :
∀ {n1 n2} (B1 : 'E^n1) (B2 : 'E^n2),
inclF B1 (lin_span B2) ↔
∃ M12, ∀ i1, B1 i1 = lin_comb (M12^~ i1) B2.
Proof.
intros; rewrite lin_spanF_ex; split; intros [L HL];
∃ (flipT L); intros j; rewrite HL; easy.
Qed.
Lemma lin_span_incl :
∀ {n1 n2} (B1 : 'E^n1) (B2 : 'E^n2),
inclF B1 (lin_span B2) → incl (lin_span B1) (lin_span B2).
Proof.
move=>> /lin_spanF_ex [M12 HM12] _ [L1]; apply lin_span_ex.
eexists; apply (lc2_l_alt HM12).
Qed.
Lemma lin_span_monot :
∀ {n1 n2} (B1 : 'E^n1) (B2 : 'E^n2),
invalF B1 B2 → incl (lin_span B1) (lin_span B2).
Proof. intros; apply lin_span_incl, lin_span_inclF; easy. Qed.
Lemma lin_span_ext :
∀ {n1 n2} (B1 : 'E^n1) (B2 : 'E^n2),
inclF B1 (lin_span B2) → inclF B2 (lin_span B1) →
lin_span B1 = lin_span B2.
Proof. intros; apply subset_ext_equiv; split; apply lin_span_incl; easy. Qed.
Lemma lin_span_concatF_sym_inclF :
∀ {n1 n2} (B1 : 'E^n1) (B2 : 'E^n2),
inclF (concatF B1 B2) (lin_span (concatF B2 B1)).
Proof.
intros n1 n2 B1 B2 i; apply lin_span_ex.
destruct (lt_dec i n1) as [Hi | Hi]; eexists.
rewrite concatF_correct_l -lc_kron_l_in_r.
rewrite -(lc_concatF_zero_lr _ _ B2) lc_concatF.
rewrite plus_comm; symmetry; apply lc_concatF.
rewrite concatF_correct_r -lc_kron_l_in_l.
rewrite -(lc_concatF_zero_ll _ B1) lc_concatF.
rewrite plus_comm; symmetry; apply lc_concatF.
Qed.
Lemma lin_span_coupleF_sym_inclF :
∀ (x0 x1 : E), inclF (coupleF x1 x0) (plane x0 x1).
Proof. intros; apply lin_span_inclF, invalF_coupleF_sym. Qed.
Lemma lin_span_coupleF_sym : ∀ (x0 x1 : E), plane x0 x1 = plane x1 x0.
Proof. intros; apply lin_span_ext; apply lin_span_coupleF_sym_inclF. Qed.
Lemma lin_span_castF_compat :
∀ {n1 n2} (H : n1 = n2) (B1 : 'E^n1),
lin_span (castF H B1) = lin_span B1.
Proof.
intros n1 n2 Hn B1; apply subset_ext_equiv;
split; intros _ [L]; apply lin_span_ex.
subst n1; ∃ L; rewrite castF_id; easy.
subst n2; ∃ L; rewrite castF_id; easy.
Qed.
Lemma lin_span_concatF_sym :
∀ {n1 n2} (B1 : 'E^n1) (B2 : 'E^n2),
lin_span (concatF B1 B2) = lin_span (concatF B2 B1).
Proof. intros; apply lin_span_ext; apply lin_span_concatF_sym_inclF. Qed.
Lemma lin_span_concatF_l :
∀ {n1 n2} (B1 : 'E^n1) (B2 : 'E^n2),
inclF B2 (lin_span B1) → lin_span (concatF B1 B2) = lin_span B1.
Proof.
intros n1 n2 B1 B2 HB; apply lin_span_ext.
apply concatF_lub_inclF; try apply lin_span_inclF_diag; easy.
eapply (inclF_monot_r (lin_span _));
[apply lin_span_monot, concatF_ub_l | apply lin_span_inclF_diag].
Qed.
Lemma lin_span_concatF_r :
∀ {n1 n2} (B1 : 'E^n1) (B2 : 'E^n2),
inclF B1 (lin_span B2) → lin_span (concatF B1 B2) = lin_span B2.
Proof.
intros; apply lin_span_ext.
apply concatF_lub_inclF; try apply lin_span_inclF_diag; easy.
eapply (inclF_monot_r (lin_span _));
[apply lin_span_monot, concatF_ub_r | apply lin_span_inclF_diag].
Qed.
Lemma lin_span_permutF :
∀ {n} {p} {B : 'E^n}, inclF (permutF p B) (lin_span B).
Proof. move=>>; apply lin_span_inclF, permutF_invalF_l. Qed.
Lemma lin_span_permutF_eq :
∀ {n} {p} {B : 'E^n},
bijective p → lin_span (permutF p B) = lin_span B.
Proof.
intros n p B Hp; apply lin_span_ext. apply lin_span_permutF.
rewrite {1}(permutF_f_inv_l Hp B); apply lin_span_permutF.
Qed.
Lemma lin_span_lin_span :
∀ {n1 n2} (B1 : 'E^n1) (B2 : 'E^n2) (L : 'K^n2),
(∀ i, lin_span B1 (B2 i)) → lin_span B1 (lin_comb L B2).
Proof.
intros n1 n2 B1 B2 L Hi.
generalize (lin_span_incl B2 B1); unfold incl; intros H.
apply H; easy.
Qed.
End Linear_span_Subset_Facts.
Section Linear_span_Linear_Facts.
Linear properties of lin_span.
Context {K : Ring}.
Context {E : ModuleSpace K}.
Context {n : nat}.
Variable B : 'E^n.
Lemma lin_span_zero_closed : lin_span B 0.
Proof. rewrite <- (lc_zero_compat_l 0 B); easy. Qed.
Lemma lin_span_nonempty : nonempty (lin_span B).
Proof. ∃ 0; apply lin_span_zero_closed. Qed.
Lemma lin_span_scal_closed : scal_closed (lin_span B).
Proof. intros l _ [Lx]; rewrite -lc_scal_l; easy. Qed.
Lemma lin_span_opp_closed : opp_closed (lin_span B).
Proof. apply scal_opp_closed, lin_span_scal_closed. Qed.
Lemma lin_span_plus_closed : plus_closed (lin_span B).
Proof. intros _ _ [Lx] [Ly]; rewrite -lc_plus_l; easy. Qed.
Lemma lin_span_minus_closed : minus_closed (lin_span B).
Proof.
apply plus_opp_minus_closed;
[apply lin_span_plus_closed | apply lin_span_opp_closed].
Qed.
Lemma lin_span_cms : compatible_ms (lin_span B).
Proof.
apply plus_scal_closed_cms; [∃ 0; apply lin_span_zero_closed |
apply lin_span_plus_closed | apply lin_span_scal_closed].
Qed.
Lemma lin_span_lc_closed : lc_closed (lin_span B).
Proof. intros m; apply cms_lc, lin_span_cms. Qed.
[GostiauxT1]
Th 6.19, pp. 168-169.
Lemma lin_span_equiv : lin_span B = span_ms (inF^~ B).
Proof.
apply subset_ext_equiv; split.
intros x [L]; apply span_ms_lc.
intros i; apply span_ms_incl; ∃ i; easy.
apply span_ms_lub.
apply lin_span_cms.
intros x [i Hi]; rewrite Hi; apply lin_span_inclF_diag.
Qed.
Lemma lin_span_ex_decomp : lc_surjL (lin_span B) B.
Proof. intros _ [L]; ∃ L; easy. Qed.
Lemma lin_span_lb :
∀ {PE}, compatible_ms PE → inclF B PE → incl (lin_span B) PE.
Proof. intros PE HPE HB x [L]; apply cms_lc; easy. Qed.
Lemma lin_span_glb :
lin_span B = (fun x ⇒ ∀ PE, compatible_ms PE → inclF B PE → PE x).
Proof.
apply subset_ext_equiv; split.
intros _ [L] PE HPE1 HPE2; apply cms_lc; easy.
intros x Hx; apply Hx; [apply lin_span_cms | apply lin_span_inclF_diag].
Qed.
Lemma lin_span_filter_n0F :
∀ {n} {B : 'E^n}, lin_span (filter_n0F B) = lin_span B.
Proof.
clear n B; intros n B; apply subset_ext_equiv; split; intros _ [L].
destruct (lc_filter_n0F_r_ex B L) as [L' ->]; easy.
rewrite -lc_filter_n0F_r; easy.
Qed.
End Linear_span_Linear_Facts.
Section Linear_combination_L_Facts.
Proof.
apply subset_ext_equiv; split.
intros x [L]; apply span_ms_lc.
intros i; apply span_ms_incl; ∃ i; easy.
apply span_ms_lub.
apply lin_span_cms.
intros x [i Hi]; rewrite Hi; apply lin_span_inclF_diag.
Qed.
Lemma lin_span_ex_decomp : lc_surjL (lin_span B) B.
Proof. intros _ [L]; ∃ L; easy. Qed.
Lemma lin_span_lb :
∀ {PE}, compatible_ms PE → inclF B PE → incl (lin_span B) PE.
Proof. intros PE HPE HB x [L]; apply cms_lc; easy. Qed.
Lemma lin_span_glb :
lin_span B = (fun x ⇒ ∀ PE, compatible_ms PE → inclF B PE → PE x).
Proof.
apply subset_ext_equiv; split.
intros _ [L] PE HPE1 HPE2; apply cms_lc; easy.
intros x Hx; apply Hx; [apply lin_span_cms | apply lin_span_inclF_diag].
Qed.
Lemma lin_span_filter_n0F :
∀ {n} {B : 'E^n}, lin_span (filter_n0F B) = lin_span B.
Proof.
clear n B; intros n B; apply subset_ext_equiv; split; intros _ [L].
destruct (lc_filter_n0F_r_ex B L) as [L' ->]; easy.
rewrite -lc_filter_n0F_r; easy.
Qed.
End Linear_span_Linear_Facts.
Section Linear_combination_L_Facts.
Properties of lc_surjL, lc_injL and lc_bijL.
Context {K : Ring}.
Context {E : ModuleSpace K}.
Variable PE : E → Prop.
Context {n : nat}.
Variable B : 'E^n.
Lemma lc_surjL_injL_bijL :
lc_surjL PE B → lc_injL B → lc_bijL PE B.
Proof.
intros HB1 HB2 x Hx; destruct (HB1 _ Hx) as [L HL].
∃ L; split; try easy.
intros L' HL'; apply HB2; rewrite <- HL; easy.
Qed.
Lemma lc_bijL_surjL : lc_bijL PE B → lc_surjL PE B.
Proof. intros HB x Hx; destruct (HB _ Hx) as [L [HL _]]; ∃ L; easy. Qed.
Lemma lc_bijL_injL :
compatible_ms PE → inclF B PE → lc_bijL PE B → lc_injL B.
Proof.
intros HPE HB1 HB2 L L' HL.
destruct (HB2 (lin_comb L B)) as [Lx [_ HLx]]; try now apply cms_lc.
apply trans_eq with Lx; [symmetry |]; apply HLx; easy.
Qed.
End Linear_combination_L_Facts.