Bounded linear maps #
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}
[decidable_eq ι]
[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}
[decidable_eq ι]
[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]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
{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]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
{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]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
{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]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
{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]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
{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}
[decidable_eq ι]
[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.
``.
noncomputable
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.lmul_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.lmul_left_right 𝕜 𝕜') p.fst) p.snd)
The function lmul_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) :