Library Algebra.Finite_dim.Finite_dim_AS_aff_span

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 finite affine span 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 Finite_dim_AS_def.

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

Lemma aff_span_eq :
   {n} (A : 'E^n), aff_span A = baryc_closure (inF^~ A).
Proof.
intros n A; apply subset_ext_equiv; split; intros C HC.
induction HC; apply Barycenter_closure; [easy | apply invalF_refl].
induction HC as [m L C HL HC].
destruct (baryc_injF_ex L C HL) as [p [N [D [HN [HD1 [HD2 ->]]]]]].
clear L HL; apply ((invalF_trans _ D _)^~ HC) in HD2.
destruct (baryc_unfun0F N D A) as [L [HL1 [HL2 ->]]]; easy.
Qed.

Lemma aff_span_inclF_diag : {n} (A : 'E^n), inclF A (aff_span A).
Proof.
intros n A i; rewrite -baryc_kron_r; apply Aff_span.
rewrite sum_kron_r//; apply invertible_one.
Qed.

Lemma aff_span_ub : {n} (A : 'E^n) C i, C = A i aff_span A C.
Proof. intros; subst; apply aff_span_inclF_diag. Qed.

Lemma aff_span_inclF :
   {n1 n2} (A1 : 'E^n1) (A2 : 'E^n2), invalF A1 A2 inclF A1 (aff_span A2).
Proof.
move=>> HA i; destruct (HA i) as [i2 Hi2]; rewrite Hi2; apply aff_span_inclF_diag.
Qed.

Lemma aff_spanF_ex :
   {n1 n2} (A1 : 'E^n1) (A2 : 'E^n2),
    inclF A1 (aff_span A2)
     M12, i1,
      invertible (sum (M12 i1)) A1 i1 = barycenter (M12 i1) A2.
Proof.
intros n1 n2 A1 A2; split; intros HA.
assert (HA' : i1, L2,
    invertible (sum L2) A1 i1 = barycenter L2 A2).
  intros i1; destruct (HA i1) as [L2]; L2; easy.
apply (choiceF _ HA').
intros i1; destruct HA as [M HM], (HM i1) as [HM1a HM1b]; rewrite HM1b; easy.
Qed.

Lemma aff_spanF_ex1 :
   {n1 n2} (A1 : 'E^n1) (A2 : 'E^n2),
    inclF A1 (aff_span A2)
     M12, i1, sum (M12 i1) = 1 A1 i1 = barycenter (M12 i1) A2.
Proof.
move=>>; rewrite aff_spanF_ex; split; move⇒ [M12 /all_and_equiv [HM12 HA1]].
(fun i1scal (/ sum (M12 i1)) (M12 i1)); intros i1.
apply baryc_normalized; easy.
M12; intros; rewrite HM12; split; [apply invertible_one | easy].
Qed.

Lemma aff_span_incl :
   {n1 n2} (A1 : 'E^n1) (A2 : 'E^n2),
    inclF A1 (aff_span A2) incl (aff_span A1) (aff_span A2).
Proof.
move=>> HA1 _ [L1 HL1]; apply aff_spanF_ex1 in HA1; destruct HA1 as [M HM].
apply all_and_equiv in HM; destruct HM as [HM HA1].
apply aff_span_ex; (fun i2lin_comb L1 (M^~ i2)); split.
2: apply barycenter2_r; easy.
replace (sum _) with (sum L1); try easy.
rewrite -lc_sum_r (lc_ext_r ones).
rewrite lc_ones_r; easy.
intros i1; rewrite (HM i1); easy.
Qed.

Lemma aff_span_monot :
   {n1 n2} (A1 : 'E^n1) (A2 : 'E^n2),
    invalF A1 A2 incl (aff_span A1) (aff_span A2).
Proof. intros; apply aff_span_incl, aff_span_inclF; easy. Qed.

Lemma aff_span_ext :
   {n1 n2} (A1 : 'E^n1) (A2 : 'E^n2),
    inclF A1 (aff_span A2) inclF A2 (aff_span A1)
    aff_span A1 = aff_span A2.
Proof. intros; apply subset_ext_equiv; split; apply aff_span_incl; easy. Qed.

Lemma aff_span_inv_frameF_orig :
   {n} (B : 'V^n) (O : E) i0, aff_span (inv_frameF O B i0) O.
Proof.
intros n B O i0; rewrite -{2}(transl_zero O); apply (aff_span_ub _ _ i0).
unfold inv_frameF; rewrite translF_insertF insertF_correct_l; easy.
Qed.

End Affine_span_Subset_Facts.

Section Affine_span_Affine_Facts.

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

Lemma aff_span_exs :
   {n1 n2} {A2 : 'E^n2} {G1 : 'E^n1},
    inclF G1 (aff_span A2)
     L, ( i, sum (L i) = 1) G1 = fun ibarycenter (L i) A2.
Proof.
moven1 n2 A2 G1 HG1.
destruct (choiceF (fun i Lsum L = 1 G1 i = barycenter L A2)) as [L HL].
  intros i; destruct (aff_span_EX _ _ (HG1 i)) as [L HL]; L; easy.
apply all_and_equiv in HL; L; split; try apply extF; easy.
Qed.

End Affine_span_Affine_Facts.

Section Affine_span_R_Facts.

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

Lemma aff_span_cas :
   {n} (A : 'E^n), compatible_as (aff_span A).
Proof.
intros; apply cas_equiv, eq_sym; rewrite aff_span_eq.
apply baryc_closure_idem_R.
Qed.

Lemma aff_span_lin_span_eq :
   {n} {A : 'E^n.+1} {O} i0,
    aff_span A O vectP (aff_span A) O = lin_span (frameF A i0).
Proof.
intros n A O i0 HO; rewrite (vectP_orig_indep (A i0) HO).
2: { apply cas_cms_equiv_R; try apply aff_span_inclF_diag.
    move=>> HL HC; apply aff_span_cas; easy. }
apply subset_ext_equiv; split; unfold vectP, preimage; intros u Hu.
apply aff_span_EX in Hu; destruct Hu as [L [HL1 HL2]].
rewrite (baryc_correct_orig_equiv (A i0)) in HL2.
2: rewrite HL1; apply invertible_one.
rewrite transl_correct_r HL1 scal_one in HL2; rewrite HL2.
unfold frameF; rewrite vectF_skipF (lc_skipF i0)
    vectF_correct vect_zero scal_zero_r plus_zero_l; easy.
induction Hu as [L]; unfold frameF; rewrite vectF_skipF (transl_lc i0).
rewrite translF_skipF translF_vectF insertF_skipF.
apply Aff_span, invertible_eq_one, sum_insertF_baryc.
Qed.

End Affine_span_R_Facts.