mathlib documentation

analysis.normed_space.bounded_linear_maps

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 : ℝ) :
(∀ (x : E), ∥f x∥ ≤ M * ∥x∥) → is_bounded_linear_map 𝕜 f

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
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 (𝓝 x) (𝓝 (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} :

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] :
is_bounded_linear_map 𝕜 (λ (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} [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), 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) [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 α} :
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} [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.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} :
f (x - y, z) = f (x, z) - f (y, z)

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} :
f (x, y - z) = f (x, y) - f (x, z)

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] [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} [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] :
is_bounded_bilinear_map 𝕜 (λ (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} [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] :
is_bounded_bilinear_map 𝕜 (λ (p : (E →L[𝕜] F) × E), ⇑(p.fst) p.snd)

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)] :

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

Equations
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
@[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) :
⇑(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) [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.