# 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}.

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