Library Algebra.Finite_dim.Finite_dim_MS_lin_indep_R

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 of module spaces on the ring of real numbers.

Description

Some results need that the ring of scalars is commutative, or being ordered. Such results are stated here in the case of the ring of real numbers R_Ring.
For generic results that do not need additional assumption on the ring of scalars, see Algebra.Finite_dim.Finite_dim_MS_lin_indep.

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_wR 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 Finite_dim_MS_lin_span.
From Algebra Require Import Finite_dim_MS_lin_indep.

Local Open Scope R_scope.
Local Open Scope Monoid_scope.
Local Open Scope Group_scope.
Local Open Scope Ring_scope.
Local Open Scope ModuleSpace_scope.

Section Linear_independent_R_Facts1.

Properties of lin_dep/lin_indep on R module spaces.
Establish first the property on lin_dep.

Context {E : ModuleSpace R_Ring}.

Lemma lin_dep_monot :
   {n1 n2} (B1 : 'E^n1) {B2 : 'E^n2},
    injective B1 invalF B1 B2 lin_dep B1 lin_dep B2.
Proof.
intros n1 n2 B1 B2; destruct (classic (injective B2)) as [HB2 | HB2].
rewrite 2!lin_dep_ex; intros HB1 HB [L1 [HL1a HL1b]].
destruct (lc_invalF_injF L1 _ _ HB1 HB2 HB) as [L2 [HL2a [HL2b _]]].
L2; split; try now rewrite -HL2a.
destruct (nextF_rev _ _ HL1b) as [i1 Hi1], (invalF_fun HL2b) as [f Hf1].
apply nextF; (f i1); rewrite -Hf1; easy.
intros _ _ _; apply lin_dep_not_injF; try easy.
apply nonzero_struct_R.
Qed.

Lemma lin_dep_equiv_injF :
   {n1 n2} (B1 : 'E^n1) (B2 : 'E^n2),
    injective B1 injective B2 invalF B1 B2 invalF B2 B1
    lin_dep B1 lin_dep B2.
Proof. intros; split; apply lin_dep_monot; easy. Qed.

Lemma lin_dep_1_equiv : {B : 'E^1}, lin_dep B B ord0 = 0.
Proof.
move=>>; split.
rewrite lin_dep_ex; move⇒ [L [HL /nextF_rev [i Hi]]];
    rewrite I_1_is_unit in Hi.
rewrite lc_1 in HL; apply (scal_zero_reg_r_R (L ord0)); easy.
intros; apply lin_dep_with_zero; try now ord0.
apply nonzero_struct_R.
Qed.

Lemma lin_dep_singleF_equiv : {x0 : E}, lin_dep (singleF x0) x0 = 0.
Proof. intros; rewrite lin_dep_1_equiv singleF_0; easy. Qed.

Lemma lin_dep_2_equiv :
   {B : 'E^2}, lin_dep B B ord0 = 0 line (B ord0) (B ord_max).
Proof.
move=>>; split.
move⇒ /lin_dep_ex [L [HL HL0]]; rewrite lc_2 in HL.
destruct (Req_dec (L ord_max) 0) as [HL0' | HL0']; [left | right].
rewrite HL0' scal_zero_l plus_zero_r in HL.
apply scal_zero_rev_R in HL; destruct HL as [HL | HL]; try easy.
contradict HL0; apply extF; intros i;
    destruct (ord2_dec i) as [Hi | Hi]; rewrite Hi; easy.
apply lin_span_ex; (singleF (- (/ L ord_max) × (L ord0))).
rewrite lc_1 2!singleF_0.
apply (scal_reg_r_R (L ord_max)); try easy.
rewrite plus_comm in HL.
move: HL ⇒ /plus_is_zero_l HL; rewrite HL.
rewrite -scal_opp_l scal_assoc; f_equal.
apply invertible_equiv_R in HL0'.
rewrite mult_assoc -opp_mult_r -opp_mult_l mult_inv_r// mult_one_l; easy.
move⇒ [HB | HB].
apply lin_dep_with_zero; try now ord0. apply nonzero_struct_R.
apply (lin_dep_line nonzero_struct_R ord_0_not_max HB).
Qed.

Lemma lin_dep_coupleF_equiv :
   {x0 x1 : E}, lin_dep (coupleF x0 x1) x0 = 0 line x0 x1.
Proof. intros; rewrite lin_dep_2_equiv coupleF_0 coupleF_1; easy. Qed.

Lemma lin_dep_3_equiv :
   {B : 'E^3}, lin_dep B
    B ord0 = 0 line (B ord0) (B ord1)
    plane (B ord0) (B ord1) (B ord_max).
Proof.
move=>>; split.
move⇒ /lin_dep_ex [L [HL HL0]]; rewrite lc_3 in HL.
destruct (Req_dec (L ord_max) 0) as [HL0a | HL0a];
    try rewrite HL0a scal_zero_l plus_zero_r in HL.
destruct (Req_dec (L ord1) 0) as [HL0b | HL0b];
    try rewrite HL0b scal_zero_l plus_zero_r in HL.
left; apply (scal_zero_reg_r_R (L ord0)); try easy.
contradict HL0; apply extF; intros i.
destruct (ord3_dec i) as [[Hi | Hi] | Hi]; rewrite Hi; easy.
right; left; apply lin_span_ex; (singleF (- / (L ord1) × (L ord0))).
apply (scal_reg_r_R (L ord1) _ _ HL0b).
move: HL ⇒ /plus_is_zero_r HL.
rewrite HL lc_1 2!singleF_0 -opp_mult_l
    scal_opp_l scal_opp_r scal_assoc mult_assoc; do 2 f_equal.
apply invertible_equiv_R in HL0b.
rewrite mult_inv_r// mult_one_l; easy.
right; right; apply lin_span_ex;
     (coupleF (- / L ord_max × L ord0) (- / L ord_max × L ord1)).
apply (scal_reg_r_R (L ord_max) _ _ HL0a).
move: HL ⇒ /plus_is_zero_r HL.
rewrite HL opp_plus lc_2 2!coupleF_0 2!coupleF_1.
apply invertible_equiv_R in HL0a.
rewrite scal_distr_l -2!opp_mult_l 2!scal_opp_l 2!scal_opp_r
  2!scal_assoc 2!mult_assoc mult_inv_r// 2!mult_one_l; easy.
move⇒ [HB | [HB | HB]].
apply lin_dep_with_zero; try now ord0. apply nonzero_struct_R.
apply (lin_dep_line nonzero_struct_R ord_0_not_1 HB).
apply (lin_dep_plane nonzero_struct_R ord_0_not_max ord_1_not_max HB).
Qed.

Lemma lin_dep_tripleF_equiv :
   {x0 x1 x2 : E},
    lin_dep (tripleF x0 x1 x2) x0 = 0 line x0 x1 plane x0 x1 x2.
Proof.
intros; rewrite lin_dep_3_equiv tripleF_0 tripleF_1 tripleF_2; easy.
Qed.

Lemma lin_indep_monot :
   {n1 n2} {B1 : 'E^n1} (B2 : 'E^n2),
    injective B1 invalF B1 B2 lin_indep B2 lin_indep B1.
Proof. move=>> HB1 HB; apply contra_equiv; apply lin_dep_monot; easy. Qed.

Lemma lin_indep_equiv_injF :
   {n1 n2} (B1 : 'E^n1) (B2 : 'E^n2),
    injective B1 injective B2 invalF B1 B2 invalF B2 B1
    lin_indep B1 lin_indep B2.
Proof. intros; split; apply lin_indep_monot; easy. Qed.

Lemma lin_indep_1_equiv : {B : 'E^1}, lin_indep B B ord0 0.
Proof. intros; apply iff_not_r_equiv, lin_dep_1_equiv. Qed.

Lemma lin_indep_singleF_equiv :
   {x0 : E}, lin_indep (singleF x0) x0 0.
Proof. intros; rewrite lin_indep_1_equiv singleF_0; easy. Qed.

Lemma lin_indep_2_equiv :
   {B : 'E^2},
    lin_indep B B ord0 0 ¬ line (B ord0) (B ord_max).
Proof.
intros; rewrite -not_or_equiv; apply iff_not_r_equiv, lin_dep_2_equiv.
Qed.

Lemma lin_indep_coupleF_equiv :
   {x0 x1 : E},
    lin_indep (coupleF x0 x1) x0 0 ¬ line x0 x1.
Proof. intros; rewrite lin_indep_2_equiv coupleF_0 coupleF_1; easy. Qed.

Lemma lin_indep_3_equiv :
   {B : 'E^3}, lin_indep B
    B ord0 0 ¬ line (B ord0) (B ord1)
    ¬ plane (B ord0) (B ord1) (B ord_max).
Proof.
intros; rewrite -not_or3_equiv; apply iff_not_r_equiv, lin_dep_3_equiv.
Qed.

Lemma lin_indep_tripleF_equiv :
   {x0 x1 x2 : E},
    lin_indep (tripleF x0 x1 x2)
    x0 0 ¬ line x0 x1 ¬ plane x0 x1 x2.
Proof.
intros; rewrite lin_indep_3_equiv tripleF_0 tripleF_1 tripleF_2; easy.
Qed.

Establish first the property on lin_indep.

Lemma lin_indep_equiv :
   {n1 n2} (B1 : 'E^n1) (B2 : 'E^n2),
    n1 = n2 invalF B1 B2 invalF B2 B1
    lin_indep B1 lin_indep B2.
Proof.
intros n1 n2 B1 B2 Hn HB12 HB21; split; intros HBa;
    move: (lin_indep_injF nonzero_struct_R HBa) ⇒ HBb.
apply (lin_indep_monot B1); try apply (injF_equiv B1); easy.
apply (lin_indep_monot B2); try apply (injF_equiv B2); easy.
Qed.

Lemma lin_indep_coupleF_sym :
   {x0 x1 : E}, lin_indep (coupleF x0 x1) lin_indep (coupleF x1 x0).
Proof.
intros x0 x1 H; apply (lin_indep_equiv (coupleF x0 x1)); try easy.
1,2: apply invalF_coupleF_sym.
Qed.

Lemma lin_dep_equiv :
   {n1 n2} (B1 : 'E^n1) (B2 : 'E^n2),
    n1 = n2 invalF B1 B2 invalF B2 B1
    lin_dep B1 lin_dep B2.
Proof. intros; rewrite -iff_not_equiv; apply lin_indep_equiv; easy. 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.

Mixed properties of lin_dep/lin_indep.
[GostiauxT1] Th 6.61, pp. 189-190. (<=)
Lemma lin_dep_insertF_rev :
   {n} {B : 'E^n} {x0} i0,
    lin_indep B lin_dep (insertF B x0 i0) lin_span B x0.
Proof.
moven B x0 i0 HB /lin_dep_ex [L [HL1 HL2]];
    rewrite lc_insertF_r in HL1.
destruct (Hierarchy.eq_dec (L i0) 0) as [HL3 | HL3].
rewrite HL3 scal_zero_l plus_zero_l in HL1.
apply HB in HL1; contradict HL2.
apply (extF_zero_skipF _ i0); easy.
assert (HL3' : - L i0 0) by now rewrite -opp_zero; apply opp_neq_compat.
apply lin_span_ex; (scal (/ - L i0) (skipF L i0)); symmetry.
apply (scal_reg_r_R (- L i0)); try easy.
rewrite lc_scal_l scal_assoc scal_opp_l; apply plus_is_zero_l.
apply invertible_equiv_R in HL3'.
rewrite mult_inv_r// scal_one plus_comm; easy.
Qed.

[GostiauxT1] Th 6.61, pp. 189-190. (<=>)
Lemma lin_dep_insertF_equiv :
   {n} {B : 'E^n} {x0} i0,
    lin_indep B lin_dep (insertF B x0 i0) lin_span B x0.
Proof.
intros; split; [apply lin_dep_insertF_rev; easy |
    apply lin_dep_insertF, nonzero_struct_R].
Qed.

Lemma lin_indep_insertF :
   {n} {B : 'E^n} {x0} i0,
    lin_indep B ¬ lin_span B x0 lin_indep (insertF B x0 i0).
Proof.
move=>> HB; rewrite contra_not_l_equiv; apply lin_dep_insertF_rev; easy.
Qed.

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

[GostiauxT1] Th 6.62, pp. 190-192.
Lemma lin_dep_S_lin_span :
   {n} (B : 'E^n) {C : 'E^n.+1}, inclF C (lin_span B) lin_dep C.
Proof.
moven B C /lin_spanF_ex_flipT [L HC]; induction n as [| n IHn].
apply lin_dep_ex; ones; split; try apply ones_not_zero_R.
apply lc_zero_compat_r, extF; intros i; rewrite HC; apply lc_nil.
destruct (classic (L ord0 = 0)) as [HL | HL].
eapply lin_dep_ext; try apply (insertF_skipF _ ord_max).
apply lin_dep_insertF_compat; rewrite skipF_last; eapply IHn; intros j.
unfold widenF_S; rewrite (HC (widen_S j)).
rewrite (lc_skipF ord0) HL scal_zero_l plus_zero_l; easy.
destruct (nextF_rev _ _ HL) as [j0 Hj0]; rewrite zeroF in Hj0; clear HL.
generalize (HC j0); rewrite (lc_skipF ord0); intros HCj0.
apply axpy_equiv_R in HCj0; try easy; rewrite -lc_scal_l in HCj0.
pose (L0 := skipF (L ord0) j0); pose (L1 := skipF L ord0);
    pose (L2 := skipT L ord0 j0).
pose (M0 := scal (/ L ord0 j0) L0);
    pose (M1 i j := - (M0 j × L1 i j0) + L2 i j).
pose (D j := skipF C j0 j - scal (M0 j) (C j0)).
assert (HD : lin_dep D).
  apply (IHn (skipF B ord0) _ M1); intros; unfold D, skipF.
  symmetry; rewrite -plus_minus_r_equiv HC (lc_skipF ord0).
  rewrite HCj0 scal_minus_distr_l -lc_scal_l 2!scal_assoc mult_comm_R.
  rewrite -plus_assoc -lc_opp_l -lc_plus_l -inv_eq_R; easy.
apply lin_dep_ex in HD; destruct HD as [N [HN1 HN2]]; unfold D in HN1.
rewrite lc_minus_r minus_sym -scal_lc_l -scal_opp_l in HN1.
destruct (lc_skipF_ex_l (- lin_comb N M0) N C j0) as [LL [HLL1 [_ HLL2]]].
apply lin_dep_ex; LL; split; try now rewrite HLL1.
apply (neqxF_reg j0), skipF_neqxF_reg; rewrite HLL2; easy.
Qed.

Lemma lin_dep_gt_lin_span :
   {n1 n2} (B1 : 'E^n1) {B2 : 'E^n2},
    (n1 < n2)%coq_nat inclF B2 (lin_span B1) lin_dep B2.
Proof.
move=>> /ltP Hn HB; apply lin_dep_castF_reg with (eq_sym (subnKC Hn)).
eapply lin_dep_ext; try (symmetry; apply concatF_splitF).
eapply lin_dep_concatF_compat_l, lin_dep_S_lin_span; intros i2.
unfold firstF, castF; apply HB.
Qed.

Lemma lin_indep_le_lin_gen :
   {n1 n2} (PE : E Prop) (B1 : 'E^n1) (B2 : 'E^n2),
    inclF B1 PE lin_indep B1 lin_gen PE B2 (n1 n2)%coq_nat.
Proof.
intros n1 n2 PE B1 B2 HB1a HB1b HB2; rewrite HB2 in HB1a.
destruct (lt_dec n2 n1) as [Hn | Hn].
contradict HB1b; apply (lin_dep_gt_lin_span _ Hn HB1a).
apply Nat.nlt_ge; easy.
Qed.

End Linear_independent_R_Facts1.

Section Linear_independent_R_Facts2.

Context {E F : ModuleSpace R_Ring}.
Variable PE : E Prop.

Context {n : nat}.
Context {f : E 'R^n}.
Hypothesis Hf : lin_map f.

Lemma lin_indep_scatter : surjS PE fullset f lin_indep (scatter f).
Proof.
moveHf1 L /fun_ext_rev HL; apply extF; intros i.
rewrite -lc_kron_l_in_r (lc_scalF_compat _ _ (scalF_comm_R _ _)).
destruct (Hf1 (kronR i)) as [x [Hx Hf2]]; [easy |].
rewrite -Hf2 zeroF -(fct_zero_eq x) -HL fct_lc_r_eq; easy.
Qed.

End Linear_independent_R_Facts2.