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.

Brief description

Support affine maps on affine spaces.

Description

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

Usage

This module may be used through the import of Algebra.AffineSpace.AffineSpace, 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 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 u1f 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^nbarycenter 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.
movef 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 _ : E1O2).
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 A2O1 +++ 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 ifct_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 if (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.
movef 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.
movea 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.