Library Top.continuous_linear_map

This file is part of the Elfic library
Copyright (C) Boldo, Clément, Faissole, Martin, Mayero
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.

Require Export linear_map.
Require Export fixed_point.
Require Import mathcomp.ssreflect.ssreflect.
Require Import Decidable.

Properties of linear_maps of NormedModule

Section DefsLin.

Context {E : NormedModule R_AbsRing}.
Context {F : NormedModule R_AbsRing}.

Definition is_bounded (f:EF) :=
     M : R, 0 M
         ( x : E, norm (f x) M × norm x).

Definition is_bounded_linear_mapping (f : E F) :=
     is_linear_mapping f is_bounded f.

End DefsLin.

Decidability Is_only_zero_set
Continuous Linear Maps

Section ContinuousLinearMap.

Context {E : NormedModule R_AbsRing}.
Context {F : NormedModule R_AbsRing}.

Additional properties

Lemma norm_gt_0: (x:E), x zero 0 < norm x.

Lemma is_zero_dec: (x:E), x = zero x zero.

Lemma norm_unit_vector: (u:E), u zero norm (scal (/norm u) u) = 1.

Lemma norm_of_image_of_unit_vector: (f:EF), (u:E), is_linear_mapping f u zero
   norm (f (scal (/norm u) u)) = norm (f u) / norm u.

Lemma norm_of_image_of_unit_vector': (f:EF), (u:E),
  is_linear_mapping f
    norm (f (scal (/norm u) u)) × norm u = norm (f u).

Operator norms

Definition operator_norm (f:EF) : Rbar :=
   match Is_only_zero_set_dec E with
    | left _Lub_Rbar (fun x u:E, u zero
                   x = norm (f u) / norm u)
    | right _ ⇒ 0
  end.

Lemma operator_norm_ge_0: f,
  Rbar_le 0 (operator_norm f).

Lemma operator_norm_ge_0': f,
  0 (operator_norm f).

Lemma operator_norm_helper:
     f, is_linear_mapping f is_finite (operator_norm f)
       (Is_only_zero_set E operator_norm f = 0)
      (¬Is_only_zero_set E u, norm (f u) operator_norm f × norm u).

Lemma operator_norm_helper':
     f, is_finite (operator_norm f)
        ( u, u zero norm (f u) operator_norm f × norm u).

Lemma operator_norm_helper2:
     f, is_finite (operator_norm f)
       (Is_only_zero_set E operator_norm f = 0)
      (¬Is_only_zero_set E M, 0 M
         ( u, u zero norm (f u) M × norm u)
            operator_norm f M).

Lemma operator_norm_helper3:
     f, M, 0 M
       ( u, u zero norm (f u) M × norm u)
         is_finite (operator_norm f).

Lemma operator_norm_helper3':
     f, M, 0 M
       ( u, u zero norm (f u) M × norm u)
         (operator_norm f M).

Equivalent definitions of continuity for linear maps
Equivalence of several assertions for continuity : More precisely, given (f:E->F), is_linear_mapping f, then the followings are equivalent: (1) continuous f zero (2) forall (x:E), continuous f x (3) forall (eps:posreal), exists (delta:posreal), forall x y, ball x delta y -> ball (f x) eps (f y) {uniform continuity} (4) exists k, is_Lipschitz f k (5) is_bounded f (6) is_finite (operator_norm f) (7) exists M : R, 0 <= M /\ (forall x : E, norm x = 1 -> norm (f x) <= M). (8) exists M : R, 0 <= M /\ (forall x : E, norm x <= 1 -> norm (f x) <= M).

Lemma continuous_linear_map_2_1:
    (f:EF),
   ( (x:E), continuous f x)
      continuous f zero.

Lemma continuous_linear_map_3_2:
   (f:EF),
    ( (eps:posreal), (delta:posreal), x y,
       ball x delta y ball (f x) eps (f y))
    ( (x:E), continuous f x).

Lemma continuous_linear_map_4_3:
   (f:EF),
    ( k, is_Lipschitz f k)
    ( (eps:posreal), (delta:posreal), x y,
       ball x delta y ball (f x) eps (f y)).

Lemma continuous_linear_map_5_4:
    (f:EF), is_linear_mapping f
     is_bounded f
      ( k, is_Lipschitz f k).

Lemma continuous_linear_map_6_5:
    (f:EF), is_linear_mapping f
   is_finite (operator_norm f)
   is_bounded f.

Lemma continuous_linear_map_7_6:
    (f:EF), is_linear_mapping f
    ( M : R, 0 M
         ( x : E, norm x = 1 norm (f x) M))
   is_finite (operator_norm f).

Lemma continuous_linear_map_8_7:
    (f:EF),
    ( M : R, 0 M
         ( x : E, norm x 1 norm (f x) M))
    ( M : R, 0 M
         ( x : E, norm x = 1 norm (f x) M)).

Lemma continuous_linear_map_1_8:
    (f:EF), is_linear_mapping f
     continuous f zero
   ( M : R, 0 M
          ( x : E, norm x 1 norm (f x) M)).

End ContinuousLinearMap.

Finiteness properties of operator norm
Composition and operator norm

Context {G : NormedModule R_AbsRing}.

Lemma is_linear_mapping_compose: (f:EF), (g:FG),
    is_linear_mapping f is_linear_mapping g
      is_linear_mapping (fun xg (f x)).

Lemma operator_norm_compose:
   (f:E F), (g:F G), (g zero = zero)
   is_finite (operator_norm f) is_finite (operator_norm g)
     operator_norm (fun (x:E) ⇒ g (f x)) operator_norm g × operator_norm f.

Lemma is_finite_operator_norm_compose: (f:EF), (g:FG),
    (g zero = zero) is_finite (operator_norm f) is_finite (operator_norm g)
       is_finite (operator_norm (fun xg (f x))).

End avantV.

Require Import ProofIrrelevance.
Require Import FunctionalExtensionality.

Section Clm.

Variable E : NormedModule R_AbsRing.
Variable F : NormedModule R_AbsRing.

Definition of clm

Record clm := Clm {
  m:> EF ;
  Lf: is_linear_mapping m;
  Cf: is_finite (operator_norm m)
}.

Clm is AbelianGroup

Definition clm_zero : clm := Clm (fun _zero)
    is_linear_mapping_f_zero is_finite_norm_zero.

Definition clm_plus (f:clm) (g:clm) := Clm
    (plus (m f) (m g))
    (is_linear_mapping_f_plus _ _ (Lf f) (Lf g))
    (is_finite_operator_norm_plus _ _ (Cf f) (Cf g)).

Definition clm_opp (f:clm) := Clm
    (opp (m f))
    (is_linear_mapping_f_opp _ (Lf f))
    (is_finite_operator_norm_opp _ (Cf f)).

Definition clm_scal (l:R) (f:clm) := Clm
    (scal l (m f))
    (is_linear_mapping_f_scal l _ (Lf f))
    (is_finite_operator_norm_scal l _ (Cf f)).

Lemma clm_eq: (f g:clm), (m f = m g) f = g.

Lemma clm_eq_ext: (f g:clm), ( x, f x = g x) f = g.

Lemma clm_plus_comm: (f g:clm), clm_plus f g = clm_plus g f.

Lemma clm_plus_assoc:
   (x y z:clm), clm_plus x (clm_plus y z) = clm_plus (clm_plus x y) z.

Lemma clm_plus_zero_r: x:clm, clm_plus x clm_zero = x.

Lemma clm_plus_opp_r: x:clm, clm_plus x (clm_opp x) = clm_zero.

Definition clm_AbelianGroup_mixin :=
  AbelianGroup.Mixin clm clm_plus clm_opp clm_zero clm_plus_comm
   clm_plus_assoc clm_plus_zero_r clm_plus_opp_r.

Canonical clm_AbelianGroup :=
  AbelianGroup.Pack clm (clm_AbelianGroup_mixin) clm.

Clm is ModuleSpace

Lemma clm_scal_assoc: x y (u:clm),
   clm_scal x (clm_scal y u) = clm_scal (mult x y) u.

Lemma clm_scal_one: (u:clm), clm_scal one u = u.

Lemma clm_scal_distr_l: x (u v:clm), clm_scal x (plus u v)
        = clm_plus (clm_scal x u) (clm_scal x v).

Lemma clm_scal_distr_r: (x y:R) (u:clm), clm_scal (Rplus x y) u
         = clm_plus (clm_scal x u) (clm_scal y u).

Definition clm_ModuleSpace_mixin :=
  ModuleSpace.Mixin R_Ring clm_AbelianGroup clm_scal clm_scal_assoc
     clm_scal_one clm_scal_distr_l clm_scal_distr_r.

Canonical clm_ModuleSpace :=
  ModuleSpace.Pack R_Ring clm
   (ModuleSpace.Class R_Ring clm _ clm_ModuleSpace_mixin) clm.

Clm is UniformSpace

Definition clm_ball := fun (x:clm) eps yoperator_norm (minus y x) < eps.

Lemma clm_ball_center : (x : clm) (e : posreal),
  clm_ball x e x.

Lemma clm_ball_sym :
   (x y : clm) (e : R),
  clm_ball x e y clm_ball y e x.

Lemma clm_ball_triangle :
   (x y z : clm) (e1 e2 : R),
  clm_ball x e1 y clm_ball y e2 z clm_ball x (e1 + e2) z.

Definition clm_UniformSpace_mixin :=
  UniformSpace.Mixin clm clm_ball clm_ball_center clm_ball_sym clm_ball_triangle.

Canonical clm_UniformSpace :=
  UniformSpace.Pack clm (clm_UniformSpace_mixin) clm.

Clm is NormedModule

Canonical clm_NormedModuleAux :=
  NormedModuleAux.Pack R_AbsRing clm
   (NormedModuleAux.Class R_AbsRing clm
     (ModuleSpace.class _ clm_ModuleSpace)
        clm_UniformSpace_mixin) clm.

Lemma clm_norm_triangle: (x y:clm), operator_norm (plus x y) operator_norm x + operator_norm y.

Lemma clm_norm_ball1 : (x y : clm) (eps : R),
        operator_norm (minus y x) < eps Hierarchy.ball x eps y.

Lemma clm_norm_ball2: (x y : clm) (eps : posreal),
          Hierarchy.ball x eps y operator_norm (minus y x) < 1 × eps.

Lemma clm_norm_scal_aux:
  ( (l : R) (x : clm), operator_norm (scal l x) abs l × operator_norm x).

Lemma clm_norm_eq_0: (x:clm), real (operator_norm x) = 0 x = zero.

Definition clm_NormedModule_mixin :=
  NormedModule.Mixin R_AbsRing _
   (fun freal (operator_norm (m f))) 1%R clm_norm_triangle clm_norm_scal_aux clm_norm_ball1 clm_norm_ball2 clm_norm_eq_0.

Canonical clm_NormedModule :=
  NormedModule.Pack R_AbsRing clm
     (NormedModule.Class _ _ _ clm_NormedModule_mixin) clm.

End Clm.


Composition of clm

Section Composition_lcm.

Variable E : NormedModule R_AbsRing.
Variable F : NormedModule R_AbsRing.
Variable G : NormedModule R_AbsRing.

Lemma operator_norm_estimation:
    (f:clm E F), (u:E),
      norm (f u) norm f × norm u.

Definition compose_lcm (g:clm F G) (f:clm E F) :=
   Clm E G (fun xg (f x))
    (is_linear_mapping_compose _ _ (Lf _ _ f) (Lf _ _ g))
    (is_finite_operator_norm_compose _ _
        (is_linear_mapping_zero _ (Lf _ _ g)) (Cf _ _ f) (Cf _ _ g)).

Lemma norm_compose_lcm:
   (f:clm E F), (g:clm F G),
     norm (compose_lcm g f) norm g × norm f.

End Composition_lcm.

Topo_dual
Bilinear maps

Section DefsBilin.

Context {E : NormedModule R_AbsRing}.
Context {F : NormedModule R_AbsRing}.
Context {G : NormedModule R_AbsRing}.

Definition is_bounded_bi (f:EFG) (M:R) :=
   0 M
     ( (x:E) (y:F), norm (f x y) M × norm x × norm y).

Definition is_bounded_bilinear_mapping (f : E F G) (M:R) :=
     is_bilinear_mapping f is_bounded_bi f M.

Definition is_coercive (f : E E R) (M:R):=
  0 < M
    ( x : E, M × norm x × norm x (f x x)).

End DefsBilin.

Section Bilin_rep.

Context {E : NormedModule R_AbsRing}.

Lemma is_bounded_bilinear_mapping_representation':
    phi M,
     is_bounded_bilinear_mapping phi M
        (A:clm E (topo_dual E)),
            (u v:E), phi u v = (A u) v.

Lemma is_bounded_bilinear_mapping_representation_unique:
    (phi:EE R),
        (A B :clm E (topo_dual E)),
           phi = (m A) phi = (m B) A = B.

Lemma is_bounded_bilinear_mapping_representation:
    phi M,
     is_bounded_bilinear_mapping phi M
       ! (A:clm E (topo_dual E)),
            (u v:E), phi u v = (A u) v.

Lemma is_bounded_bilinear_mapping_representation_moreover:
     phi M (A:clm E (topo_dual E)),
       is_bounded_bilinear_mapping phi M
       ( (u v:E), phi u v = (A u) v)
          norm A M.

Lemma coercivity_le_continuity:
   ¬ (Is_only_zero_set E)
    (phi:EER) M1 M2,
     is_bounded_bilinear_mapping phi M1
     is_coercive phi M2
       M2 M1.

End Bilin_rep.

Clm with subset

Decidability Is_only_zero_set subset
Operator norm subset

Section Op_norm_sub.

Context {E : NormedModule R_AbsRing}.
Context {F : NormedModule R_AbsRing}.
Variable phi :E Prop.

Definition operator_norm_phi (f:EF) : Rbar :=
   match Is_only_zero_set_dec_phi E phi with
    | left _Lub_Rbar (fun x u:E, u zero
                   phi u x = norm (f u) / norm u)
    | right _ ⇒ 0
  end.

Lemma operator_norm_ge_0_phi: f,
  Rbar_le 0 (operator_norm_phi f).

Lemma operator_norm_ge_0'_phi : f,
  0 (operator_norm_phi f).

Lemma operator_norm_helper'_phi:
     f, is_finite (operator_norm_phi f)
        ( u, u zero phi u norm (f u) operator_norm_phi f × norm u).

Lemma operator_norm_helper2_phi:
     f, is_finite (operator_norm_phi f)
       (Is_only_zero_set_phi E phi operator_norm_phi f = 0)
      (¬Is_only_zero_set_phi E phi M, 0 M
         ( u, u zero norm (f u) M × norm u)
            operator_norm_phi f M).

Lemma operator_norm_helper2'_phi:
     f, is_finite (operator_norm_phi f)
       (Is_only_zero_set_phi E phi operator_norm_phi f = 0)
      (¬Is_only_zero_set_phi E phi M, 0 M
         ( u, u zero phi u norm (f u) M × norm u)
            operator_norm_phi f M).

Lemma operator_norm_helper3_phi :
     f, M, 0 M
       ( u, u zero phi u norm (f u) M × norm u)
         is_finite (operator_norm_phi f).

Lemma operator_norm_helper3b_phi:
     f, M, 0 M
       ( u, u zero norm (f u) M × norm u)
         is_finite (operator_norm_phi f).

Lemma operator_norm_helper3'_phi:
     f, M, 0 M
       ( u, u zero phi u norm (f u) M × norm u)
         (operator_norm_phi f M).

Lemma coercivity_le_continuity_phi:
   ¬ (Is_only_zero_set_phi E phi)
    (p:EER) M1 M2,
     is_bounded_bilinear_mapping p M1
     is_coercive p M2
       M2 M1.

Lemma op_norm_finite_phi : f, is_finite (operator_norm f)
                   is_finite (operator_norm_phi f).

End Op_norm_sub.