Library Algebra.Finite_dim.Finite_dim_AS_aff_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.
Support for affine independent finite families in affine spaces.
Some results are only valid when the ring of scalars is commutative, or being
ordered, they are only stated in the case of the ring of real numbers R_Ring.
This module may be used through the import of
Algebra.Finite_dim.Finite_dim_AS, Algebra.Finite_dim.Finite_dim,
Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.
Brief description
Description
Usage
From Requisite Require Import ssr_wMC.
From Coquelicot Require Import Hierarchy.
Close Scope R_scope.
From Subsets Require Import Subsets_wDep.
From Algebra Require Import Hierarchy_compl.
From Algebra Require Import Monoid Group Ring ModuleSpace AffineSpace.
From Algebra Require Import Finite_dim_MS.
From Algebra Require Import Finite_dim_AS_def Finite_dim_AS_aff_gen.
Local Open Scope Monoid_scope.
Local Open Scope Group_scope.
Local Open Scope Ring_scope.
Local Open Scope ModuleSpace_scope.
Local Open Scope AffineSpace_scope.
Section Affine_span_Affine_Facts.
Context {K : Ring}.
Context {V : ModuleSpace K}.
Context {E : AffineSpace V}.
Lemma aff_indep_alt :
∀ {n} {A : 'E^n.+1} i0, lin_indep (frameF A i0) → aff_indep A.
Proof.
intros n A i0 HA i; destruct (ord_eq_dec i i0) as [Hi | Hi]; try now rewrite Hi.
destruct n as [| n]; [contradict Hi; rewrite !I_1_is_unit; easy |].
intros L; unfold frameF; rewrite (vectF_change_orig (A i0))
lc_plus_r lc_constF_r scal_opp -vect_sym vectF_skipF.
rewrite -lc_insertF_l (lc_skip_zero_r i0 (vectF_zero_alt _ _)).
move⇒ /HA /extF_rev HL1.
assert (HL1a : skipF L (insert_ord (not_eq_sym Hi)) = 0).
apply skipF_zero_compat; move⇒ j /skip_insert_ord_neq Hj.
specialize (HL1 (insert_ord Hj)).
rewrite skipF_correct insertF_correct in HL1; easy.
apply (extF_zero_skipF _ (insert_ord (not_eq_sym Hi))); try easy.
rewrite -sum_one // opp_zero_equiv; move: (HL1 (insert_ord Hi)).
rewrite zeroF skipF_correct insertF_correct_l; easy.
Qed.
Lemma aff_dep_alt :
∀ {n} {A : 'E^n.+1} i0, lin_dep (frameF A i0) → aff_dep A.
Proof. move=>>; rewrite -contra_equiv; easy. Qed.
Lemma baryc_coord_uniq :
∀ {n} L1 L2 (A : 'E^n.+1),
aff_indep A → sum L1 = 1 → sum L2 = 1 →
barycenter L1 A = barycenter L2 A → L1 = L2.
Proof.
intros n L1 L2 A HA HL1 HL2 HL.
assert (HL' : liftF_S L1 = liftF_S L2).
rewrite -!skipF_first; apply minus_zero_reg, (HA ord0).
rewrite lc_minus_l; apply: minus_zero_compat.
rewrite -!(lc_vectF_skipF ord0) -!(baryc_correct_orig (A ord0));
[| apply invertible_eq_one; easy..].
rewrite HL1 HL2 HL; easy.
apply (eqxF_reg _ ord0).
apply (plus_reg_r (sum (liftF_S L1))).
rewrite {2}HL' -!sum_ind_l HL2; easy.
apply liftF_S_reg; easy.
Qed.
End Affine_span_Affine_Facts.
Section AffineSpace_FD_R_Facts.
Context {V : ModuleSpace R_Ring}.
Context {E : AffineSpace V}.
Lemma aff_indep_monot :
∀ {n1 n2} {A1 : 'E^n1.+1} {A2 : 'E^n2.+1},
injective A1 → invalF A1 A2 → aff_indep A2 → aff_indep A1.
Proof.
intros n1 n2 A1 A2 HA1 HA HA2; destruct (HA ord0) as [i2 Hi2].
apply (aff_indep_alt ord0), (lin_indep_monot (frameF A2 i2)); try easy.
apply frameF_inj_equiv, skipF_inj; easy.
apply frameF_invalF_equiv; [| apply skipF_invalF]; easy.
Qed.
Lemma aff_dep_monot :
∀ {n1 n2} {A1 : 'E^n1.+1} {A2 : 'E^n2.+1},
injective A1 → invalF A1 A2 → aff_dep A1 → aff_dep A2.
Proof.
move=>> HA1 HA; rewrite -contra_equiv; apply aff_indep_monot; easy.
Qed.
Lemma aff_indep_skipF :
∀ {n} {A : 'E^n.+2} i0, aff_indep A → aff_indep (skipF A i0).
Proof.
intros n A i0 HA; destruct (ord_eq_dec i0 ord0) as [Hi0 | Hi0]; [subst |].
apply (aff_indep_alt ord_max); rewrite -(insert_ord_max ord_max_not_0).
rewrite frameF_skipF_alt; apply lin_indep_skipF_compat; easy.
apply (aff_indep_alt ord0); rewrite -(insert_ord_0 (not_eq_sym Hi0)).
rewrite frameF_skipF; apply lin_indep_skipF_compat; easy.
Qed.
Lemma aff_indep_permutF :
∀ {n} {A : 'E^n.+1} p,
bijective p → aff_indep A → aff_indep (permutF p A).
Proof.
intros n A p Hp HA i0; apply (aff_indep_alt (p i0)).
rewrite (frameF_permutF (bij_inj Hp)); apply lin_indep_permutF; [| easy].
apply skip_f_ord_bij.
Qed.
Lemma aff_indep_permutF_rev :
∀ {n} {A : 'E^n.+1} p,
bijective p → aff_indep (permutF p A) → aff_indep A.
Proof.
intros n A p Hp; rewrite {2}(permutF_f_inv_l Hp A).
apply aff_indep_permutF, f_inv_bij.
Qed.
Lemma aff_indep_permutF_equiv :
∀ {n} {A : 'E^n.+1} p,
bijective p → aff_indep A ↔ aff_indep (permutF p A).
Proof.
intros; split; [apply aff_indep_permutF | apply aff_indep_permutF_rev]; easy.
Qed.
End AffineSpace_FD_R_Facts.
Section ModuleSpace_AffineSpace_R_Facts.
Context {E : ModuleSpace R_Ring}.
Definition affine_independent {n} (A : 'E^n.+1) :=
lin_indep (liftF_S A - constF n (A ord0)).
Lemma affine_independent_equiv :
∀ {n} (A : 'E^n.+1), affine_independent A ↔ aff_indep A.
Proof.
intros n A; split; intros HA.
apply (aff_indep_alt ord0); unfold frameF; rewrite skipF_first; easy.
unfold affine_independent; rewrite -skipF_first; apply HA.
Qed.
Lemma affine_independent_skipF :
∀ {n} {A : 'E^n.+2} i0,
affine_independent A → affine_independent (skipF A i0).
Proof.
move=>>; rewrite !affine_independent_equiv; apply aff_indep_skipF.
Qed.
Lemma affine_independent_permutF :
∀ {n} {A : 'E^n.+1} p,
bijective p → affine_independent A → affine_independent (permutF p A).
Proof.
move=>>; rewrite !affine_independent_equiv; apply aff_indep_permutF.
Qed.
Lemma affine_independent_permutF_rev :
∀ {n} {A : 'E^n.+1} p,
bijective p → affine_independent (permutF p A) → affine_independent A.
Proof.
move=>>; rewrite !affine_independent_equiv; apply aff_indep_permutF_rev.
Qed.
Lemma affine_independent_permutF_equiv :
∀ {n} {A : 'E^n.+1} p,
bijective p → affine_independent A ↔ affine_independent (permutF p A).
Proof.
move=>>; rewrite !affine_independent_equiv; apply aff_indep_permutF_equiv.
Qed.
Lemma affine_independent_revF_equiv :
∀ {n} {A : 'E^n.+1},
affine_independent A ↔ affine_independent (revF A).
Proof. intros; apply affine_independent_permutF_equiv, rev_ord_bij. Qed.
Lemma affine_independent_moveF_equiv :
∀ {n} {A : 'E^n.+1} i0 i1,
affine_independent A ↔ affine_independent (moveF A i0 i1).
Proof. intros; apply affine_independent_permutF_equiv, move_ord_bij. Qed.
Lemma affine_independent_transpF_equiv :
∀ {n} {A : 'E^n.+1} i0 i1,
affine_independent A ↔ affine_independent (transpF A i0 i1).
Proof. intros; apply affine_independent_permutF_equiv, transp_ord_bij. Qed.
Lemma affine_independent_lc :
∀ {n} L1 L2 (A : 'E^n.+1),
affine_independent A →
sum L1 = sum L2 → lin_comb L1 A = lin_comb L2 A → L1 = L2.
Proof.
intros n L1 L2 A HA HL HLA.
assert (H : skipF L1 ord0 = skipF L2 ord0).
rewrite 2!skipF_first.
apply minus_zero_reg, HA; rewrite lc_minus_l 2!lc_minus_r.
apply: minus_zero_compat.
rewrite (minus_plus_l_eq (scal (L1 ord0) (A ord0))).
rewrite (minus_plus_l_eq (scal (L2 ord0) (A ord0)) (lin_comb (_ L2) _)).
rewrite -2!lc_ind_l HLA; f_equal.
rewrite 2!lc_constF_r -2!scal_distr_r -2!sum_ind_l HL; easy.
apply (extF_skipF ord0); try easy.
apply plus_reg_r with (sum (skipF L1 ord0)); rewrite {2}H.
rewrite -2!(sum_skipF _ ord0); easy.
Qed.
End ModuleSpace_AffineSpace_R_Facts.