Library Algebra.Finite_dim.Finite_dim_MS_lin_indep

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 independent 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_lin_indep_R where they are only stated in the case of the ring of real numbers R_Ring.

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

Properties of lin_dep/lin_indep.

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

Lemma lin_dep_ex :
   {n} {B : 'E^n}, lin_dep B L, lin_comb L B = 0 L 0.
Proof.
intros n B; split; intros HB.
destruct (not_all_ex_not _ _ HB) as [L HL]; L; apply imply_to_and; easy.
destruct HB as [L [HL1 HL2]]; apply ex_not_not_all; L; intros; auto.
Qed.

Establish first the property on lin_dep.

Lemma lin_dep_with_zero : {n} {B : 'E^n}, inF 0 B lin_dep B.
Proof.
intros n B [i Hi]; apply lin_dep_ex; (kron _ i); split.
rewrite lc_kron_l_in_r; easy.
apply nextF; i; rewrite kron_is_1; try easy.
apply one_not_zero; easy.
Qed.

Lemma lin_dep_S_zero : {n}, lin_dep (0 : 'E^n.+1).
Proof. intros; apply lin_dep_with_zero; ord0; easy. Qed.

Lemma lin_dep_zero_rev : {n}, lin_dep (0 : 'E^n) (0 < n)%coq_nat.
Proof.
move=>> /lin_dep_ex [L [_ /nextF_rev [i _]]].
apply Nat.neq_0_lt_0; contradict i; rewrite i; intros [j Hj]; easy.
Qed.

Lemma lin_dep_zero_equiv : {n}, lin_dep (0 : 'E^n) (0 < n)%coq_nat.
Proof.
intros n; split; [apply lin_dep_zero_rev |].
destruct n as [| n]; try easy; intros _; apply lin_dep_S_zero.
Qed.

Lemma lin_dep_not_injF : {n} {B : 'E^n}, ¬ injective B lin_dep B.
Proof.
moven B /not_all_ex_not [i0 /not_all_ex_not [i1 H]].
destruct n; try now destruct i0.
apply imply_to_and in H; destruct H as [HB Hi]; apply not_eq_sym in Hi.
destruct n; try now rewrite 2!I_1_is_unit in Hi.
rewrite lin_dep_ex; (kron _ i0 - kron _ i1); split.
rewrite lc_plus_l lc_opp_l 2!lc_kron_l_in_r -HB.
apply: minus_eq_zero.
apply nextF; i0.
rewritefct_minus_eq, kron_is_1, kron_is_0; try easy.
rewrite minus_zero_r; apply one_not_zero; easy.
apply ord_neq_compat; easy.
Qed.

Lemma lin_dep_castF_compat :
   {n1 n2} (H : n1 = n2) {B1 : 'E^n1},
    lin_dep B1 lin_dep (castF H B1).
Proof.
intros n1 n2 H B1; rewrite 2!lin_dep_ex.
intros [L [HL HL0]]; (castF H L); split; try now rewrite lc_castF.
contradict HL0; apply (castF_zero_reg H); easy.
Qed.

Lemma lin_dep_castF_reg :
   {n1 n2} (H : n1 = n2) {B1 : 'E^n1},
    lin_dep (castF H B1) lin_dep B1.
Proof.
intros n1 n2 H B1 HB; rewrite -(castF_can _ (eq_sym H) B1).
apply lin_dep_castF_compat; easy.
Qed.

Lemma lin_dep_castF_equiv :
   {n1 n2} (H : n1 = n2) {B1 : 'E^n1},
    lin_dep (castF H B1) lin_dep B1.
Proof.
intros; split. apply lin_dep_castF_reg. apply lin_dep_castF_compat.
Qed.

Lemma lin_dep_concatF_compat_l :
   {n1 n2} {B1 : 'E^n1} (B2 : 'E^n2),
    lin_dep B1 lin_dep (concatF B1 B2).
Proof.
move=>>; rewrite 2!lin_dep_ex; intros [L HL]; (concatF L 0); split.
rewrite lc_concatF_zero_lr; easy.
apply concatF_zero_nextF_compat_l; easy.
Qed.

Lemma lin_dep_concatF_compat_r :
   {n1 n2} (B1 : 'E^n1) {B2 : 'E^n2},
    lin_dep B2 lin_dep (concatF B1 B2).
Proof.
move=>>; rewrite 2!lin_dep_ex; intros [L HL]; (concatF 0 L); split.
rewrite lc_concatF_zero_ll; easy.
apply concatF_zero_nextF_compat_r; easy.
Qed.

Lemma lin_dep_concatF_not_disjF :
   {n1 n2} {B1 : 'E^n1} {B2 : 'E^n2} x,
    inF x B1 inF x B2 lin_dep (concatF B1 B2).
Proof.
intros n1 n2 B1 B2 x [i1 Hx1] [i2 Hx2]; apply lin_dep_not_injF.
assert (Hf : (first_ord n2 i1 < n1)%coq_nat) by now apply /ltP; simpl.
assert (Hl : ¬ (last_ord n1 i2 < n1)%coq_nat)
    by (apply Nat.nlt_ge; apply /leP; apply leq_addr).
apply ex_not_not_all; (first_ord n2 i1).
apply ex_not_not_all; (last_ord n1 i2).
rewrite not_imp_and_equiv; split; try apply ord_neq; auto with zarith.
rewrite concatF_correct_l concat_l_first
    concatF_correct_r concat_r_last -Hx1; easy.
Qed.

Lemma lin_dep_insertF_compat :
   {n} {B : 'E^n} x0 i0, lin_dep B lin_dep (insertF B x0 i0).
Proof.
intros n B x0 i0; rewrite 2!lin_dep_ex; move⇒ [L [HL /nextF_rev [i Hi]]].
(insertF L 0 i0); split.
rewrite lc_insertF scal_zero_l HL plus_zero_l; easy.
apply nextF; (skip_ord i0 i); rewrite insertF_correct; easy.
Qed.

Lemma lin_dep_skipF_reg :
   {n} {B : 'E^n.+1} i0, lin_dep (skipF B i0) lin_dep B.
Proof.
intros n B i0; rewrite -{2}(insertF_skipF B i0).
apply lin_dep_insertF_compat.
Qed.

Lemma lin_dep_line :
   {n} {B : 'E^n} {i j}, i j line (B i) (B j) lin_dep B.
Proof.
moven B i j Hi /lin_span_EX [Lj HLj]; apply lin_dep_ex;
     (kron _ j - scal (Lj ord0) (kron _ i)); split.
rewrite lc_minus_l lc_scal_l 2!lc_kron_l_in_r HLj.
rewrite lc_1; apply: minus_eq_zero.
apply nextF; j.
rewritefct_minus_eq, fct_scal_r_eq, kron_is_1, kron_is_0; try easy.
rewrite scal_zero_r minus_zero_r; apply one_not_zero; easy.
intros; contradict Hi; apply ord_inj; easy.
Qed.

Lemma lin_dep_plane :
   {n} {B : 'E^n} {i j k},
    i k j k plane (B i) (B j) (B k) lin_dep B.
Proof.
moven B i j k Hi Hj /lin_span_EX [Lk HLk]; apply lin_dep_ex;
   (kron _ k
      - scal (Lk ord0) (kron _ i) - scal (Lk ord_max) (kron _ j)); split.
rewrite 2!lc_minus_l 2!lc_scal_l 3!lc_kron_l_in_r HLk.
rewrite lc_2 coupleF_0 coupleF_1; apply: minus2_eq_zero.
apply nextF; k.
rewrite → 2!fct_minus_eq, 2!fct_scal_r_eq,
    kron_is_1, 2!kron_is_0; try apply ord_neq_compat; try easy.
rewrite 2!scal_zero_r 2!minus_zero_r; apply one_not_zero; easy.
Qed.

Lemma lin_indep_without_zero : {n} {B : 'E^n}, lin_indep B ¬ inF 0 B.
Proof. move=>>; rewrite contra_not_r_equiv; apply lin_dep_with_zero. Qed.

Lemma lin_indep_zero_rev : {n}, lin_indep (0 : 'E^n) n = O.
Proof.
intros n; rewrite -Nat.le_0_r -Nat.nlt_ge contra_not_r_equiv.
destruct n as [| n]; try easy; intros _; apply lin_dep_S_zero.
Qed.

Lemma lin_indep_zero_equiv : {n}, lin_indep (0 : 'E^n) n = O.
Proof.
move=>>; rewrite -Nat.le_0_r -Nat.nlt_ge iff_not_r_equiv.
apply lin_dep_zero_equiv.
Qed.

Lemma lin_indep_nil_or_nonzero :
   {n} (B : 'E^n), lin_indep B n = O B 0.
Proof.
intros [| n]; [intros; left; easy |].
move=>> HB; right; contradict HB; rewrite HB; apply lin_dep_S_zero.
Qed.

Lemma lin_indep_S_nonzero : {n} {B : 'E^n.+1}, lin_indep B B 0.
Proof. move=>> /lin_indep_nil_or_nonzero [H | H]; easy. Qed.

Lemma lin_indep_nonnil_or_zero :
   {n} (B : 'E^n), lin_indep B (0 < n)%coq_nat B = 0.
Proof.
intros [| n]; [intros; right; apply nil_is_zero |].
move=>>; left; auto with arith.
Qed.

Lemma lin_indep_nonnil :
   {n} (B : 'E^n), lin_indep B B 0 (0 < n)%coq_nat.
Proof. move=>> /lin_indep_nonnil_or_zero [H | H]; easy. Qed.

Lemma lin_indep_nonnil_nonzero_equiv :
   {n} (B : 'E^n), lin_indep B (0 < n)%coq_nat B 0.
Proof.
intros n B HB; apply iff_sym; split; [apply lin_indep_nonnil; easy |].
destruct n as [| n]; try easy; intros _; apply lin_indep_S_nonzero; easy.
Qed.

Lemma lin_indep_nil_zero_equiv :
   {n} (B : 'E^n), lin_indep B n = O B = 0.
Proof.
intros; rewrite -Nat.le_0_r iff_not_equiv Nat.nle_gt.
apply lin_indep_nonnil_nonzero_equiv; easy.
Qed.

Lemma lin_indep_injF : {n} {B : 'E^n}, lin_indep B injective B.
Proof. move=>>; rewrite contra_equiv; apply lin_dep_not_injF. Qed.

Lemma lin_indep_castF_compat :
   {n1 n2} (H : n1 = n2) {B1 : 'E^n1},
    lin_indep B1 lin_indep (castF H B1).
Proof. move=>>; apply contra_equiv, lin_dep_castF_reg. Qed.

Lemma lin_indep_castF_reg :
   {n1 n2} (H : n1 = n2) {B1 : 'E^n1},
    lin_indep (castF H B1) lin_indep B1.
Proof. move=>>; apply contra_equiv, lin_dep_castF_compat. Qed.

Lemma lin_indep_castF_equiv :
   {n1 n2} (H : n1 = n2) {B1 : 'E^n1},
    lin_indep (castF H B1) lin_indep B1.
Proof. move=>>; apply iff_not_equiv, lin_dep_castF_equiv. Qed.

Lemma lin_indep_concatF_reg_l :
   {n1 n2} {B1 : 'E^n1} (B2 : 'E^n2),
    lin_indep (concatF B1 B2) lin_indep B1.
Proof. move=>>; apply contra_equiv; apply lin_dep_concatF_compat_l. Qed.

Lemma lin_indep_concatF_reg_r :
   {n1 n2} (B1 : 'E^n1) {B2 : 'E^n2},
    lin_indep (concatF B1 B2) lin_indep B2.
Proof. move=>>; apply contra_equiv; apply lin_dep_concatF_compat_r. Qed.

Lemma lin_indep_concatF_disjF :
   {n1 n2} {B1 : 'E^n1} {B2 : 'E^n2} x,
    lin_indep (concatF B1 B2) ¬ inF x B1 ¬ inF x B2.
Proof.
move=>>; rewrite -not_and_equiv contra_not_r_equiv.
intros [H1 H2]; eapply lin_dep_concatF_not_disjF; [apply H1 | easy].
Qed.

Lemma lin_indep_insertF_reg :
   {n} {B : 'E^n} x0 i0, lin_indep (insertF B x0 i0) lin_indep B.
Proof. move=>>; rewrite contra_equiv; apply lin_dep_insertF_compat. Qed.

Lemma lin_indep_skipF_compat :
   {n} {B : 'E^n.+1} i0, lin_indep B lin_indep (skipF B i0).
Proof. move=>>; rewrite contra_equiv; apply lin_dep_skipF_reg. Qed.

Lemma lin_indep_not_line :
   {n} {B : 'E^n},
    lin_indep B i j, i j ¬ line (B i) (B j).
Proof.
move=>> HB; move=>> Hi H; contradict HB;
    eapply lin_dep_line; [apply Hi | apply H].
Qed.

Lemma lin_indep_not_plane :
   {n} {B : 'E^n},
    lin_indep B i j k, i k j k ¬ plane (B i) (B j) (B k).
Proof.
move=>> HB; move=>> Hi Hj H; contradict HB;
    eapply lin_dep_plane; [apply Hi | apply Hj | apply H].
Qed.

Establish first the property on lin_indep.

Lemma lin_indep_coupleF_sym :
   (x0 x1 : E), lin_indep (coupleF x0 x1) lin_indep (coupleF x1 x0).
Proof.
move=>> H L; rewrite (coupleF_correct L) lc_coupleF; intros HL.
apply coupleF_zero_compat. apply (coupleF_zero_reg_r (L ord_max)).
2: apply (coupleF_zero_reg_l _ (L ord0)).
all: apply H; rewrite lc_coupleF plus_comm; easy.
Qed.

Lemma lin_indep_concatF_sym :
   {n1 n2} {B1 : 'E^n1} {B2 : 'E^n2},
    lin_indep (concatF B1 B2) lin_indep (concatF B2 B1).
Proof.
move=>> H L; specialize (H (concatF (lastF L) (firstF L))); revert H.
rewrite lc_concatF lc_splitF_l plus_comm; intros H HL.
specialize (H HL); apply concatF_zero_reg in H; apply splitF_zero_reg; easy.
Qed.

Lemma lin_indep_uniq_decomp :
   {n} {B : 'E^n}, lin_indep B lc_injL B.
Proof.
intros n B HB L L' HL%minus_zero_compat.
rewrite -lc_minus_l in HL; apply minus_zero_reg; auto.
Qed.

Lemma lin_indep_uniq_decomp_rev :
   {n} {B : 'E^n}, lc_injL B lin_indep B.
Proof.
intros n B HB L HL; apply HB; rewrite (lc_zero_compat_l 0); easy.
Qed.

Lemma lin_indep_uniq_decomp_equiv :
   {n} {B : 'E^n}, lin_indep B lc_injL B.
Proof.
intros; split. apply lin_indep_uniq_decomp. apply lin_indep_uniq_decomp_rev.
Qed.

Lemma lin_indep_nil : (B : 'E^0), lin_indep B.
Proof. intros B L HL; apply extF; intros [i Hi]; easy. Qed.

Lemma lin_indep_permutF :
   {n} {p} {B : 'E^n},
    bijective p lin_indep B lin_indep (permutF p B).
Proof.
intros n p B Hp HB L; rewrite {1}(permutF_f_inv_r Hp L) lc_permutF;
    try now apply bij_inj.
move⇒ /HB /extF_rev HL; apply extF; intros i.
specialize (HL (p i)); rewrite zeroF in HL; rewrite zeroF -HL.
unfold permutF; rewrite f_inv_can_l; easy.
Qed.

Lemma lin_indep_permutF_equiv :
   {n} {p} {B : 'E^n},
    bijective p lin_indep (permutF p B) lin_indep B.
Proof.
intros n p B Hp; split. 2: apply lin_indep_permutF; easy.
rewrite <- (permutF_can p (f_inv Hp) B), permutF_can.
apply lin_indep_permutF, f_inv_bij.
apply f_inv_can_l.
apply f_inv_can_r.
Qed.

Lemma lin_dep_coupleF_sym :
   (x0 x1 : E), lin_dep (coupleF x0 x1) lin_dep (coupleF x1 x0).
Proof. move=>>; rewrite -contra_equiv; apply lin_indep_coupleF_sym. Qed.

Lemma lin_dep_concatF_sym :
   {n1 n2} {B1 : 'E^n1} {B2 : 'E^n2},
    lin_dep (concatF B1 B2) lin_dep (concatF B2 B1).
Proof. move=>>; rewrite -contra_equiv; apply lin_indep_concatF_sym. Qed.

Lemma lin_dep_not_uniq_decomp :
   {n} {B : 'E^n}, lin_dep B ¬ lc_injL B.
Proof. move=>>; rewrite -contra_equiv; apply lin_indep_uniq_decomp_rev. Qed.

Lemma lin_dep_not_uniq_decomp_rev :
   {n} {B : 'E^n}, ¬ lc_injL B lin_dep B.
Proof. move=>>; rewrite -contra_equiv; apply lin_indep_uniq_decomp. Qed.

Lemma lin_dep_not_uniq_decomp_equiv :
   {n} {B : 'E^n}, lin_dep B ¬ lc_injL B.
Proof. move=>>; apply not_iff_compat, lin_indep_uniq_decomp_equiv. Qed.

Lemma lin_dep_nonnil : {n} (B : 'E^n), lin_dep B (0 < n)%coq_nat.
Proof.
move=>>; rewrite contra_not_l_equiv Nat.nlt_ge Nat.le_0_r.
intros; subst; apply lin_indep_nil.
Qed.

Mixed properties of lin_dep/lin_indep.
[GostiauxT1] Th 6.61, pp. 189-190. (=>)
Lemma lin_dep_insertF :
   {n} {B : 'E^n} {x0} i0, lin_span B x0 lin_dep (insertF B x0 i0).
Proof.
intros n B x0 i0 [L]; apply lin_dep_ex; (insertF L (- 1%K) i0); split.
rewrite lc_insertF scal_opp_l scal_one; apply: plus_opp_l.
rewrite -(insertF_zero i0); apply insertF_nextF_compat_r.
apply one_not_zero in HK; contradict HK; apply opp_inj; rewrite opp_zero; easy.
Qed.

Lemma lin_indep_insertF_rev :
   {n} {B : 'E^n} {x0} i0,
    lin_indep (insertF B x0 i0) ¬ lin_span B x0.
Proof. move=>>; rewrite contra_not_r_equiv; apply lin_dep_insertF. Qed.

End Linear_independent_Facts.

Section Linear_independent_sub_Facts1a.

Properties of lin_indep 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_indep_sub : lin_indep B lin_indep B_ms.
Proof.
intros HB1 L HL; apply HB1;
    rewrite mk_sub_lc in HL; apply mk_sub_inj in HL; easy.
Qed.

Lemma lin_indep_sub_rev : lin_indep B_ms lin_indep B.
Proof. intros HB1 L HL; apply HB1; apply val_inj; rewrite val_lc; easy. Qed.

Lemma lin_indep_sub_equiv : lin_indep B_ms lin_indep B.
Proof. split; [apply lin_indep_sub_rev | apply lin_indep_sub]. Qed.

End Linear_independent_sub_Facts1a.

Section Linear_independent_sub_Facts1c.

More properties of lin_indep 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_ms : 'PE_ms^n}.
Let B := mapF val B_ms.

Lemma lin_indep_val : lin_indep B_ms lin_indep B.
Proof.
rewrite -(lin_indep_sub_equiv HPE (in_subF B_ms)) -(mk_subF_eq B_ms); easy.
Qed.

Lemma lin_indep_val_rev : lin_indep B lin_indep B_ms.
Proof. rewrite (mk_subF_eq B_ms) (lin_indep_sub_equiv HPE); easy. Qed.

Lemma lin_indep_val_equiv : lin_indep B lin_indep B_ms.
Proof. rewrite (mk_subF_eq B_ms) (lin_indep_sub_equiv HPE); easy. Qed.

End Linear_independent_sub_Facts1c.