Library Algebra.Finite_dim.Finite_dim_AS_def
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.
Definitions for finite-dimensional affine spaces.
When there is a finite generator family, affine algebra is simplified. With
the notions of basis and dimension (the cardinal of bases), many results are
simplified.
Let K : Ring, V : ModuleSpace K and E : AffineSpace V.
Let PE : E → Prop.
Let A : 'E^n and A' : 'E^n.+1.
Let A0 A1 A2 : E.
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
- aff_span A is the affine span of A,
i.e. the subset of the barycenters of points of A.
- aff_point A0 is the singleton A0.
- aff_line A0 A1 is the subset of E generated by A0 and A1.
- aff_plane A0 A1 A2 is the subset of E generated by A0, A1 and A2.
- baryc_surjL PE A means that each element of PE is a barycenter of A.
- baryc_injL A means that barycenters of A are unique.
- baryc_bijL PE A means that each element of PE is a unique barycenter
of A.
- aff_gen PE A means that the points of A span PE
(i.e. PE = aff_span A), i.e. A is an affine generator of PE.
- aff_indep A' means that the points of A' are affinely independent.
- aff_dep A' means that the points of A' are affinely dependent.
- aff_basis PE A' means that A' is both generator of PE and affinely
independent, i.e. it is an affine basis of PE.
- has_aff_dim PE n means that PE admits an affine basis of length n.+1.
Used logic axioms
- ex_EX, an alias for constructive_indefinite_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_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 FD_AS_Def.
Context {K : Ring}.
Context {V : ModuleSpace K}.
Context {E : AffineSpace V}.
Inductive aff_span {n} (A : 'E^n) : E → Prop :=
Aff_span : ∀ L, invertible (sum L) → aff_span A (barycenter L A).
Lemma aff_span_EX :
∀ {n} (A : 'E^n) G,
aff_span A G → { L | sum L = 1 ∧ G = barycenter L A }.
Proof.
move=>> Hx; apply ex_EX; induction Hx as [L HL];
eexists; apply (baryc_normalized _ _ _ HL); easy.
Qed.
Lemma aff_span_ex :
∀ {n} (A : 'E^n) G,
(∃ L, invertible (sum L) ∧ G = barycenter L A) → aff_span A G.
Proof. move=>> [L [HL1 HL2]]; rewrite HL2; easy. Qed.
Definition aff_point (A0 : E) := aff_span (singleF A0).
Definition aff_line (A0 A1 : E) := aff_span (coupleF A0 A1).
Definition aff_plane (A0 A1 A2 : E) := aff_span (tripleF A0 A1 A2).
Definition baryc_surjL (PE : E → Prop) {n} (A : 'E^n) :=
∀ G, PE G → ∃ L, invertible (sum L) ∧ G = barycenter L A.
Definition baryc_injL {n} (A : 'E^n) :=
∀ L L', invertible (sum L) → sum L = sum L' →
barycenter L A = barycenter L' A → L = L'.
Definition baryc_bijL (PE : E → Prop) {n} (A : 'E^n) :=
∀ G, PE G → ∃! L, sum L = 1 ∧ G = barycenter L A.
Definition aff_gen (PE : E → Prop) {n} (A : 'E^n) := PE = aff_span A.
Lemma aff_gen_ext :
∀ {PE} {n} (A1 : 'E^n) {A2}, A1 = A2 → aff_gen PE A1 → aff_gen PE A2.
Proof. intros; subst; easy. Qed.
Lemma aff_gen_ext2 :
∀ PE1 {PE2} {n} (A1 : 'E^n) {A2},
PE1 = PE2 → A1 = A2 → aff_gen PE1 A1 → aff_gen PE2 A2.
Proof. intros; subst; easy. Qed.
Definition aff_indep {n} (A : 'E^n.+1) :=
∀ i0, lin_indep (frameF A i0).
Lemma aff_indep_ext :
∀ {n} (A1 : 'E^n.+1) {A2}, A1 = A2 → aff_indep A1 → aff_indep A2.
Proof. intros; subst; easy. Qed.
Definition aff_dep {n} (A : 'E^n.+1) := ¬ aff_indep A.
Lemma aff_dep_ext :
∀ {n} (A1 : 'E^n.+1) {A2}, A1 = A2 → aff_dep A1 → aff_dep A2.
Proof. intros; subst; easy. Qed.
Definition aff_basis (PE : E → Prop) {n} (A : 'E^n.+1) :=
aff_gen PE A ∧ aff_indep A.
Lemma aff_basis_ext :
∀ {PE} {n} (A1 : 'E^n.+1) {A2},
A1 = A2 → aff_basis PE A1 → aff_basis PE A2.
Proof. intros; subst; easy. Qed.
Lemma aff_basis_ext2 :
∀ PE1 {PE2} {n} (A1 : 'E^n.+1) {A2},
PE1 = PE2 → A1 = A2 → aff_basis PE1 A1 → aff_basis PE2 A2.
Proof. intros; subst; easy. Qed.
Inductive has_aff_dim (PE : E → Prop) n : Prop :=
Aff_dim : ∀ (A : 'E^n.+1), aff_basis PE A → has_aff_dim PE n.
Lemma has_aff_dim_EX :
∀ PE n, has_aff_dim PE n → { A : 'E^n.+1 | aff_basis PE A }.
Proof. move=>> H; apply ex_EX; induction H as [A]; ∃ A; easy. Qed.
Lemma has_aff_dim_ex:
∀ PE n, (∃ A : 'E^n.+1, aff_basis PE A) → has_aff_dim PE n.
Proof. move=>> [A HA]. apply (Aff_dim _ _ A HA). Qed.
Lemma has_aff_dim_ext :
∀ {PE} n1 {n2}, n1 = n2 → has_aff_dim PE n1 → has_aff_dim PE n2.
Proof. intros; subst; easy. Qed.
Lemma has_aff_dim_ext2 :
∀ PE1 {PE2} n1 {n2},
PE1 = PE2 → n1 = n2 → has_aff_dim PE1 n1 → has_aff_dim PE2 n2.
Proof. intros; subst; easy. Qed.
End FD_AS_Def.