Newer
Older

François Clément
committed
(**
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].

François Clément
committed
#<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>#.

François Clément
committed
* 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.

François Clément
committed
*)
From Requisite Require Import stdlib_wR ssr_wMC.

François Clément
committed
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
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.

François Clément
committed
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.

François Clément
committed
(* . *)
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.

François Clément
committed
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
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.

François Clément
committed
(* . *)
right; left; apply lin_span_ex; exists (singleF (- / (L ord1) * (L ord0))).

François Clément
committed
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)).

François Clément
committed
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

François Clément
committed
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 :

François Clément
committed
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
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. *)

François Clément
committed
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.

François Clément
committed
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.

François Clément
committed
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.

François Clément
committed
1,2: apply invalF_coupleF_sym.
Qed.

François Clément
committed
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.

François Clément
committed
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.

François Clément
committed
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. (<=) *)

François Clément
committed
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.

François Clément
committed
Proof.
move=> n i0 x0 B HB /lin_dep_ex [L [HL1 HL2]];

François Clément
committed
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.

François Clément
committed
(* *)
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.

François Clément
committed
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. (<=>) *)

François Clément
committed
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.

François Clément
committed
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).

François Clément
committed
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.

François Clément
committed
Proof. move=>>; rewrite iff_not_r_equiv; apply lin_dep_insertF_equiv. Qed.
(**
#<A HREF="##GostiauxT1">#[[GostiauxT1]]#</A>#
Th 6.62, pp. 190-192. *)

François Clément
committed
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.

François Clément
committed
(* *)
destruct (classic (L ord0 = 0)) as [HL | HL].
(* . *)
eapply lin_dep_ext; try apply (insertF_skipF ord_max).

François Clément
committed
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).

François Clément
committed
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)).

François Clément
committed
assert (HD : lin_dep D).
apply (IHn (skipF0 B) _ M1); intros; unfold D, skipF.

François Clément
committed
symmetry; rewrite -plus_minus_r_equiv HC (lc_skipF ord0).
rewrite HCj0 scal_minus_r -lc_scal_l 2!scal_assoc mult_comm_R.

François Clément
committed
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
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.

François Clément
committed
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.