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.

Brief description

Support for linear generator finite families in module spaces.

Description

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.

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