Library Algebra.AffineSpace.AffineSpace_aff_map
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.
Support affine maps on affine spaces.
Let K : Ring and V1 V2 : ModuleSpace K.
Let E1 : AffineSpace V1 and E2 : AffineSpace V2.
Let f : E1 → E2, O1 : E1 and lf : V1 → V2.
Lemmas about predicate aff_map have "am" in their names, usually as prefix
"am_", sometimes as suffix "_am".
This module may be used through the import of Algebra.AffineSpace.AffineSpace,
Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.
Brief description
Description
- fct_lm f O1 is the linear part of f, defined by forall u1 : V1,
fct_lm f O1 u1 := f O1 --> f (O1 +++ u1);
- f_vect_compat_gen f lf states that for all A1 B1 : E1, lf (A1 --> B1) = f A1 --> f B1, ie vect is transported from E1 to E2;
- f_transl_compat_gen f lf states that for all A1 : E1 u1 : V1, f (A1 +++ u1) = f A1 +++ lf u1, ie transl is transported from V1 to V2;
- f_vect_compat f O1 is the specialization f_vect_compat_gen f (fct_lm f O1);
- f_transl_compat f O1 is the specialization
f_transl_compat_gen f (fct_lm f O1);
- f_vectF_compat_gen f lf states that for all O : E A1 : 'E1^n, mapF lf (vectF O A1) = vectF (f O) (mapF f A1);
- f_transl_compat_gen f lf states that for all O : E u1 : 'V1^n, mapF f (translF O u1) = translF (f O) (mapF lf u1);
- f_vectF_compat f O1 is the specialization f_vectF_compat_gen f (fct_lm f O1);
- f_translF_compat f O1 is the specialization
f_translF_compat_gen f (fct_lm f O1).
- aff_map f states that f preserves regular barycenters.
Usage
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 Monoid Group Ring ModuleSpace.
From Algebra Require Import AffineSpace_def AffineSpace_FF AffineSpace_baryc.
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 AffineSpace_Morphism_Def.
Morphisms between affine spaces are usually called affine mappings.
Context {K : Ring}.
Context {V1 V2 : ModuleSpace K}.
Context {E1 : AffineSpace V1}.
Context {E2 : AffineSpace V2}.
Definition fct_lm (f : E1 → E2) (O1 : E1) : V1 → V2 :=
fun u1 ⇒ f O1 --> f (O1 +++ u1).
Definition f_vect_compat_gen (f : E1 → E2) (lf : V1 → V2) : Prop :=
∀ A1 B1, lf (A1 --> B1) = f A1 --> f B1.
Definition f_transl_compat_gen (f : E1 → E2) (lf : V1 → V2) : Prop :=
∀ A1 u1, f (A1 +++ u1) = f A1 +++ lf u1.
Definition f_vect_compat f O1 := f_vect_compat_gen f (fct_lm f O1).
Definition f_transl_compat f O1 := f_transl_compat_gen f (fct_lm f O1).
Definition f_vectF_compat_gen (f : E1 → E2) (lf : V1 → V2) : Prop :=
∀ n O (A1 : 'E1^n), mapF lf (vectF O A1) = vectF (f O) (mapF f A1).
Definition f_translF_compat_gen (f : E1 → E2) (lf : V1 → V2) : Prop :=
∀ n (O : E1) (u1 : 'V1^n),
mapF f (translF O u1) = translF (f O) (mapF lf u1).
Definition f_vectF_compat f O1 := f_vectF_compat_gen f (fct_lm f O1).
Definition f_translF_compat f O1 := f_translF_compat_gen f (fct_lm f O1).
Definition aff_map (f : E1 → E2) : Prop :=
∀ n L (A1 : 'E1^n),
invertible (sum L) → f (barycenter L A1) = barycenter L (mapF f A1).
Lemma fct_lm_ext :
∀ (f g : E1 → E2), same_fun f g → fct_lm f = fct_lm g.
Proof. move=>> /fun_ext H; subst; easy. Qed.
Lemma am_ext :
∀ (f g : E1 → E2), same_fun f g → aff_map f → aff_map g.
Proof. move=>> /fun_ext H; subst; easy. Qed.
End AffineSpace_Morphism_Def.
Section AffineSpace_Morphism_Facts0.
Context {V : ModuleSpace R_Ring}.
Context {E : AffineSpace V}.
Lemma baryc_am :
∀ {n} L, invertible (sum L) → aff_map (fun B : 'E^n ⇒ barycenter L B).
Proof.
move=>> HL; move=>> HM; apply baryc_comm_R; apply invertible_equiv_R; easy.
Qed.
End AffineSpace_Morphism_Facts0.
Section AffineSpace_Morphism_Facts1.
Context {K : Ring}.
Context {V1 V2 : ModuleSpace K}.
Context {E1 : AffineSpace V1}.
Context {E2 : AffineSpace V2}.
Lemma f_vect_transl_compat_gen_equiv :
∀ {f : E1 → E2} {lf},
f_vect_compat_gen f lf ↔ f_transl_compat_gen f lf.
Proof.
intros; split; intros Hf; move=>>.
rewrite transl_vect_equiv -Hf transl_correct_r; easy.
rewrite -transl_vect_equiv -Hf transl_correct_l; easy.
Qed.
Lemma f_vect_transl_compat_equiv :
∀ {f : E1 → E2} {O1}, f_vect_compat f O1 ↔ f_transl_compat f O1.
Proof. intros; apply f_vect_transl_compat_gen_equiv. Qed.
Lemma f_plus_transl_compat :
∀ {f : E1 → E2} {O1},
f_plus_compat (fct_lm f O1) → f_transl_compat f O1.
Proof.
intros f O1 Hf A1 u1; apply (vect_l_inj (f O1)).
rewrite -(transl_correct_l O1 A1) transl_assoc vect_transl_assoc; apply Hf.
Qed.
Lemma f_transl_plus_compat :
∀ {f : E1 → E2} O1,
f_transl_compat f O1 → f_plus_compat (fct_lm f O1).
Proof.
intros f O1 Hf u1 v1; unfold fct_lm; apply (transl_l_inj (f O1)).
rewrite -transl_assoc -(transl_assoc (f O1)) !transl_correct_l; apply Hf.
Qed.
Lemma f_transl_plus_compat_equiv :
∀ {f : E1 → E2} O1,
f_transl_compat f O1 ↔ f_plus_compat (fct_lm f O1).
Proof.
intros; split; [apply f_transl_plus_compat | apply f_plus_transl_compat].
Qed.
Lemma f_plus_vect_compat :
∀ {f : E1 → E2} {O1},
f_plus_compat (fct_lm f O1) → f_vect_compat f O1.
Proof.
move=>>; rewrite f_vect_transl_compat_equiv; apply f_plus_transl_compat.
Qed.
Lemma f_vect_plus_compat :
∀ {f : E1 → E2} O1, f_vect_compat f O1 → f_plus_compat (fct_lm f O1).
Proof. move=>> /f_vect_transl_compat_equiv; apply f_transl_plus_compat. Qed.
Lemma f_vect_plus_compat_equiv :
∀ {f : E1 → E2} O1, f_vect_compat f O1 ↔ f_plus_compat (fct_lm f O1).
Proof.
intros; rewrite f_vect_transl_compat_equiv; apply f_transl_plus_compat_equiv.
Qed.
Lemma fct_lm_orig_indep :
∀ {f : E1 → E2} O1 O1',
f_plus_compat (fct_lm f O1) → fct_lm f O1 = fct_lm f O1'.
Proof.
unfold fct_lm; intros f O1 O1' Hlf; apply fun_ext; intros u1.
rewrite -(vect_chasles (f O1) (f O1')) -{2}(transl_correct_l O1 O1').
rewrite transl_assoc Hlf transl_correct_l plus_assoc.
rewrite (vect_sym (f O1')) plus_opp_l plus_zero_l; easy.
Qed.
Lemma f_vect_compat_orig_indep :
∀ {f : E1 → E2} O1 O1', f_vect_compat f O1 → f_vect_compat f O1'.
Proof.
intros f O1 O1' Hf; generalize (f_vect_plus_compat O1 Hf); intros Hlf A1 B1.
rewrite -(fct_lm_orig_indep O1); easy.
Qed.
Lemma f_transl_compat_orig_indep :
∀ {f : E1 → E2} O1 O1', f_transl_compat f O1 → f_transl_compat f O1'.
Proof.
intros f O1 O1' Hf; generalize (f_transl_plus_compat O1 Hf); intros Hlf A1 u1.
rewrite -(fct_lm_orig_indep O1); easy.
Qed.
Lemma f_transl_compat_gen_flm_uniq :
∀ {f : E1 → E2} {lf} {O1 : E1},
f_plus_compat lf → f_transl_compat_gen f lf → lf = fct_lm f O1.
Proof.
move=>> Hlf Hf; apply fun_ext; intro; unfold fct_lm.
rewrite Hf transl_correct_r; easy.
Qed.
Lemma f_vect_compat_gen_flm_uniq :
∀ {f : E1 → E2} {lf} {O1 : E1},
f_plus_compat lf → f_vect_compat_gen f lf → lf = fct_lm f O1.
Proof.
move=>>; rewrite f_vect_transl_compat_gen_equiv.
apply f_transl_compat_gen_flm_uniq.
Qed.
Lemma am_lm :
∀ {f : E1 → E2} O1, lin_map (fct_lm f O1) → aff_map f.
Proof.
intros f O1 Hf.
generalize (f_lc_compat_lm Hf); intros Hf'.
intros n L A1 HL; apply (baryc_correct_orig_equiv (f O1)); try easy.
rewrite -(transl_correct_l O1 (barycenter _ _)).
fold (fct_lm f O1 (O1 --> barycenter L A1)).
rewrite -(proj2 Hf) (baryc_correct_orig _ _ HL) Hf' vectF_mapF.
apply lc_ext_r; intros i.
unfold fct_lm; rewrite !mapF_correct transl_correct_l; easy.
Qed.
Lemma am_lm_rev :
∀ {f : E1 → E2} O1, aff_map f → lin_map (fct_lm f O1).
Proof.
intros f O1 Hf; unfold fct_lm; split.
intros u1 v1; generalize (@sum_alt_ones_3_invertible K); intros H3.
rewrite transl_plus_baryc Hf; try easy.
rewrite mapF_tripleF -(scal_one (_ --> barycenter _ _)) -{1}(sum_alt_ones_3).
rewrite baryc_correct_orig; try easy.
rewrite vectF_tripleF lc_tripleF.
rewrite vect_zero scal_zero_r plus_zero_r 2!scal_one plus_comm; easy.
intros a u1; generalize (sum_unit_partition_1_invertible a); intros Ha.
rewrite transl_scal_baryc Hf; try easy.
rewrite mapF_coupleF -(scal_one (_ --> barycenter _ _))
-{1}(sum_unit_partition_1 a).
rewrite baryc_correct_orig; try easy.
rewrite vectF_coupleF lc_coupleF vect_zero scal_zero_r plus_zero_l; easy.
Qed.
Lemma am_lm_equiv :
∀ {f : E1 → E2} O1, aff_map f ↔ lin_map (fct_lm f O1).
Proof. intros; split. apply am_lm_rev. apply am_lm. Qed.
Lemma am_flm_orig_indep :
∀ {f : E1 → E2} {O1} O1',
aff_map f → fct_lm f O1 = fct_lm f O1'.
Proof. intros; apply fct_lm_orig_indep, lm_plus, am_lm_equiv; easy. Qed.
Lemma am_vect :
∀ {f : E1 → E2} O1, aff_map f → f_vect_compat f O1.
Proof.
move⇒ f O1 /(am_lm_equiv O1) Hf A1 B1.
rewrite (fct_lm_orig_indep _ A1).
unfold fct_lm; rewrite transl_correct_l; easy.
apply lm_plus; easy.
Qed.
Lemma am_transl :
∀ {f : E1 → E2} O1, aff_map f → f_transl_compat f O1.
Proof.
intros; apply f_vect_transl_compat_equiv, am_vect; easy.
Qed.
Lemma fct_cst_am : ∀ (O2 : E2), aff_map (fun _ : E1 ⇒ O2).
Proof.
intros; apply (am_lm (point_of_as _)), (lm_ext 0); [| apply lm_fct_zero].
intros; unfold fct_lm; rewrite vect_zero; easy.
Qed.
Lemma fct_point_of_as_am : aff_map (@fct_point_of_as E1 _ _ E2).
Proof. apply fct_cst_am. Qed.
Lemma fct_lm_bij_compat :
∀ {f : E1 → E2} O1, bijective f → bijective (fct_lm f O1).
Proof.
intros f O1 [g Hg1 Hg2]; apply Bijective with (fct_lm g (f O1)); unfold fct_lm.
intro; rewrite transl_correct_l !Hg1 transl_correct_r; easy.
intro; rewrite Hg1 transl_correct_l Hg2 transl_correct_r; easy.
Qed.
Lemma am_bij_equiv :
∀ {f : E1 → E2} O1,
aff_map f → bijective f ↔ bijective (fct_lm f O1).
Proof.
intros f O1 Hf1; split; try apply fct_lm_bij_compat.
intros [lg Hlg1 Hlg2];
apply Bijective with (fun A2 ⇒ O1 +++ lg (f O1 --> A2)).
intro; rewrite -(am_vect O1 Hf1) Hlg1 transl_correct_l; easy.
intro; rewrite (am_transl O1 Hf1) Hlg2 transl_correct_l; easy.
Qed.
End AffineSpace_Morphism_Facts1.
Section AffineSpace_Morphism_Facts2.
Context {K : Ring}.
Context {V1 V2 V3 : ModuleSpace K}.
Context {E1 : AffineSpace V1}.
Context {E2 : AffineSpace V2}.
Context {E3 : AffineSpace V3}.
Lemma fct_lm_comp :
∀ {f12 : E1 → E2} {f23 : E2 → E3} O1,
fct_lm (f23 \o f12) O1 = (fct_lm f23 (f12 O1)) \o (fct_lm f12 O1).
Proof.
intros; apply fun_ext; intro.
unfold fct_lm; rewrite !comp_correct transl_correct_l; easy.
Qed.
Lemma am_comp :
∀ {f12 : E1 → E2} {f23 : E2 → E3},
aff_map f12 → aff_map f23 → aff_map (f23 \o f12).
Proof.
intros f12 f23; pose (O1 := point_of_as E1).
move⇒ /(am_lm_equiv O1) H12 /(am_lm_equiv (f12 O1)) H23.
apply (am_lm_equiv O1).
rewrite fct_lm_comp; apply lm_comp; easy.
Qed.
End AffineSpace_Morphism_Facts2.
Section AffineSpace_Morphism_Facts3.
Context {K : Ring}.
Context {V1 V2 : ModuleSpace K}.
Context {E1 : AffineSpace V1}.
Context {E2 : AffineSpace V2}.
Lemma fct_lm_inv :
∀ {f : E1 → E2} (Hf : bijective f) O1,
fct_lm (f_inv Hf) (f O1) = f_inv (fct_lm_bij_compat O1 Hf).
Proof.
intros f Hf O1; apply fun_ext; intros u2.
rewrite -{1}(f_inv_can_r (fct_lm_bij_compat O1 Hf) u2); unfold fct_lm.
rewrite transl_correct_l !f_inv_can_l transl_correct_r; easy.
Qed.
Lemma am_bij_compat :
∀ {f : E1 → E2} (Hf : bijective f), aff_map f → aff_map (f_inv Hf).
Proof.
intros f Hf; pose (O1 := point_of_as E1).
rewrite (am_lm_equiv O1) (am_lm_equiv (f O1)) fct_lm_inv.
apply lm_bij_compat.
Qed.
End AffineSpace_Morphism_Facts3.
Section AffineSpace_Morphism_Facts4.
Context {K : Ring}.
Context {V1 V2 : ModuleSpace K}.
Context {E1 : AffineSpace V1}.
Context {E2 : AffineSpace V2}.
Lemma fct_lm_gather :
∀ {n} (f : '(E1 → E2)^n) O1,
fct_lm (gather f) O1 = gather (fun i ⇒ fct_lm (f i) O1).
Proof. easy. Qed.
Lemma gather_am_compat :
∀ {n} (f : '(E1 → E2)^n),
(∀ i, aff_map (f i)) ↔ aff_map (gather f).
Proof.
intros n f; pose (O1 := point_of_as E1).
rewrite (am_lm_equiv O1) fct_lm_gather -gather_lm_compat.
apply equiv_forall; intros i; apply am_lm_equiv.
Qed.
Lemma scatter_am_compat :
∀ {n} (f : E1 → 'E2^n),
(∀ i, aff_map (scatter f i)) ↔ aff_map f.
Proof. intros n f; apply (gather_am_compat (scatter f)). Qed.
End AffineSpace_Morphism_Facts4.
Section ModuleSpace_AffineSpace_Morphism.
Context {K : Ring}.
Context {E1 E2 : ModuleSpace K}.
Lemma fct_lm_ms_eq :
∀ {f : E1 → E2} O1 u1, fct_lm f O1 u1 = f (O1 + u1) - f O1.
Proof.
intros f O1 u1; unfold fct_lm; rewrite ms_vect_eq ms_transl_eq; easy.
Qed.
Lemma fct_lm_ms_eq_ex:
∀ {f lf : E1 → E2},
lin_map lf →
lf = fct_lm f 0 ↔ ∃ c2, f = lf + (fun⇒ c2).
Proof.
intros f lf Hlf; split;
[intros Hf; ∃ (f 0) | intros [c2 Hf]]; apply fun_ext; intro.
rewrite Hf fct_plus_eq fct_lm_ms_eq plus_zero_l plus_minus_l; easy.
rewrite fct_lm_ms_eq Hf !fct_plus_eq (lm_zero Hlf)
!plus_zero_l minus_plus_r; easy.
Qed.
Lemma fct_lm_ms_cst_reg :
∀ (f : E1 → E2) (c2 : E2) (O1 : E1),
fct_lm (f + (fun⇒ c2)) O1 = fct_lm f O1.
Proof.
intros; apply fun_ext; intro.
rewrite !fct_lm_ms_eq !fct_plus_eq -minus_plus_r_eq; easy.
Qed.
Lemma fct_lm_ms_lin :
∀ {f : E1 → E2} (O1 : E1), lin_map f → fct_lm f O1 = f.
Proof.
move=>> [Hf _]; apply fun_ext; intro.
rewrite fct_lm_ms_eq Hf minus_plus_l; easy.
Qed.
Lemma am_ms_equiv :
∀ {f : E1 → E2},
aff_map f ↔ ∃ lf c2, lin_map lf ∧ f = lf + (fun⇒ c2).
Proof.
intros f; split.
intros Hf; ∃ (fct_lm f 0), (f 0); split.
apply am_lm_equiv; easy.
apply fun_ext; intros u; rewrite fct_plus_eq plus_minus_l_equiv
-{2}(plus_zero_l u) -ms_transl_eq -ms_vect_eq; easy.
intros [lf [c2 [Hlf1 Hlf2]]]; apply (am_lm_equiv (0 : E1)).
apply (lm_ext lf); try easy.
intros u; unfold fct_lm; rewrite Hlf2 ms_transl_eq ms_vect_eq !fct_plus_eq.
rewrite (lm_zero Hlf1) !plus_zero_l minus_plus_r; easy.
Qed.
Lemma am_lm_ms :
∀ {lf : E1 → E2} c2, lin_map lf → aff_map (lf + (fun⇒ c2)).
Proof. intros lf c2 Hf; rewrite am_ms_equiv; ∃ lf, c2; easy. Qed.
Lemma am_lm_0 : ∀ {f : E1 → E2}, lin_map (f - (fun⇒ f 0)) → aff_map f.
Proof.
intros f Hf; apply am_ms_equiv; ∃ (f - (fun⇒ f 0)), (f 0); split. easy.
rewrite -plus_assoc plus_opp_l plus_zero_r; easy.
Qed.
Lemma am_lm_0_rev :
∀ {f : E1 → E2}, aff_map f → lin_map (f - (fun⇒ f 0)).
Proof.
move=>> /am_ms_equiv [lf [c2 [Hlf1 Hlf2]]].
apply lm_ext with lf; try easy.
intro; rewrite Hlf2 fct_minus_eq !fct_plus_eq (lm_zero Hlf1)
plus_zero_l minus_plus_r; easy.
Qed.
Lemma am_lm_0_equiv :
∀ {f : E1 → E2}, aff_map f ↔ lin_map (f - (fun⇒ f 0)).
Proof. intros; split; [apply am_lm_0_rev | apply am_lm_0]. Qed.
Lemma am_ac_compat :
∀ {n} {f : E1 → E2} {L} {B : 'E1^n},
aff_map f → sum L = 1 → f (lin_comb L B) = lin_comb L (fun i ⇒ f (B i)).
Proof.
move=>> /am_ms_equiv [lf [c [Hlf1 Hlf2]]] HL.
rewrite Hlf2 fct_plus_eq f_lc_compat_lm; try easy.
rewrite lc_plus_r; f_equal.
rewrite -{1}(scal_one c) -HL -lc_constF_r; easy.
Qed.
Lemma am_f_plus :
∀ {f g : E1 → E2}, aff_map f → aff_map g → aff_map (f + g).
Proof.
move⇒ f g /am_lm_0_rev Hf /am_lm_0_rev Hg;
apply am_lm_0, (lm_ext ((f - fun⇒ f 0) + (g - (fun⇒ g 0)))).
intros; rewrite !fct_plus_eq !fct_minus_eq fct_plus_eq !minus_eq opp_plus
plus_comm4_m; easy.
apply lm_fct_plus; easy.
Qed.
Lemma am_f_sum :
∀ {n} {f : '(E1 → E2)^n}, (∀ i, aff_map (f i)) → aff_map (sum f).
Proof.
intros n f Hf; induction n as [| n IHn].
rewrite sum_nil; apply (am_ext (fun⇒ (0 : E2))); [easy |]; apply fct_cst_am.
rewrite sum_ind_l; apply am_f_plus; [easy |]; apply IHn; intros; apply Hf.
Qed.
End ModuleSpace_AffineSpace_Morphism.
Section ModuleSpace_AffineSpace_Morphism_R.
Context {E1 E2 : ModuleSpace R_Ring}.
Lemma am_f_scal :
∀ a {f : E1 → E2}, aff_map f → aff_map (scal a f).
Proof.
move⇒ a f /am_lm_0_rev Hf; apply am_lm_0, (lm_ext (scal a (f - fun⇒ f 0))).
intros; rewrite fct_minus_eq !fct_scal_eq fct_minus_eq scal_minus_r; easy.
apply lm_fct_scal; easy.
Qed.
Lemma am_f_lc :
∀ {n} (L : 'R^n) {f : '(E1 → E2)^n},
(∀ i, aff_map (f i)) → aff_map (lin_comb L f).
Proof. intros; apply am_f_sum; intros; apply am_f_scal; easy. Qed.
End ModuleSpace_AffineSpace_Morphism_R.