structure
is_bounded_linear_map
(𝕜 : Type u_5)
[normed_field 𝕜]
{E : Type u_6}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_7}
[normed_group F]
[normed_space 𝕜 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}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F]
{f : E → F}
(hf : is_linear_map 𝕜 f)
(M : ℝ) :
theorem
continuous_linear_map.is_bounded_linear_map
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_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}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F]
(f : E → F) :
is_bounded_linear_map 𝕜 f → (E →ₗ[𝕜] 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}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F]
{f : E → F} :
is_bounded_linear_map 𝕜 f → (E →L[𝕜] 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}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F] :
is_bounded_linear_map 𝕜 (λ (x : E), 0)
theorem
is_bounded_linear_map.id
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E] :
is_bounded_linear_map 𝕜 (λ (x : E), x)
theorem
is_bounded_linear_map.fst
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F] :
is_bounded_linear_map 𝕜 (λ (x : E × F), x.fst)
theorem
is_bounded_linear_map.snd
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F] :
is_bounded_linear_map 𝕜 (λ (x : E × F), x.snd)
theorem
is_bounded_linear_map.smul
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F]
{f : E → F}
(c : 𝕜) :
is_bounded_linear_map 𝕜 f → is_bounded_linear_map 𝕜 (λ (e : E), c • f e)
theorem
is_bounded_linear_map.neg
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F]
{f : E → F} :
is_bounded_linear_map 𝕜 f → is_bounded_linear_map 𝕜 (λ (e : E), -f e)
theorem
is_bounded_linear_map.add
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F]
{f g : E → F} :
is_bounded_linear_map 𝕜 f → is_bounded_linear_map 𝕜 g → is_bounded_linear_map 𝕜 (λ (e : E), f e + g e)
theorem
is_bounded_linear_map.sub
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F]
{f g : E → F} :
is_bounded_linear_map 𝕜 f → is_bounded_linear_map 𝕜 g → is_bounded_linear_map 𝕜 (λ (e : E), f e - g e)
theorem
is_bounded_linear_map.comp
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_group G]
[normed_space 𝕜 G]
{f : E → F}
{g : F → G} :
is_bounded_linear_map 𝕜 g → is_bounded_linear_map 𝕜 f → is_bounded_linear_map 𝕜 (g ∘ f)
theorem
is_bounded_linear_map.tendsto
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F]
{f : E → F}
(x : E) :
is_bounded_linear_map 𝕜 f → filter.tendsto f (nhds x) (nhds (f x))
theorem
is_bounded_linear_map.continuous
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F]
{f : E → F} :
is_bounded_linear_map 𝕜 f → continuous f
theorem
is_bounded_linear_map.lim_zero_bounded_linear_map
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F]
{f : E → F} :
is_bounded_linear_map 𝕜 f → filter.tendsto f (nhds 0) (nhds 0)
theorem
is_bounded_linear_map.is_O_id
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F]
{f : E → F}
(h : is_bounded_linear_map 𝕜 f)
(l : filter E) :
asymptotics.is_O f (λ (x : E), x) l
theorem
is_bounded_linear_map.is_O_comp
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_group G]
[normed_space 𝕜 G]
{E : Type u_2}
{g : F → G}
(hg : is_bounded_linear_map 𝕜 g)
{f : E → F}
(l : filter E) :
asymptotics.is_O (λ (x' : E), g (f x')) f l
theorem
is_bounded_linear_map.is_O_sub
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F]
{f : E → F}
(h : is_bounded_linear_map 𝕜 f)
(l : filter E)
(x : E) :
asymptotics.is_O (λ (x' : E), f (x' - x)) (λ (x' : E), x' - x) l
theorem
is_bounded_linear_map_prod_iso
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_group G]
[normed_space 𝕜 G] :
Taking the cartesian product of two continuous linear maps is a bounded linear operation.
theorem
is_bounded_linear_map_prod_multilinear
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_group G]
[normed_space 𝕜 G]
{ι : Type u_5}
[decidable_eq ι]
[fintype ι]
{E : ι → Type u_2}
[Π (i : ι), normed_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}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_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), continuous_multilinear_map.comp_continuous_linear_map 𝕜 E f 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.
structure
is_bounded_bilinear_map
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_group G]
[normed_space 𝕜 G] :
(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
is_bounded_bilinear_map.is_O
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_group G]
[normed_space 𝕜 G]
{f : E × F → G} :
theorem
is_bounded_bilinear_map.is_O_comp
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_group G]
[normed_space 𝕜 G]
{f : E × F → G}
{α : Type u_5}
(H : is_bounded_bilinear_map 𝕜 f)
{g : α → E}
{h : α → F}
{l : filter α} :
theorem
is_bounded_bilinear_map.is_O'
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_group G]
[normed_space 𝕜 G]
{f : E × F → G} :
is_bounded_bilinear_map 𝕜 f → asymptotics.is_O f (λ (p : E × F), ∥p∥ * ∥p∥) ⊤
theorem
is_bounded_bilinear_map.map_sub_left
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_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}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_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.is_bounded_linear_map_left
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_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}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_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}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E] :
is_bounded_bilinear_map 𝕜 (λ (p : 𝕜 × E), p.fst • p.snd)
theorem
is_bounded_bilinear_map_smul_algebra
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{𝕜' : Type u_2}
[normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{E : Type u_3}
[normed_group E]
[normed_space 𝕜' E] :
is_bounded_bilinear_map 𝕜 (λ (p : 𝕜' × semimodule.restrict_scalars 𝕜 𝕜' E), p.fst • p.snd)
theorem
is_bounded_bilinear_map_mul
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜] :
is_bounded_bilinear_map 𝕜 (λ (p : 𝕜 × 𝕜), p.fst * p.snd)
theorem
is_bounded_bilinear_map_comp
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_group G]
[normed_space 𝕜 G] :
theorem
continuous_linear_map.is_bounded_linear_map_comp_left
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_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}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_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}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F] :
theorem
is_bounded_bilinear_map_smul_right
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_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}
[nondiscrete_normed_field 𝕜]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_group G]
[normed_space 𝕜 G]
{ι : Type u_2}
{E : ι → Type u_5}
[decidable_eq ι]
[fintype ι]
[Π (i : ι), normed_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}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_group G]
[normed_space 𝕜 G]
{f : E × F → G} :
is_bounded_bilinear_map 𝕜 f → E × F → (E × F →ₗ[𝕜] G)
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 a bounded linear map from E × F to G. The fact that this
is indeed the derivative of f is proved in is_bounded_bilinear_map.has_fderiv_at in
fderiv.lean
def
is_bounded_bilinear_map.deriv
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_group G]
[normed_space 𝕜 G]
{f : E × F → G} :
is_bounded_bilinear_map 𝕜 f → E × F → (E × F →L[𝕜] G)
The derivative of a bounded bilinear map at a point p : E × F, as a continuous linear map
from E × F to G.
Equations
- h.deriv p = (h.linear_deriv p).mk_continuous_of_exists_bound _
@[simp]
theorem
is_bounded_bilinear_map_deriv_coe
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_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)
[nondiscrete_normed_field 𝕜]
(𝕜' : Type u_2)
[normed_ring 𝕜']
[normed_algebra 𝕜 𝕜'] :
The function lmul_left_right : 𝕜' × 𝕜' → (𝕜' →L[𝕜] 𝕜') is a bounded bilinear map.
theorem
is_bounded_bilinear_map.is_bounded_linear_map_deriv
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_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.