Finite_dim_AS_aff_basis.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 basis 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 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.
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_span.
From Algebra Require Import Finite_dim_AS_aff_gen Finite_dim_AS_aff_indep.

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

Context {K : Ring}.
Context {V : ModuleSpace K}.
Context {E : AffineSpace V}.
Context {PE : E -> Prop}.

Lemma aff_basis_aff_gen :
  forall {PE n} (A : 'E^n.+1), aff_basis PE A -> aff_gen PE A.
Proof. move=>> [HA _]; easy. Qed.

Lemma aff_basis_aff_indep :
  forall PE {n} (A : 'E^n.+1), aff_basis PE A -> aff_indep A.
Proof. move=>> [_ HA]; easy. Qed.

Lemma aff_basis_aff_span_equiv :
  forall {n} {A : 'E^n.+1}, aff_basis (aff_span A) A <-> aff_indep A.
Proof.
assert (H : forall P Q : Prop, P -> P /\ Q <-> Q) by tauto.
intros; apply H; easy.
Qed.

Lemma aff_basis_inclF : forall {n} {A : 'E^n.+1}, aff_basis PE A -> inclF A PE.
Proof. move=>> /aff_basis_aff_gen; apply aff_gen_inclF. Qed.

Lemma aff_basis_nonempty :
  forall {n} {A : 'E^n.+1}, aff_basis PE A -> exists O, PE O.
Proof. move=>> [HA _]; apply (aff_gen_nonempty HA). Qed.

Lemma aff_basis_decomp_ex :
  forall {n} {A : 'E^n.+1}, aff_basis PE A -> baryc_surjL PE A.
Proof. move=>> /aff_basis_aff_gen; apply aff_gen_decomp_ex. Qed.

Lemma aff_basis_decomp_uniq :
  forall PE {n} {A : 'E^n.+1}, aff_basis PE A -> baryc_injL A.
Proof. move=>> /aff_basis_aff_indep; apply aff_indep_decomp_uniq. Qed.

Lemma aff_basis_decomp_ex_uniq :
  forall {n} {A : 'E^n.+1}, aff_basis PE A -> baryc_bijL PE A.
Proof.
move=>> HA; apply baryc_surjL_injL_bijL;
    [apply aff_basis_decomp_ex | apply (aff_basis_decomp_uniq PE)]; easy.
Qed.

Lemma aff_basis_decomp_ex_uniq_rev :
  forall {n} {A : 'E^n.+1}, compatible_as PE -> inclF A PE ->
    baryc_bijL PE A -> aff_basis PE A.
Proof.
move=>> HPE HA1 HA2; split.
apply aff_gen_decomp_ex_rev; [..| apply baryc_bijL_surjL]; easy.
apply aff_indep_decomp_uniq_rev, (baryc_bijL_injL PE); easy.
Qed.

Lemma aff_basis_decomp_ex_uniq_equiv :
  forall {n} {A : 'E^n.+1}, compatible_as PE -> inclF A PE ->
    aff_basis PE A <-> baryc_bijL PE A.
Proof.
intros; split; [apply aff_basis_decomp_ex_uniq |
    apply aff_basis_decomp_ex_uniq_rev; easy].
Qed.

Lemma has_aff_dim_aff_span :
  forall {n} {A : 'E^n.+1}, aff_indep A -> has_aff_dim (aff_span A) n.
Proof. intros; apply: Aff_dim; apply aff_basis_aff_span_equiv; easy. Qed.

Lemma has_aff_dim_aff_span_alt :
  forall {n1 n2} {A1 : 'E^n1.+1},
    n1 = n2 -> aff_indep A1 -> has_aff_dim (aff_span A1) n2.
Proof. move=>> H; subst; apply has_aff_dim_aff_span. Qed.

Lemma has_aff_dim_nonempty :
  forall {n}, has_aff_dim PE n -> exists O, PE O.
Proof. move=>> [A HA]; apply (aff_basis_nonempty HA). Qed.

End Affine_span_Subset_Facts.


Section AffineSpace_FD_R_Facts.

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

Lemma aff_basis_cas :
  forall {PE n} (A : 'E^n.+1), aff_basis PE A -> compatible_as PE.
Proof. move=>> /aff_basis_aff_gen; apply aff_gen_cas. Qed.

Lemma has_aff_dim_cas :
  forall {PE : E -> Prop} n, has_aff_dim PE n -> compatible_as PE.
Proof. move=>> [B HB]; apply (aff_basis_cas _ HB). Qed.

Lemma aff_basis_lin_basis :
  forall {PE n} i0 O {A : 'E^n.+1},
    aff_span A O -> basis (vectP PE O) (frameF i0 A) -> aff_basis PE A.
Proof.
move=>> HO; apply modus_ponens_and;
    [apply aff_gen_lin_gen; easy | apply aff_indep_lin_indep].
Qed.

Lemma aff_basis_lin_basis_rev :
  forall {PE : E -> Prop} {n} i0 {O} {A : 'E^n.+1},
    PE O -> aff_basis PE A -> basis (vectP PE O) (frameF i0 A).
Proof.
move=>> HO; apply modus_ponens_and;
    [apply aff_gen_lin_gen_rev; easy | apply aff_indep_lin_indep_rev].
Qed.

Lemma aff_basis_lin_basis_equiv :
  forall {PE n} i0 {O} {A : 'E^n.+1},
    PE O -> aff_span A O ->
    aff_basis PE A <-> basis (vectP PE O) (frameF i0 A).
Proof.
intros; apply and_iff_compat;
    [apply aff_gen_lin_gen_equiv; easy | apply aff_indep_lin_indep_equiv].
Qed.

Lemma lin_basis_aff_basis :
  forall {PV n} i0 (O : E) {B : 'V^n},
    zero_closed PV ->
    aff_basis (translP PV O) (inv_frameF i0 O B) -> basis PV B.
Proof.
move=>> HO; apply modus_ponens_and;
    [apply lin_gen_aff_gen; easy | apply lin_indep_aff_indep].
Qed.

Lemma lin_basis_aff_basis_rev :
  forall {PV n} i0 (O : E) {B : 'V^n},
    basis PV B -> aff_basis (translP PV O) (inv_frameF i0 O B).
Proof.
move=>>; apply modus_ponens_and;
    [apply lin_gen_aff_gen_rev; easy | apply lin_indep_aff_indep_rev].
Qed.

Lemma lin_basis_aff_basis_equiv :
  forall {PV n} i0 (O : E) {B : 'V^n}, zero_closed PV ->
    basis PV B <-> aff_basis (translP PV O) (inv_frameF i0 O B).
Proof.
intros; apply and_iff_compat;
    [apply lin_gen_aff_gen_equiv; easy | apply lin_indep_aff_indep_equiv].
Qed.

Lemma has_aff_dim_has_dim :
  forall {PE : E -> Prop} {n} O, has_dim (vectP PE O) n -> has_aff_dim PE n.
Proof.
move=> PE n O [B /(lin_basis_aff_basis_rev ord0 O) HB];
    rewrite translP_vectP in HB; apply (Aff_dim _ _ _ HB).
Qed.

Lemma has_aff_dim_has_dim_rev :
  forall {PE : E -> Prop} {n} {O},
    PE O -> has_aff_dim PE n -> has_dim (vectP PE O) n.
Proof.
move=>> HO [A /(aff_basis_lin_basis_rev ord0 HO) HA]; apply (Dim _ _ _ HA).
Qed.

Lemma has_aff_dim_has_dim_equiv :
  forall {PE : E -> Prop} {n} {O}, PE O ->
    has_aff_dim PE n <-> has_dim (vectP PE O) n.
Proof.
intros; split;
    [apply has_aff_dim_has_dim_rev; easy | apply has_aff_dim_has_dim].
Qed.

Lemma has_dim_has_aff_dim :
  forall {PV n} (O : E),
    zero_closed PV -> has_aff_dim (translP PV O) n -> has_dim PV n.
Proof.
move=> PV n O /(translP_zero_closed_equiv O) HO
    [A /(aff_basis_lin_basis_rev ord0 HO) HA];
    rewrite vectP_translP in HA; apply (Dim _ _ _ HA).
Qed.

Lemma has_dim_has_aff_dim_rev :
  forall {PV n} (O : E), has_dim PV n -> has_aff_dim (translP PV O) n.
Proof.
move=> PV n O [B /(lin_basis_aff_basis_rev ord0 O) HB];
    apply (Aff_dim _ _ _ HB).
Qed.

Lemma has_dim_has_aff_dim_equiv :
  forall {PV n} (O : E), zero_closed PV ->
    has_dim PV n <-> has_aff_dim (translP PV O) n.
Proof.
intros; split;
    [apply has_dim_has_aff_dim_rev | apply has_dim_has_aff_dim; easy].
Qed.

Lemma has_aff_dim_has_dim_eq :
  forall {PE : E -> Prop} nas nms {O},
    PE O -> has_aff_dim PE nas -> has_dim (vectP PE O) nms -> nas = nms.
Proof.
move=>> HO Ha Hms; apply: (dim_uniq _ Hms); apply has_aff_dim_has_dim_rev; easy.
Qed.

Lemma aff_dim_uniq :
  forall {PE : E -> Prop} {n1 n2},
    has_aff_dim PE n1 -> has_aff_dim PE n2 -> n1 = n2.
Proof.
intros PE n1 n2 HPE; destruct (has_aff_dim_nonempty HPE) as [O HO]; move: HPE.
rewrite !(has_aff_dim_has_dim_equiv HO); apply dim_uniq.
Qed.

Lemma aff_gen_aff_basis :
  forall {PE n} {A : 'E^n.+1},
    has_aff_dim PE n -> aff_gen PE A -> aff_basis PE A.
Proof.
intros PE n A HPE HA; destruct (has_aff_dim_nonempty HPE) as [O HO].
assert (HO' : aff_span A O) by now rewrite -HA.
move: (has_aff_dim_has_dim_rev HO HPE) => HPE'.
move: (aff_gen_lin_gen_rev ord0 HO HA) => HA'.
apply (aff_basis_lin_basis ord0 _ HO').
apply (lin_gen_basis HPE' HA').
Qed.

Lemma aff_gen_aff_indep :
  forall {PE n} {A : 'E^n.+1},
    has_aff_dim PE n -> aff_gen PE A -> aff_indep A.
Proof.
intros PE n A HPE HA; apply (aff_basis_aff_indep PE).
apply aff_gen_aff_basis; easy.
Qed.

Lemma aff_indep_aff_gen :
  forall {PE n} {A : 'E^n.+1},
    has_aff_dim PE n -> inclF A PE -> aff_indep A -> aff_gen PE A.
Proof.
intros PE n A HPE HA1 HA2.
move: (has_aff_dim_has_dim_rev (HA1 ord0) HPE) => HPE'.
apply (aff_gen_lin_gen ord0 (A ord0)).
apply aff_span_inclF_diag.
apply (lin_indep_lin_gen HPE'); try easy.
apply frameF_inclF; easy.
Qed.

Lemma aff_indep_aff_basis :
  forall {PE n} {A : 'E^n.+1},
    has_aff_dim PE n -> inclF A PE -> aff_indep A -> aff_basis PE A.
Proof. intros; split; [apply aff_indep_aff_gen |]; easy. Qed.

Lemma aff_indep_aff_basis_equiv :
  forall {PE n} {A : 'E^n.+1},
    has_aff_dim PE n -> inclF A PE -> aff_indep A <-> aff_gen PE A.
Proof.
intros; split; [apply aff_indep_aff_gen | apply aff_gen_aff_indep]; easy.
Qed.

End AffineSpace_FD_R_Facts.


Section ModuleSpace_AffineSpace_R_Facts.

Context {E : ModuleSpace R_Ring}.
Context {PE : E -> Prop}.

Lemma has_aff_dim_has_dim_ms :
  forall {n} O, has_dim (vectP_ms PE O) n -> has_aff_dim_ms PE n.
Proof. move=>>; apply has_aff_dim_has_dim. Qed.

Lemma aff_indep_aff_gen_R :
  forall {n} (A : 'E^n.+1),
    has_dim (@fullset E) n -> aff_indep_ms A ->
    forall x, exists L, sum L = 1 /\ x = barycenter_ms L A.
Proof.
move=> n A /(has_dim_has_aff_dim_rev (A ord0)) HE HA.
apply aff_gen_ms_equiv, aff_indep_aff_gen; [apply nonzero_struct_R | easy..].
Qed.

Lemma aff_indep_aff_gen_R_lc :
  forall {n} (A : 'E^n.+1),
    has_dim (@fullset E) n -> aff_indep_ms A ->
    forall x, exists L, sum L = 1 /\ x = lin_comb L A.
Proof.
intros n A HE HA x; destruct (aff_indep_aff_gen_R _ HE HA x) as [L HL].
exists L; rewrite -baryc_ms_eq; easy.
Qed.

End ModuleSpace_AffineSpace_R_Facts.


Section Euclidean_space_AffineSpace_R_Facts.

Lemma has_aff_dim_Rn : forall {n}, has_aff_dim_ms (@fullset 'R^n) n.
Proof.
intros n; apply (has_aff_dim_has_dim_ms 0).
rewrite vectP_ms_correct vectP_fullset; apply has_dim_Rn.
Qed.

End Euclidean_space_AffineSpace_R_Facts.