Library Algebra.ModuleSpace.ModuleSpace_lin_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 for linear maps on module spaces.

Description

For results that are only valid when the ring of scalars is commutative, or being ordered, see Algebra.ModuleSpace.ModuleSpace_R_compl where they are only stated in the case of the ring of real numbers R_Ring.

Support for linear map

Let K : Ring and E1 E2 : ModuleSpace K. Let f : E1 E2.
  • f_scal_compat f states that f transports the external law scal.
  • lin_map f states that f transports the module space structure.
Lemmas about predicate lin_map have "lm" in their names, usually as prefix "lm_", sometimes as suffix "_lm".

Embryonic support for bilinear map

Let K : Ring and E1 E2 E3 : ModuleSpace K. Let f : E1 E2 E3.
  • bilin_map f states that f is linear wrt each argument.
Lemmas about predicate bilin_map have "blm" in their names, usually as prefix "blm_", sometimes as suffix "_blm".

Usage

This module may be used through the import of Algebra.ModuleSpace.ModuleSpace, 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 Monoid Group.
From Algebra Require Import ModuleSpace_compl ModuleSpace_FF_FT.
From Algebra Require Import ModuleSpace_lin_comb.

Local Open Scope Monoid_scope.
Local Open Scope Group_scope.
Local Open Scope Ring_scope.

Section Lin_map_Def.

Context {K : Ring}.
Context {E1 E2 : ModuleSpace K}.

Definition f_scal_compat (f : E1 E2) : Prop :=
   a x1, f (scal a x1) = scal a (f x1).

Definition lin_map (f : E1 E2) := f_plus_compat f f_scal_compat f.

End Lin_map_Def.

Section Lin_map_Facts1a.

Context {K : Ring}.
Context {E F : ModuleSpace K}.

Lemma f_plus_scal_compat_lm :
   {f : E F}, f_plus_compat f f_scal_compat f lin_map f.
Proof. easy. Qed.

Lemma f_scal_compat_fct_plus :
   {f g : E F},
    f_scal_compat f f_scal_compat g f_scal_compat (f + g).
Proof. move=>> Hf Hg =>>; rewrite !fct_plus_eq scal_distr_l Hf Hg; easy. Qed.

Lemma f_scal_compat_fct_zero : f_scal_compat (0 : E F).
Proof. move=>>; rewrite scal_zero_r; easy. Qed.

Lemma f_scal_compat_fct_sum :
   {n} {f : '(E F)^n},
    ( i, f_scal_compat (f i)) f_scal_compat (sum f).
Proof.
move=>> Hf =>>; rewrite !fct_sum_eq scal_sum_distr_l; f_equal.
apply extF; intros i; apply (Hf i).
Qed.

Lemma f_scal_compat_fct_opp :
   {f : E F}, f_scal_compat f f_scal_compat (- f).
Proof. move=>> Hf =>>; rewrite !fct_opp_eq scal_opp_r Hf; easy. Qed.

Lemma f_scal_compat_fct_minus :
   {f g : E F},
    f_scal_compat f f_scal_compat g f_scal_compat (f - g).
Proof.
move=>> Hf Hg =>>; rewrite !fct_minus_eq scal_minus_distr_l Hf Hg; easy.
Qed.

Lemma lm_mg : {f : E F}, lin_map f morphism_g f.
Proof. intros f [Hf _]; easy. Qed.

Lemma lm_mm : {f : E F}, lin_map f morphism_m f.
Proof. move=>> /lm_mg; apply: mg_mm. Qed.

Lemma lm_zero : {f : E F}, lin_map f f_zero_compat f.
Proof. move=>> /lm_mg; apply: mg_zero. Qed.

Lemma lm_plus : {f : E F}, lin_map f f_plus_compat f.
Proof. move=>> /lm_mg; apply: mg_plus. Qed.

Lemma lm_sum : {f : E F}, lin_map f f_sum_compat f.
Proof. move=>> /lm_mg; apply: mg_sum. Qed.

Lemma lm_opp : {f : E F}, lin_map f f_opp_compat f.
Proof. move=>> /lm_mg; apply: mg_opp. Qed.

Lemma lm_minus : {f : E F}, lin_map f f_minus_compat f.
Proof. move=>> /lm_mg; apply: mg_minus. Qed.

Lemma lm_scal : {f : E F}, lin_map f f_scal_compat f.
Proof. intros f [_ Hf]; easy. Qed.

Lemma lm_fct_plus :
   {f g : E F}, lin_map f lin_map g lin_map (f + g).
Proof.
move=>> Hf Hg; apply f_plus_scal_compat_lm.
apply mm_fct_plus; apply lm_mm; easy.
apply f_scal_compat_fct_plus; apply lm_scal; easy.
Qed.

Lemma lm_fct_zero : lin_map (0 : E F).
Proof.
apply f_plus_scal_compat_lm;
    [apply mm_fct_zero | apply f_scal_compat_fct_zero].
Qed.

Lemma lm_fct_sum :
   {n} {f : '(E F)^n}, ( i, lin_map (f i)) lin_map (sum f).
Proof.
move=>> Hf; apply f_plus_scal_compat_lm.
apply: mg_fct_sum; intro; apply lm_mg; easy.
apply f_scal_compat_fct_sum; intro; apply lm_scal; easy.
Qed.

Lemma lm_fct_opp : {f : E F}, lin_map f lin_map (- f).
Proof.
move=>> Hf; apply f_plus_scal_compat_lm.
apply: mg_fct_opp; apply lm_mg; easy.
apply f_scal_compat_fct_opp, lm_scal; easy.
Qed.

Lemma lm_fct_minus :
   {f g : E F}, lin_map f lin_map g lin_map (f - g).
Proof.
move=>> Hf Hg; apply f_plus_scal_compat_lm.
apply: mg_fct_minus; apply lm_mg; easy.
apply f_scal_compat_fct_minus; apply lm_scal; easy.
Qed.

Lemma lm_fct_scal_l :
   {f : E K} (u : F), lin_map f lin_map (fct_scal_l f u).
Proof.
move=>> [Hf1 Hf2]; split; move=>>; rewrite !fct_scal_l_eq.
rewrite Hf1; apply scal_distr_r.
rewrite Hf2 scal_assoc; easy.
Qed.


Lemma lm_fct_scalF_l :
   {n} (f : '(E K)^n) (B : 'F^n) i,
    lin_map (f i) lin_map (fct_scalF_l f B i).
Proof.
move=>> [Hf1 Hf2]; split; move=>>; rewrite !fct_scalF_l_eq !scalF_correct.
rewrite Hf1; apply scal_distr_r.
rewrite Hf2 scal_assoc; easy.
Qed.

Lemma lm_ext :
   (f g : E F), ( u, f u = g u) lin_map f lin_map g.
Proof. move=>> /fun_ext H; subst; easy. Qed.

End Lin_map_Facts1a.

Section Lin_map_Facts1b.

Context {K : Ring}.
Context {E F G : ModuleSpace K}.

Lemma lm_pt_eval : (u : E), lin_map (pt_eval F u).
Proof. easy. Qed.

Lemma lm_component : {n} i, lin_map (fun B : 'E^nB i).
Proof. easy. Qed.

Lemma lm_constF : n, lin_map (@constF E n).
Proof. easy. Qed.

Lemma lc_lm_l : {n} (B : 'E^n), lin_map (lin_comb^~ B).
Proof.
intros; split; move=>>; [rewrite lc_plus_l | rewrite lc_scal_l]; easy.
Qed.


Lemma f_scal_compat_mapF :
   {n} {f : E F},
    f_scal_compat f f_scal_compat (mapF f : 'E^n 'F^n).
Proof. move=>> Hf a x; apply extF; intro; rewrite mapF_correct Hf; easy. Qed.

Lemma lm_mapF :
   {n} {f : E F}, lin_map f lin_map (mapF f : 'E^n 'F^n).
Proof.
intros n f Hf; apply f_plus_scal_compat_lm.
apply f_plus_compat_mapF, lm_plus; easy.
apply f_scal_compat_mapF, lm_scal; easy.
Qed.

Lemma lm_map2F : {n} {f : E F G} (x : 'E^n),
  ( i, lin_map (f (x i))) lin_map (map2F f x).
Proof.
intros n f x Hf; apply f_plus_scal_compat_lm.
intros y1 y2; apply extF; intros i; destruct (Hf i) as [Hf1 _].
rewrite map2F_correct Hf1; easy.
intros a y; apply extF; intros i; destruct (Hf i) as [_ Hf2].
rewrite map2F_correct Hf2; easy.
Qed.

End Lin_map_Facts1b.

Section Lin_map_Facts2.

Context {K : Ring}.
Context {E F G : ModuleSpace K}.

Lemma f_scal_compat_comp :
   {f : E F} {g : F G},
    f_scal_compat f f_scal_compat g f_scal_compat (g \o f).
Proof. move=>> Hf Hg x1 y1; rewrite !comp_correct Hf; easy. Qed.

Lemma lm_comp :
   {f : E F} {g : F G},
    lin_map f lin_map g lin_map (g \o f).
Proof.
intros f g [Hf1 Hf2] [Hg1 Hg2]; apply f_plus_scal_compat_lm.
intros x y; rewrite comp_correct Hf1 Hg1; easy.
intros a x; rewrite comp_correct Hf2 Hg2; easy.
Qed.

Lemma f_scal_compat_comp_l :
   (f : E F), f_scal_compat (fun g : F Gg \o f).
Proof. easy. Qed.

Lemma lm_comp_l : (f : E F), lin_map (fun g : F Gg \o f).
Proof. easy. Qed.

Lemma f_scal_compat_comp_r :
   {g : F G},
    f_scal_compat g f_scal_compat (fun f : E Fg \o f).
Proof.
move=>> Hg; move=>>; apply fun_ext; intro;
    rewrite comp_correct fct_scal_r_eq Hg; easy.
Qed.

Lemma lm_comp_r :
   {g : F G}, lin_map g lin_map (fun f : E Fg \o f).
Proof.
move=>> Hg; apply f_plus_scal_compat_lm.
apply f_plus_compat_comp_r, lm_plus; easy.
apply f_scal_compat_comp_r, lm_scal; easy.
Qed.

Lemma lm_bij_compat :
   {f : E F} (Hf : bijective f), lin_map f lin_map (f_inv Hf).
Proof.
intros f Hf1 [Hf2 Hf3]; split; move=>>;
    apply (bij_inj Hf1); [rewrite Hf2 | rewrite Hf3];
    rewrite !f_inv_can_r; easy.
Qed.

End Lin_map_Facts2.

Section Lin_map_Lin_comb_Facts.

Context {K : Ring}.
Context {E F : ModuleSpace K}.

Definition f_lc_compat (f : E F) : Prop :=
   n L (B : 'E^n), f (lin_comb L B) = lin_comb L (mapF f B).

Lemma f_lc_compat_lm : {f}, lin_map f f_lc_compat f.
Proof.
intros f Hf n L B; induction n as [| n Hn].
rewrite 2!lc_nil lm_zero; easy.
rewrite 2!lc_ind_l (proj1 Hf) (proj2 Hf) Hn; easy.
Qed.

Lemma f_lc_compat_lm_rev : {f}, f_lc_compat f lin_map f.
Proof.
intros f Hf; split.
intros x y.
rewrite -{1}(scal_one x) -{1}(scal_one y) -(scal_one (f x)) -(scal_one (f y)).
rewrite -2!lc_coupleF -mapF_coupleF; easy.
move=>>; rewrite -2!lc_singleF -mapF_singleF; easy.
Qed.

Lemma lm_equiv : {f}, lin_map f f_lc_compat f.
Proof. intros; split; [apply f_lc_compat_lm | apply f_lc_compat_lm_rev]. Qed.

Lemma fct_lc_l_lm :
   {n} {f : '(E K)^n} (B : 'F^n),
    ( i, lin_map (f i)) lin_map (fun xlin_comb (f^~ x) B). Proof.
intros n; induction n as [| n Hn]; intros f B Hf.
apply lm_ext with zero.
intros; rewrite lc_nil; easy.
apply lm_fct_zero.
apply lm_ext with
  ((fun xscal (f^~ x ord0) (B ord0)) +
        (fun xlin_comb
          (fun i : 'I_n(f^~ x) (lift_S i))
          (fun i : 'I_nB (lift_S i)))).
intros; rewrite lc_ind_l; easy.
apply lm_fct_plus.
apply lm_fct_scal_l; easy.
apply Hn; intros; apply Hf.
Qed.


End Lin_map_Lin_comb_Facts.

Section Lin_map_Swap_Facts.

Context {K : Ring}.
Context {E1 E2 : ModuleSpace K}.

Lemma gather_lm_compat :
   {n} (f : '(E1 E2)^n),
    ( i, lin_map (f i)) lin_map (gather f).
Proof.
intros n f; split.
intros Hf; split; move=>>; apply extF; intro; apply Hf.
intros [Hf1 Hf2] i; split.
intros x y; apply trans_eq with (gather f (x + y) i); try easy.
rewrite Hf1; easy.
intros l x; apply trans_eq with (gather f (scal l x) i); try easy.
rewrite Hf2; easy.
Qed.

Lemma scatter_lm_compat :
   {n} (f : E1 'E2^n),
    ( i, lin_map (scatter f i)) lin_map f.
Proof. intros n f; apply (gather_lm_compat (scatter f)). Qed.

End Lin_map_Swap_Facts.

Section Bilin_map_Def.

Context {K : Ring}.
Context {E1 E2 E3 : ModuleSpace K}.

Definition lm_left (f : E1 E2 E3) : Prop := x2, lin_map (f^~ x2).
Definition lm_right (f : E1 E2 E3) : Prop := x1, lin_map (f x1).

Definition bilin_map f : Prop := lm_left f lm_right f.

End Bilin_map_Def.

Section Bilin_map_Facts1.

Context {K : Ring}.
Context {E1 E2 E3 : ModuleSpace K}.

Lemma blm_fct_plus :
   {f g : E1 E2 E3},
    bilin_map f bilin_map g bilin_map (f + g).
Proof. move=>> [Hfl Hfr] [Hgl Hgr]; split; intro; apply lm_fct_plus; easy. Qed.

Lemma blm_fct_zero : bilin_map (0 : E1 E2 E3).
Proof. split; intro; apply lm_fct_zero. Qed.

Lemma blm_fct_opp :
   {f : E1 E2 E3}, bilin_map f bilin_map (- f).
Proof. move=>> [Hfl Hfr]; split; intro; apply lm_fct_opp; easy. Qed.

Lemma blm_ext :
   (f g : E1 E2 E3),
    ( u1 u2, f u1 u2 = g u1 u2) bilin_map f bilin_map g.
Proof. move=>> /fun_ext2 H; subst; easy. Qed.

End Bilin_map_Facts1.

Section Compose_n_ModuleSpace_Facts.

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

Lemma comp_n_f_scal_compat :
   {n} (f : '(E E)^n),
    ( i, f_scal_compat (f i)) f_scal_compat (comp_n f).
Proof.
intros n f Hf; induction n as [| n Hn];
    [rewrite comp_n_nil; easy | rewrite comp_n_ind_l].
apply f_scal_compat_comp; [apply Hn; intro; apply Hf | easy].
Qed.

Lemma comp_n_lm :
   {n} (f : '(E E)^n),
    ( i, lin_map (f i)) lin_map (comp_n f).
Proof.
intros n f Hf; induction n as [| n Hn];
    [rewrite comp_n_nil; easy | rewrite comp_n_ind_l].
apply lm_comp; [apply Hn; intro; apply Hf | easy].
Qed.

End Compose_n_ModuleSpace_Facts.

Section Compose_n_part_ModuleSpace_Facts.

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

Lemma comp_n_part_f_scal_compat :
   {n} (f : '(E E)^n) j,
    ( i, f_scal_compat (f i)) f_scal_compat (comp_n_part f j).
Proof. move=>> Hf; apply comp_n_f_scal_compat; intro; apply Hf. Qed.

Lemma comp_n_part_lm :
   {n} (f : '(E E)^n) j,
    ( i, lin_map (f i)) lin_map (comp_n_part f j).
Proof. move=>> Hf; apply comp_n_lm; intro; apply Hf. Qed.

End Compose_n_part_ModuleSpace_Facts.