Bounded linear maps #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines a class stating that a map between normed vector spaces is (bi)linear and
continuous.
Instead of asking for continuity, the definition takes the equivalent condition (because the space
is normed) that ‖f x‖ is bounded by a multiple of ‖x‖. Hence the "bounded" in the name refers to
‖f x‖/‖x‖ rather than ‖f x‖ itself.
Main definitions #
is_bounded_linear_map: Class stating that a mapf : E → Fis linear and has‖f x‖bounded by a multiple of‖x‖.is_bounded_bilinear_map: Class stating that a mapf : E × F → Gis bilinear and continuous, but through the simpler to provide statement that‖f (x, y)‖is bounded by a multiple of‖x‖ * ‖y‖is_bounded_bilinear_map.linear_deriv: Derivative of a continuous bilinear map as a linear map.is_bounded_bilinear_map.deriv: Derivative of a continuous bilinear map as a continuous linear map. The proof that it is indeed the derivative isis_bounded_bilinear_map.has_fderiv_atinanalysis.calculus.fderiv.
Main theorems #
is_bounded_bilinear_map.continuous: A bounded bilinear map is continuous.continuous_linear_equiv.is_open: The continuous linear equivalences are an open subset of the set of continuous linear maps between a pair of Banach spaces. Placed in this file because its proof usesis_bounded_bilinear_map.continuous.
Notes #
The main use of this file is is_bounded_bilinear_map. The file analysis.normed_space.multilinear
already expounds the theory of multilinear maps, but the 2-variables case is sufficiently simpler
to currently deserve its own treatment.
is_bounded_linear_map is effectively an unbundled version of continuous_linear_map (defined
in topology.algebra.module.basic, theory over normed spaces developed in
analysis.normed_space.operator_norm), albeit the name disparity. A bundled
continuous_linear_map is to be preferred over a is_bounded_linear_map hypothesis. Historical
artifact, really.
structure
is_bounded_linear_map
(𝕜 : Type u_5)
[normed_field 𝕜]
{E : Type u_6}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_7}
[normed_add_comm_group F]
[normed_space 𝕜 F]
(f : E → F) :
Prop
A function f satisfies is_bounded_linear_map 𝕜 f if it is linear and satisfies the
inequality ‖f x‖ ≤ M * ‖x‖ for some positive constant M.
theorem
is_linear_map.with_bound
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : E → F}
(hf : is_linear_map 𝕜 f)
(M : ℝ)
(h : ∀ (x : E), ‖f x‖ ≤ M * ‖x‖) :
theorem
continuous_linear_map.is_bounded_linear_map
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
(f : E →L[𝕜] F) :
A continuous linear map satisfies is_bounded_linear_map
def
is_bounded_linear_map.to_linear_map
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
(f : E → F)
(h : is_bounded_linear_map 𝕜 f) :
Construct a linear map from a function f satisfying is_bounded_linear_map 𝕜 f.
Equations
def
is_bounded_linear_map.to_continuous_linear_map
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : E → F}
(hf : is_bounded_linear_map 𝕜 f) :
Construct a continuous linear map from is_bounded_linear_map
Equations
- hf.to_continuous_linear_map = {to_linear_map := {to_fun := (is_bounded_linear_map.to_linear_map f hf).to_fun, map_add' := _, map_smul' := _}, cont := _}
theorem
is_bounded_linear_map.zero
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F] :
is_bounded_linear_map 𝕜 (λ (x : E), 0)
theorem
is_bounded_linear_map.id
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E] :
is_bounded_linear_map 𝕜 (λ (x : E), x)
theorem
is_bounded_linear_map.fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F] :
is_bounded_linear_map 𝕜 (λ (x : E × F), x.fst)
theorem
is_bounded_linear_map.snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F] :
is_bounded_linear_map 𝕜 (λ (x : E × F), x.snd)
theorem
is_bounded_linear_map.smul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : E → F}
(c : 𝕜)
(hf : is_bounded_linear_map 𝕜 f) :
is_bounded_linear_map 𝕜 (c • f)
theorem
is_bounded_linear_map.neg
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : E → F}
(hf : is_bounded_linear_map 𝕜 f) :
is_bounded_linear_map 𝕜 (λ (e : E), -f e)
theorem
is_bounded_linear_map.add
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f g : E → F}
(hf : is_bounded_linear_map 𝕜 f)
(hg : is_bounded_linear_map 𝕜 g) :
is_bounded_linear_map 𝕜 (λ (e : E), f e + g e)
theorem
is_bounded_linear_map.sub
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f g : E → F}
(hf : is_bounded_linear_map 𝕜 f)
(hg : is_bounded_linear_map 𝕜 g) :
is_bounded_linear_map 𝕜 (λ (e : E), f e - g e)
theorem
is_bounded_linear_map.comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f : E → F}
{g : F → G}
(hg : is_bounded_linear_map 𝕜 g)
(hf : is_bounded_linear_map 𝕜 f) :
is_bounded_linear_map 𝕜 (g ∘ f)
@[protected]
theorem
is_bounded_linear_map.tendsto
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : E → F}
(x : E)
(hf : is_bounded_linear_map 𝕜 f) :
filter.tendsto f (nhds x) (nhds (f x))
theorem
is_bounded_linear_map.continuous
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : E → F}
(hf : is_bounded_linear_map 𝕜 f) :
theorem
is_bounded_linear_map.lim_zero_bounded_linear_map
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : E → F}
(hf : is_bounded_linear_map 𝕜 f) :
filter.tendsto f (nhds 0) (nhds 0)
theorem
is_bounded_linear_map.is_O_id
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : E → F}
(h : is_bounded_linear_map 𝕜 f)
(l : filter E) :
theorem
is_bounded_linear_map.is_O_comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{E : Type u_2}
{g : F → G}
(hg : is_bounded_linear_map 𝕜 g)
{f : E → F}
(l : filter E) :
theorem
is_bounded_linear_map.is_O_sub
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : E → F}
(h : is_bounded_linear_map 𝕜 f)
(l : filter E)
(x : E) :
theorem
is_bounded_linear_map_prod_multilinear
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{ι : Type u_5}
[fintype ι]
{E : ι → Type u_2}
[Π (i : ι), normed_add_comm_group (E i)]
[Π (i : ι), normed_space 𝕜 (E i)] :
is_bounded_linear_map 𝕜 (λ (p : continuous_multilinear_map 𝕜 E F × continuous_multilinear_map 𝕜 E G), p.fst.prod p.snd)
Taking the cartesian product of two continuous multilinear maps is a bounded linear operation.
theorem
is_bounded_linear_map_continuous_multilinear_map_comp_linear
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{ι : Type u_5}
[fintype ι]
(g : G →L[𝕜] E) :
is_bounded_linear_map 𝕜 (λ (f : continuous_multilinear_map 𝕜 (λ (i : ι), E) F), f.comp_continuous_linear_map (λ (_x : ι), g))
Given a fixed continuous linear map g, associating to a continuous multilinear map f the
continuous multilinear map f (g m₁, ..., g mₙ) is a bounded linear operation.
We prove some computation rules for continuous (semi-)bilinear maps in their first argument.
If f is a continuuous bilinear map, to use the corresponding rules for the second argument, use
(f _).map_add and similar.
We have to assume that F and G are normed spaces in this section, to use
continuous_linear_map.to_normed_add_comm_group, but we don't need to assume this for the first
argument of f.
theorem
continuous_linear_map.map_add₂
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{R : Type u_5}
{𝕜₂ : Type u_6}
{𝕜' : Type u_7}
[nontrivially_normed_field 𝕜']
[nontrivially_normed_field 𝕜₂]
{M : Type u_8}
[topological_space M]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{G' : Type u_9}
[normed_add_comm_group G']
[normed_space 𝕜₂ G']
[normed_space 𝕜' G']
[smul_comm_class 𝕜₂ 𝕜' G']
[semiring R]
[add_comm_monoid M]
[module R M]
{ρ₁₂ : R →+* 𝕜'}
(f : M →SL[ρ₁₂] F →SL[σ₁₂] G')
(x x' : M)
(y : F) :
theorem
continuous_linear_map.map_zero₂
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{R : Type u_5}
{𝕜₂ : Type u_6}
{𝕜' : Type u_7}
[nontrivially_normed_field 𝕜']
[nontrivially_normed_field 𝕜₂]
{M : Type u_8}
[topological_space M]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{G' : Type u_9}
[normed_add_comm_group G']
[normed_space 𝕜₂ G']
[normed_space 𝕜' G']
[smul_comm_class 𝕜₂ 𝕜' G']
[semiring R]
[add_comm_monoid M]
[module R M]
{ρ₁₂ : R →+* 𝕜'}
(f : M →SL[ρ₁₂] F →SL[σ₁₂] G')
(y : F) :
theorem
continuous_linear_map.map_smulₛₗ₂
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{R : Type u_5}
{𝕜₂ : Type u_6}
{𝕜' : Type u_7}
[nontrivially_normed_field 𝕜']
[nontrivially_normed_field 𝕜₂]
{M : Type u_8}
[topological_space M]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{G' : Type u_9}
[normed_add_comm_group G']
[normed_space 𝕜₂ G']
[normed_space 𝕜' G']
[smul_comm_class 𝕜₂ 𝕜' G']
[semiring R]
[add_comm_monoid M]
[module R M]
{ρ₁₂ : R →+* 𝕜'}
(f : M →SL[ρ₁₂] F →SL[σ₁₂] G')
(c : R)
(x : M)
(y : F) :
theorem
continuous_linear_map.map_sub₂
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{R : Type u_5}
{𝕜₂ : Type u_6}
{𝕜' : Type u_7}
[nontrivially_normed_field 𝕜']
[nontrivially_normed_field 𝕜₂]
{M : Type u_8}
[topological_space M]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{G' : Type u_9}
[normed_add_comm_group G']
[normed_space 𝕜₂ G']
[normed_space 𝕜' G']
[smul_comm_class 𝕜₂ 𝕜' G']
[ring R]
[add_comm_group M]
[module R M]
{ρ₁₂ : R →+* 𝕜'}
(f : M →SL[ρ₁₂] F →SL[σ₁₂] G')
(x x' : M)
(y : F) :
theorem
continuous_linear_map.map_neg₂
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{R : Type u_5}
{𝕜₂ : Type u_6}
{𝕜' : Type u_7}
[nontrivially_normed_field 𝕜']
[nontrivially_normed_field 𝕜₂]
{M : Type u_8}
[topological_space M]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{G' : Type u_9}
[normed_add_comm_group G']
[normed_space 𝕜₂ G']
[normed_space 𝕜' G']
[smul_comm_class 𝕜₂ 𝕜' G']
[ring R]
[add_comm_group M]
[module R M]
{ρ₁₂ : R →+* 𝕜'}
(f : M →SL[ρ₁₂] F →SL[σ₁₂] G')
(x : M)
(y : F) :
theorem
continuous_linear_map.map_smul₂
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
(f : E →L[𝕜] F →L[𝕜] G)
(c : 𝕜)
(x : E)
(y : F) :
structure
is_bounded_bilinear_map
(𝕜 : Type u_1)
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
(f : E × F → G) :
Prop
- add_left : ∀ (x₁ x₂ : E) (y : F), f (x₁ + x₂, y) = f (x₁, y) + f (x₂, y)
- smul_left : ∀ (c : 𝕜) (x : E) (y : F), f (c • x, y) = c • f (x, y)
- add_right : ∀ (x : E) (y₁ y₂ : F), f (x, y₁ + y₂) = f (x, y₁) + f (x, y₂)
- smul_right : ∀ (c : 𝕜) (x : E) (y : F), f (x, c • y) = c • f (x, y)
- bound : ∃ (C : ℝ) (H : C > 0), ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖
A map f : E × F → G satisfies is_bounded_bilinear_map 𝕜 f if it is bilinear and
continuous.
theorem
continuous_linear_map.is_bounded_bilinear_map
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
(f : E →L[𝕜] F →L[𝕜] G) :
@[protected]
theorem
is_bounded_bilinear_map.is_O
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f : E × F → G}
(h : is_bounded_bilinear_map 𝕜 f) :
theorem
is_bounded_bilinear_map.is_O_comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f : E × F → G}
{α : Type u_5}
(H : is_bounded_bilinear_map 𝕜 f)
{g : α → E}
{h : α → F}
{l : filter α} :
@[protected]
theorem
is_bounded_bilinear_map.is_O'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f : E × F → G}
(h : is_bounded_bilinear_map 𝕜 f) :
theorem
is_bounded_bilinear_map.map_sub_left
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f : E × F → G}
(h : is_bounded_bilinear_map 𝕜 f)
{x y : E}
{z : F} :
theorem
is_bounded_bilinear_map.map_sub_right
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f : E × F → G}
(h : is_bounded_bilinear_map 𝕜 f)
{x : E}
{y z : F} :
theorem
is_bounded_bilinear_map.continuous
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f : E × F → G}
(h : is_bounded_bilinear_map 𝕜 f) :
Useful to use together with continuous.comp₂.
theorem
is_bounded_bilinear_map.continuous_left
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f : E × F → G}
(h : is_bounded_bilinear_map 𝕜 f)
{e₂ : F} :
continuous (λ (e₁ : E), f (e₁, e₂))
theorem
is_bounded_bilinear_map.continuous_right
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f : E × F → G}
(h : is_bounded_bilinear_map 𝕜 f)
{e₁ : E} :
continuous (λ (e₂ : F), f (e₁, e₂))
theorem
continuous_linear_map.continuous₂
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
(f : E →L[𝕜] F →L[𝕜] G) :
continuous (function.uncurry (λ (x : E) (y : F), ⇑(⇑f x) y))
Useful to use together with continuous.comp₂.
theorem
is_bounded_bilinear_map.is_bounded_linear_map_left
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f : E × F → G}
(h : is_bounded_bilinear_map 𝕜 f)
(y : F) :
is_bounded_linear_map 𝕜 (λ (x : E), f (x, y))
theorem
is_bounded_bilinear_map.is_bounded_linear_map_right
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f : E × F → G}
(h : is_bounded_bilinear_map 𝕜 f)
(x : E) :
is_bounded_linear_map 𝕜 (λ (y : F), f (x, y))
theorem
is_bounded_bilinear_map_smul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{𝕜' : Type u_2}
[normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{E : Type u_3}
[normed_add_comm_group E]
[normed_space 𝕜 E]
[normed_space 𝕜' E]
[is_scalar_tower 𝕜 𝕜' E] :
is_bounded_bilinear_map 𝕜 (λ (p : 𝕜' × E), p.fst • p.snd)
theorem
is_bounded_bilinear_map_mul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜] :
is_bounded_bilinear_map 𝕜 (λ (p : 𝕜 × 𝕜), p.fst * p.snd)
theorem
is_bounded_bilinear_map_comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G] :
theorem
continuous_linear_map.is_bounded_linear_map_comp_left
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
(g : F →L[𝕜] G) :
is_bounded_linear_map 𝕜 (λ (f : E →L[𝕜] F), g.comp f)
theorem
continuous_linear_map.is_bounded_linear_map_comp_right
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
(f : E →L[𝕜] F) :
is_bounded_linear_map 𝕜 (λ (g : F →L[𝕜] G), g.comp f)
theorem
is_bounded_bilinear_map_apply
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F] :
theorem
is_bounded_bilinear_map_smul_right
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F] :
is_bounded_bilinear_map 𝕜 (λ (p : (E →L[𝕜] 𝕜) × F), p.fst.smul_right p.snd)
The function continuous_linear_map.smul_right, associating to a continuous linear map
f : E → 𝕜 and a scalar c : F the tensor product f ⊗ c as a continuous linear map from E to
F, is a bounded bilinear map.
theorem
is_bounded_bilinear_map_comp_multilinear
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{ι : Type u_2}
{E : ι → Type u_5}
[fintype ι]
[Π (i : ι), normed_add_comm_group (E i)]
[Π (i : ι), normed_space 𝕜 (E i)] :
is_bounded_bilinear_map 𝕜 (λ (p : (F →L[𝕜] G) × continuous_multilinear_map 𝕜 E F), p.fst.comp_continuous_multilinear_map p.snd)
The composition of a continuous linear map with a continuous multilinear map is a bounded bilinear operation.
def
is_bounded_bilinear_map.linear_deriv
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f : E × F → G}
(h : is_bounded_bilinear_map 𝕜 f)
(p : E × F) :
Definition of the derivative of a bilinear map f, given at a point p by
q ↦ f(p.1, q.2) + f(q.1, p.2) as in the standard formula for the derivative of a product.
We define this function here as a linear map E × F →ₗ[𝕜] G, then is_bounded_bilinear_map.deriv
strengthens it to a continuous linear map E × F →L[𝕜] G.
``.
def
is_bounded_bilinear_map.deriv
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f : E × F → G}
(h : is_bounded_bilinear_map 𝕜 f)
(p : E × F) :
The derivative of a bounded bilinear map at a point p : E × F, as a continuous linear map
from E × F to G. The statement that this is indeed the derivative of f is
is_bounded_bilinear_map.has_fderiv_at in analysis.calculus.fderiv.
Equations
- h.deriv p = (h.linear_deriv p).mk_continuous_of_exists_bound _
@[simp]
theorem
is_bounded_bilinear_map_deriv_coe
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f : E × F → G}
(h : is_bounded_bilinear_map 𝕜 f)
(p q : E × F) :
theorem
continuous_linear_map.mul_left_right_is_bounded_bilinear
(𝕜 : Type u_1)
[nontrivially_normed_field 𝕜]
(𝕜' : Type u_2)
[normed_ring 𝕜']
[normed_algebra 𝕜 𝕜'] :
is_bounded_bilinear_map 𝕜 (λ (p : 𝕜' × 𝕜'), ⇑(⇑(continuous_linear_map.mul_left_right 𝕜 𝕜') p.fst) p.snd)
The function continuous_linear_map.mul_left_right : 𝕜' × 𝕜' → (𝕜' →L[𝕜] 𝕜') is a bounded
bilinear map.
theorem
is_bounded_bilinear_map.is_bounded_linear_map_deriv
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f : E × F → G}
(h : is_bounded_bilinear_map 𝕜 f) :
is_bounded_linear_map 𝕜 (λ (p : E × F), h.deriv p)
Given a bounded bilinear map f, the map associating to a point p the derivative of f at
p is itself a bounded linear map.
theorem
continuous.clm_comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{X : Type u_5}
[topological_space X]
{g : X → (F →L[𝕜] G)}
{f : X → (E →L[𝕜] F)}
(hg : continuous g)
(hf : continuous f) :
continuous (λ (x : X), (g x).comp (f x))
theorem
continuous_on.clm_comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{X : Type u_5}
[topological_space X]
{g : X → (F →L[𝕜] G)}
{f : X → (E →L[𝕜] F)}
{s : set X}
(hg : continuous_on g s)
(hf : continuous_on f s) :
continuous_on (λ (x : X), (g x).comp (f x)) s
The set of continuous linear equivalences between two Banach spaces is open #
In this section we establish that the set of continuous linear equivalences between two Banach spaces is an open subset of the space of linear maps between them.
@[protected]
theorem
continuous_linear_equiv.is_open
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
[complete_space E] :
@[protected]
theorem
continuous_linear_equiv.nhds
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
[complete_space E]
(e : E ≃L[𝕜] F) :