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.

Brief description

Support for finite linear span in module spaces.

Description

Bibliography

[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.

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

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.