Library Algebra.Finite_dim.Finite_dim_AS_aff_gen

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 generator 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 Finite_dim_AS_aff_span.

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_gen_nonempty :
   {PE : E Prop} {n} {A : 'E^n.+1}, aff_gen PE A O, PE O.
Proof. movePE n A ->; (A ord0); apply aff_span_inclF_diag. Qed.

End Affine_span_Subset_Facts.

Section AffineSpace_FD_R_Facts.

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

Lemma aff_gen_lin_gen :
   {PE : E Prop} {n} {A : 'E^n.+1} O i0,
    aff_span A O lin_gen (vectP PE O) (frameF A i0) aff_gen PE A.
Proof.
intros PE n A O i0 HO HA.
apply (vectP_inj O); rewrite (aff_span_lin_span_eq i0); easy.
Qed.

Lemma aff_gen_lin_gen_rev :
   {PE : E Prop} {n} {A : 'E^n.+1} {O} i0,
    PE O aff_gen PE A lin_gen (vectP PE O) (frameF A i0).
Proof.
intros PE n A O i0 HO HA.
rewrite HA (aff_span_lin_span_eq i0); [apply lin_gen_lin_span | rewrite -HA//].
Qed.

Lemma aff_gen_lin_gen_equiv :
   {PE : E Prop} {n} {A : 'E^n.+1} O i0,
    PE O aff_gen PE A
    aff_span A O lin_gen (vectP PE O) (frameF A i0).
Proof.
move=>>; split; intros [HO HA]; split.
rewrite -HA; easy.
apply aff_gen_lin_gen_rev; easy.
rewrite -vectP_zero_closed_equiv HA; apply lin_span_zero_closed.
apply (aff_gen_lin_gen _ _ HO HA).
Qed.

Lemma lin_gen_aff_gen :
   {PV : V Prop} {n} {B : 'V^n} (O : E) i0,
    zero_closed PV
    aff_gen (translP PV O) (inv_frameF O B i0) lin_gen PV B.
Proof.
movePV n B O i0
    /(translP_zero_closed_equiv O) HO /(aff_gen_lin_gen_rev i0 HO).
rewrite vectP_translP frameF_inv_frameF; easy.
Qed.

Lemma lin_gen_aff_gen_rev :
   {PV : V Prop} {n} {B : 'V^n} (O : E) i0,
    lin_gen PV B aff_gen (translP PV O) (inv_frameF O B i0).
Proof.
intros PV n B O i0 HB.
apply (aff_gen_lin_gen O i0); try rewrite vectP_translP frameF_inv_frameF//.
apply aff_span_inv_frameF_orig.
Qed.

Lemma lin_gen_aff_gen_equiv :
   {PV : V Prop} {n} {B : 'V^n} (O : E) i0,
    lin_gen PV B
    zero_closed PV aff_gen (translP PV O) (inv_frameF O B i0).
Proof.
intros PV n B O i0; split.
intros HB; split.
apply (lin_gen_zero_closed _ HB).
apply lin_gen_aff_gen_rev; easy.
intros [HPV HB]; apply (lin_gen_aff_gen _ _ HPV HB).
Qed.

End AffineSpace_FD_R_Facts.

Section ModuleSpace_AffineSpace_R_Facts.

Context {E : ModuleSpace R_Ring}.

Definition affine_generator {n} (A : 'E^n) : Prop :=
   x, L, sum L = 1 x = lin_comb L A.

Lemma affine_generator_equiv :
   {n} (A : 'E^n), affine_generator A aff_gen fullset A.
Proof.
intros n A; split; intros HA.
apply subset_ext_equiv; split; try easy; intros x _.
destruct (HA x) as [L [HL1 HL2]], n as [| n].
rewrite sum_nil in HL1; contradict HL1; apply not_eq_sym, one_not_zero_R.
assert (HL1' : invertible (sum L)).
  rewrite HL1; replace 1 with (@one R_Ring); try easy; apply invertible_one.
apply aff_span_ex; L; split; try easy.
rewrite HL2; apply eq_sym, baryc_ms_eq; easy.
intros x; assert (Hx : aff_span A x) by now rewrite -HA.
induction Hx as [L HL].
destruct (baryc_normalized L A (barycenter L A)) as [HL' HG]; try easy.
rewrite HG; (scal (/ sum L)%K L); split; try easy.
apply baryc_ms_eq; easy.
Qed.

End ModuleSpace_AffineSpace_R_Facts.