Finite_dim_MS_lin_indep_R.v

(**
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

 #<DIV><A NAME="GostiauxT1"></A></DIV>#
 [[GostiauxT1]]
 Bernard Gostiaux,
 Cours de mathématiques spéciales - 1. Algèbre,
 Mathématiques, Presses Universitaires de France, Paris, 1993,
 #<A HREF="https://www.puf.com/cours-de-mathematiques-speciales-tome-1-algebre">#
 https://www.puf.com/cours-de-mathematiques-speciales-tome-1-algebre#</A>#.

 * 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 :
  forall {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 _]]].
exists L2; split; try now rewrite -HL2a.
destruct (nextF_rev _ _ HL1b) as [i1 Hi1], (invalF_fun HL2b) as [f Hf1].
apply nextF; exists (f i1); rewrite -Hf1; easy.
(* *)
intros _ _ _; apply lin_dep_not_injF; try easy.
apply nonzero_struct_R.
Qed.

Lemma lin_dep_equiv_injF :
  forall {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_2_equiv :
  forall {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; extF i; destruct (ord2_dec i) as [Hi | Hi]; rewrite Hi; easy.
(* . *)
apply lin_span_ex; exists (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 exists ord0. apply nonzero_struct_R.
apply (lin_dep_line nonzero_struct_R ord_0_not_max HB).
Qed.

Lemma lin_dep_coupleF_equiv :
  forall {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 :
  forall {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; extF i;
  destruct (ord3_dec i) as [[Hi | Hi] | Hi]; rewrite Hi; easy.
(* . *)
right; left; apply lin_span_ex; exists (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;
    exists (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_plus_r -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 exists 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 :
  forall {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 :
  forall {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 :
  forall {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_2_equiv :
  forall {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 :
  forall {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 :
  forall {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 :
  forall {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 :
  forall {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_1_equiv :
  forall {n} (B : 'E^n), n = 1%nat -> lin_indep B <-> B <> 0.
Proof.
intros n B Hn; subst; split; [apply lin_indep_S_nonzero, nonzero_struct_R |].
move=> /nextF_rev [i HB] L; rewrite ord_one in HB; rewrite lc_1.
move=> /(scal_zero_reg_l _ _ HB); rewrite invertible_equiv_R NNPP_equiv.
apply extF_zero_1; easy.
Qed.

Lemma lin_indep_singleF_equiv :
  forall {x0 : E}, lin_indep (singleF x0) <-> x0 <> 0.
Proof. intros; rewrite lin_indep_1_equiv// singleF_zero_equiv//. Qed.

Lemma lin_indep_coupleF_sym :
  forall {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 :
  forall {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_1_equiv :
  forall {n} (B : 'E^n), n = 1%nat -> lin_dep B <-> B = 0.
Proof. intros; apply iff_not_l_equiv, lin_indep_1_equiv; easy. Qed.

Lemma lin_dep_singleF_equiv : forall {x0 : E}, lin_dep (singleF x0) <-> x0 = 0.
Proof. intros; rewrite lin_dep_1_equiv// singleF_zero_equiv//. Qed.

Lemma lin_dep_coupleF_sym :
  forall {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. *)

(**
 #<A HREF="##GostiauxT1">#[[GostiauxT1]]#</A>#
 Th 6.61, pp. 189-190. (<=) *)
Lemma lin_dep_insertF_rev :
  forall {n} i0 {x0} {B : 'E^n},
    lin_indep B -> lin_dep (insertF i0 x0 B) -> lin_span B x0.
Proof.
move=> n i0 x0 B 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; exists (scal (/ - L i0) (skipF i0 L)); 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.

(**
 #<A HREF="##GostiauxT1">#[[GostiauxT1]]#</A>#
 Th 6.61, pp. 189-190. (<=>) *)
Lemma lin_dep_insertF_equiv :
  forall {n} i0 {x0} {B : 'E^n},
    lin_indep B -> lin_dep (insertF i0 x0 B) <-> 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 :
  forall {n} i0 {x0} {B : 'E^n},
    lin_indep B -> ~ lin_span B x0 -> lin_indep (insertF i0 x0 B).
Proof.
move=>> HB; rewrite contra_not_l_equiv; apply lin_dep_insertF_rev; easy.
Qed.

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

(**
 #<A HREF="##GostiauxT1">#[[GostiauxT1]]#</A>#
 Th 6.62, pp. 190-192. *)
Lemma lin_dep_S_lin_span :
  forall {n} (B : 'E^n) {C : 'E^n.+1}, inclF C (lin_span B) -> lin_dep C.
Proof.
move=> n B C /lin_spanF_ex_flipT [L HC]; induction n as [| n IHn].
(* *)
apply lin_dep_ex; exists 1; split; try apply ones_not_zero_R.
apply lc_zero_compat_r; extF 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 j0 (L ord0)); pose (L1 := skipF0 L);
    pose (L2 := skipT ord0 j0 L).
pose (M0 := scal (/ L ord0 j0) L0);
    pose (M1 i j := - (M0 j * L1 i j0) + L2 i j).
pose (D j := skipF j0 C j - scal (M0 j) (C j0)).
assert (HD : lin_dep D).
  apply (IHn (skipF0 B) _ M1); intros; unfold D, skipF.
  symmetry; rewrite -plus_minus_r_equiv HC (lc_skipF ord0).
  rewrite HCj0 scal_minus_r -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; exists LL; split; try now rewrite HLL1.
apply (neqxF_reg j0), skipF_neqxF_reg; rewrite HLL2; easy.
Qed.

Lemma lin_dep_gt_lin_span :
  forall {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 :
  forall {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.
move=> Hf1 L /fun_ext_rev HL; extF i.
rewrite -lc_l_kron_r (lc_scalF_compat _ _ (scalF_comm_R _ _)).
destruct (Hf1 (kron 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.


Section Linear_independent_Euclidean_space_R_Facts.

Context {d : nat}.
Hypothesis Hd : d = 0.

Lemma FR0_lin_indep : lin_indep (singleF ((fun=> 1) : FRd d)).
Proof. apply FT0_lin_indep. Qed.

Lemma FR0_dual_lin_indep : lin_indep (singleF (fun f : FRd d => f 0)).
Proof. apply: FT0_dual_lin_indep. Qed.

End Linear_independent_Euclidean_space_R_Facts.