# mathlibdocumentation

analysis.normed_space.bounded_linear_maps

structure is_bounded_linear_map (𝕜 : Type u_5) [normed_field 𝕜] {E : Type u_6} [normed_group E] [ E] {F : Type u_7} [normed_group 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} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {f : E → F} (hf : f) (M : ) :
(∀ (x : E), f x M * x)

theorem continuous_linear_map.is_bounded_linear_map {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ 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} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] (f : E → 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} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {f : E → F} :
(E →L[𝕜] F)

Construct a continuous linear map from is_bounded_linear_map

Equations
theorem is_bounded_linear_map.zero {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] :
(λ (x : E), 0)

theorem is_bounded_linear_map.id {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] :
(λ (x : E), x)

theorem is_bounded_linear_map.fst {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] :
(λ (x : E × F), x.fst)

theorem is_bounded_linear_map.snd {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] :
(λ (x : E × F), x.snd)

theorem is_bounded_linear_map.smul {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {f : E → F} (c : 𝕜) :
(λ (e : E), c f e)

theorem is_bounded_linear_map.neg {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {f : E → F} :
(λ (e : E), -f e)

theorem is_bounded_linear_map.add {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {f g : E → F} :
(λ (e : E), f e + g e)

theorem is_bounded_linear_map.sub {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {f g : E → F} :
(λ (e : E), f e - g e)

theorem is_bounded_linear_map.comp {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] {f : E → F} {g : F → G} :
(g f)

theorem is_bounded_linear_map.tendsto {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {f : E → F} (x : E) :
(𝓝 x) (𝓝 (f x))

theorem is_bounded_linear_map.continuous {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {f : E → F} :

theorem is_bounded_linear_map.lim_zero_bounded_linear_map {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {f : E → F} :
(𝓝 0) (𝓝 0)

theorem is_bounded_linear_map.is_O_id {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {f : E → F} (h : f) (l : filter E) :
(λ (x : E), x) l

theorem is_bounded_linear_map.is_O_comp {𝕜 : Type u_1} {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] {E : Type u_2} {g : F → G} (hg : 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} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {f : E → F} (h : 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} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] :
(λ (p : (E →L[𝕜] F) × (E →L[𝕜] G)), p.fst.prod p.snd)

Taking the cartesian product of two continuous linear maps is a bounded linear operation.

theorem is_bounded_linear_map_prod_multilinear {𝕜 : Type u_1} {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] {ι : Type u_5} [decidable_eq ι] [fintype ι] {E : ι → Type u_2} [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] :
(λ (p : , 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} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] {ι : Type u_5} [decidable_eq ι] [fintype ι] (g : G →L[𝕜] E) :
(λ (f : (λ (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.

structure is_bounded_bilinear_map (𝕜 : Type u_1) {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ 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} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] {f : E × F → G} :
(λ (p : E × F), p.fst * p.snd)

theorem is_bounded_bilinear_map.is_O_comp {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] {f : E × F → G} {α : Type u_5} (H : f) {g : α → E} {h : α → F} {l : filter α} :
asymptotics.is_O (λ (x : α), f (g x, h x)) (λ (x : α), g x * h x) l

theorem is_bounded_bilinear_map.is_O' {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] {f : E × F → G} :
(λ (p : E × F), p * p)

theorem is_bounded_bilinear_map.map_sub_left {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] {f : E × F → G} (h : f) {x y : E} {z : F} :
f (x - y, z) = f (x, z) - f (y, z)

theorem is_bounded_bilinear_map.map_sub_right {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] {f : E × F → G} (h : f) {x : E} {y z : F} :
f (x, y - z) = f (x, y) - f (x, z)

theorem is_bounded_bilinear_map.is_bounded_linear_map_left {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] {f : E × F → G} (h : f) (y : F) :
(λ (x : E), f (x, y))

theorem is_bounded_bilinear_map.is_bounded_linear_map_right {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] {f : E × F → G} (h : f) (x : E) :
(λ (y : F), f (x, y))

theorem is_bounded_bilinear_map_smul {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] :
(λ (p : 𝕜 × E), p.fst p.snd)

theorem is_bounded_bilinear_map_smul_algebra {𝕜 : Type u_1} {𝕜' : Type u_2} [normed_field 𝕜'] [ 𝕜'] {E : Type u_3} [normed_group E] [ E] [ E] [ 𝕜' E] :
(λ (p : 𝕜' × E), p.fst p.snd)

theorem is_bounded_bilinear_map_mul {𝕜 : Type u_1}  :
(λ (p : 𝕜 × 𝕜), (p.fst) * p.snd)

theorem is_bounded_bilinear_map_comp {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] :
(λ (p : (E →L[𝕜] F) × (F →L[𝕜] G)), p.snd.comp p.fst)

theorem continuous_linear_map.is_bounded_linear_map_comp_left {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] (g : F →L[𝕜] G) :
(λ (f : E →L[𝕜] F), g.comp f)

theorem continuous_linear_map.is_bounded_linear_map_comp_right {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] (f : E →L[𝕜] F) :
(λ (g : F →L[𝕜] G), g.comp f)

theorem is_bounded_bilinear_map_apply {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] :
(λ (p : (E →L[𝕜] F) × E), (p.fst) p.snd)

theorem is_bounded_bilinear_map_smul_right {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] :
(λ (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} {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] {ι : Type u_2} {E : ι → Type u_5} [decidable_eq ι] [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), (E i)] :
(λ (p : (F →L[𝕜] G) × ,

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} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] {f : E × F → G} :
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

Equations
def is_bounded_bilinear_map.deriv {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] {f : E × F → G} :
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
@[simp]
theorem is_bounded_bilinear_map_deriv_coe {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] {f : E × F → G} (h : f) (p q : E × F) :
(h.deriv p) q = f (p.fst, q.snd) + f (q.fst, p.snd)

theorem continuous_linear_map.lmul_left_right_is_bounded_bilinear (𝕜 : Type u_1) (𝕜' : Type u_2) [normed_ring 𝕜'] [ 𝕜'] :

The function lmul_left_right : 𝕜' × 𝕜' → (𝕜' →L[𝕜] 𝕜') is a bounded bilinear map.

theorem is_bounded_bilinear_map.is_bounded_linear_map_deriv {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] {f : E × F → G} (h : f) :
(λ (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.