Finite_dim_AS_aff_indep.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 affine independent finite families in affine spaces.

 * Description

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

 * Usage

 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.
*)

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.
From Algebra Require Import Finite_dim_AS_aff_span 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_indep_Affine_Facts.

Context {K : Ring}.
Context {V : ModuleSpace K}.
Context {E : AffineSpace V}.

Lemma aff_indep_any :
  forall {n} i0 i {A : 'E^n.+1},
    lin_indep (frameF i0 A) -> lin_indep (frameF i A).
Proof.
intros n i0 i A HA; destruct (ord_eq_dec i i0) as [Hi | Hi]; try now rewrite Hi.
destruct n as [| n]; [contradict Hi; rewrite !ord_one; 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 (insert_ord (not_eq_sym Hi)) L = 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_indep_all :
  forall {n} i {A : 'E^n.+1}, aff_indep A -> lin_indep (frameF i A).
Proof. move=>>; apply aff_indep_any. Qed.

Lemma aff_indep_all_equiv :
  forall {n} {A : 'E^n.+1}, aff_indep A <-> forall i, lin_indep (frameF i A).
Proof.
intros; split; [intros; apply aff_indep_all; easy | intros H; apply H].
Qed.

Lemma aff_indep_lin_indep :
  forall {n} i0 {A : 'E^n.+1}, lin_indep (frameF i0 A) -> aff_indep A.
Proof. move=> n i0 A /(aff_indep_any i0 ord0); easy. Qed.

Lemma aff_indep_lin_indep_rev :
  forall {n} i0 {A : 'E^n.+1}, aff_indep A -> lin_indep (frameF i0 A).
Proof. move=>>; apply aff_indep_any. Qed.

Lemma aff_indep_lin_indep_equiv :
  forall {n} i0 {A : 'E^n.+1}, aff_indep A <-> lin_indep (frameF i0 A).
Proof.
intros; split; [apply aff_indep_lin_indep_rev | apply aff_indep_lin_indep].
Qed.

Lemma lin_indep_aff_indep_equiv :
  forall {n} i0 (O : E) {u : 'V^n},
    lin_indep u <-> aff_indep (inv_frameF i0 O u).
Proof.
intros n i0 O u; rewrite (aff_indep_lin_indep_equiv i0) frameF_inv_frameF//.
Qed.

Lemma lin_indep_aff_indep :
  forall {n} i0 (O : E) {u : 'V^n},
    aff_indep (inv_frameF i0 O u) -> lin_indep u.
Proof. move=>>; apply lin_indep_aff_indep_equiv. Qed.

Lemma lin_indep_aff_indep_rev :
  forall {n} i0 (O : E) {u : 'V^n},
    lin_indep u -> aff_indep (inv_frameF i0 O u).
Proof. move=>>; apply lin_indep_aff_indep_equiv. Qed.

Lemma aff_dep_any :
  forall {n} i0 {A : 'E^n.+1},
    (exists i, lin_dep (frameF i A)) -> lin_dep (frameF i0 A).
Proof.
intros n i0 A; rewrite contra_not_r_equiv not_ex_not_all_equiv.
intros; apply (aff_indep_any i0); easy.
Qed.

Lemma aff_dep_ex :
  forall {n} {A : 'E^n.+1}, (exists i, lin_dep (frameF i A)) -> aff_dep A.
Proof. move=>>; apply aff_dep_any. Qed.

Lemma aff_dep_ex_equiv :
  forall {n} {A : 'E^n.+1}, aff_dep A <-> exists i, lin_dep (frameF i A).
Proof. intros; split; [intros H; exists ord0; easy | apply aff_dep_any]. Qed.

Lemma aff_indep_decomp_uniq :
  forall {n} {A : 'E^n.+1}, aff_indep A -> baryc_injL A.
Proof.
intros n A HA L1 L2 HL1 HL2 HL.
apply: (sum_skipF_reg _ ord0); [apply: plus_reg_r | rewrite HL2; easy |].
apply minus_zero_reg, HA.
rewrite lc_minus_l minus_zero_equiv -!(vectF_lc_skipF ord0)
    -!(baryc_orig (A ord0)); [| apply invertible_eq_one; easy..].
rewrite HL1 HL2 HL; easy.
Qed.

Lemma aff_indep_decomp_uniq_rev :
  forall {n} {A : 'E^n.+1}, baryc_injL A -> aff_indep A.
Proof.
intros n A HA L HL; apply (insertF_inj_r ord0 (1 - sum L) 1).
replace (insertF _ _ L) with (part1F0 L) by easy; rewrite -itemF_insertF.
assert (H1 : sum (part1F ord0 L) = 1) by apply part1F_sum.
assert (H2 : sum (itemF n.+1 ord0 1) = (1 : K)) by now apply sum_itemF.
apply HA; [easy.. |]; apply (vect_l_inj (A ord0)).
rewrite -(scal_one_l 1 (_ --> barycenter (part1F _ _) _))// -{1}H1
    -(scal_one_l 1 (_ --> barycenter (itemF _ _ _) _))// -{1}H2.
rewrite !(baryc_orig (A ord0)); [| apply invertible_eq_one; easy..].
rewrite -minus_zero_equiv -lc_minus_l (vectF_lc_skipF ord0).
rewrite (lc_ext_l L); [easy |].
intros i; rewrite skipF_minus fct_minus_eq skipF_insertF skipF_itemF_diag.
apply: minus_zero_r.
Qed.

Lemma aff_indep_decomp_uniq_equiv :
  forall {n} {A : 'E^n.+1}, aff_indep A <-> baryc_injL A.
Proof.
intros; split; [apply aff_indep_decomp_uniq | apply aff_indep_decomp_uniq_rev].
Qed.

End Affine_indep_Affine_Facts.


Section Affine_indep_Baryc_coord_Facts.

Context {K : Ring}.
Context {V : ModuleSpace K}.
Context {E : AffineSpace V}.

Context {n : nat}.
Context {A : 'E^n.+1}.
Hypothesis HA : aff_indep A.

Lemma bc_uniq :
  forall {B} {L}, aff_span A B -> sum L = 1 ->
    barycenter L A = B -> L = baryc_coord A B.
Proof.
move=>> HB HL H; apply (aff_indep_decomp_uniq HA _ _ HL);
    [| rewrite H]; apply bc_correct; easy.
Qed.

Lemma bc_kronF_r : forall i, baryc_coord A (A i) = kron i.
Proof.
intro; apply eq_sym, bc_uniq; [apply aff_span_inclF_diag |
    apply kron_sum_r; easy | apply baryc_l_kron_r].
Qed.

Lemma bc_kron : forall i j, baryc_coord A (A i) j = kron i j.
Proof. intros; rewrite bc_kronF_r; easy. Qed.

Lemma bc_kronF_l : forall j, mapF (baryc_coord A ^~ j) A = kron^~ j.
Proof. intro; extF; rewrite mapF_correct; apply bc_kron. Qed.

End Affine_indep_Baryc_coord_Facts.


Section AffineSpace_FD_R_Facts.

Context {V : ModuleSpace R_Ring}.
Context {E : AffineSpace V}.

Lemma aff_indep_monot :
  forall {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 (lin_indep_monot (frameF i2 A2)).
apply frameF_inj_equiv, skipF_inj; easy.
apply frameF_invalF_equiv; [| apply skipF_invalF]; easy.
apply aff_indep_all; easy.
Qed.

Lemma aff_dep_monot :
  forall {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_1 : forall {A : 'E^1}, aff_indep A.
Proof. move=>> _; apply hat0F_eq; easy. Qed.

Lemma aff_indep_singleF : forall {A : E}, aff_indep (singleF A).
Proof. intros; apply aff_indep_1. Qed.

Lemma aff_indep_2_equiv :
  forall {A : 'E^2}, aff_indep A <-> A ord0 <> A ord_max.
Proof.
intros A; unfold aff_indep; rewrite lin_indep_1_equiv// -iff_not_equiv.
rewrite -(extF_zero_1_equiv ord0)// frameF_2_0 vect_zero_equiv; easy.
Qed.

Lemma aff_indep_coupleF_equiv :
  forall {A B : E}, aff_indep (coupleF A B) <-> A <> B.
Proof. intros; rewrite aff_indep_2_equiv coupleF_0 coupleF_1; easy. Qed.

Lemma aff_indep_skipF :
  forall {n} i0 {A : 'E^n.+2}, aff_indep A -> aff_indep (skipF i0 A).
Proof.
intros n i0 A HA; destruct (ord_eq_dec i0 ord0) as [Hi0 | Hi0]; [subst |].
(* *)
apply (aff_indep_any ord_max); rewrite -(insert_ord_max ord_max_not_0).
rewrite frameF_skipF_alt; apply lin_indep_skipF_compat, aff_indep_all; easy.
(* *)
apply (aff_indep_any ord0); rewrite -(insert_ord_0 (not_eq_sym Hi0)).
rewrite frameF_skipF; apply lin_indep_skipF_compat; easy.
Qed.

Lemma aff_indep_permutF :
  forall {n p} {A : 'E^n.+1},
    bijective p -> aff_indep A -> aff_indep (permutF p A).
Proof.
intros n p A Hp HA; apply (aff_indep_any (p ord0)).
rewrite (frameF_permutF (bij_inj Hp)); apply lin_indep_permutF.
apply skip_f_ord_bij.
apply aff_indep_all; easy.
Qed.

Lemma aff_indep_permutF_rev :
  forall {n p} {A : 'E^n.+1},
    bijective p -> aff_indep (permutF p A) -> aff_indep A.
Proof.
intros n p A Hp; rewrite {2}(permutF_f_inv_l Hp A).
apply aff_indep_permutF, f_inv_bij.
Qed.

Lemma aff_indep_permutF_equiv :
  forall {n p} {A : 'E^n.+1},
    bijective p -> aff_indep A <-> aff_indep (permutF p A).
Proof.
intros; split; [apply aff_indep_permutF | apply aff_indep_permutF_rev]; easy.
Qed.

Lemma aff_indep_revF_equiv :
  forall {n} {A : 'E^n.+1}, aff_indep A <-> aff_indep (revF A).
Proof. intros; apply aff_indep_permutF_equiv, rev_ord_bij. Qed.

Lemma aff_indep_moveF_equiv :
  forall {n} i0 i1 {A : 'E^n.+1}, aff_indep A <-> aff_indep (moveF i0 i1 A).
Proof. intros; apply aff_indep_permutF_equiv, move_ord_bij. Qed.

Lemma aff_indep_transpF_equiv :
  forall {n} i0 i1 {A : 'E^n.+1}, aff_indep A <-> aff_indep (transpF i0 i1 A).
Proof. intros; apply aff_indep_permutF_equiv, transp_ord_bij. Qed.

End AffineSpace_FD_R_Facts.