mathlib3 documentation

analysis.normed_space.continuous_linear_map

Constructions of continuous linear maps between (semi-)normed spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A fundamental fact about (semi-)linear maps between normed spaces over sensible fields is that continuity and boundedness are equivalent conditions. That is, for normed spaces E, F, a linear_map f : E →ₛₗ[σ] F is the coercion of some continuous_linear_map f' : E →SL[σ] F, if and only if there exists a bound C such that for all x, ‖f x‖ ≤ C * ‖x‖.

We prove one direction in this file: linear_map.mk_continuous, boundedness implies continuity. The other direction, continuous_linear_map.bound, is deferred to a later file, where the strong operator topology on E →SL[σ] F is available, because it is natural to use continuous_linear_map.bound to define a norm ⨆ x, ‖f x‖ / ‖x‖ on E →SL[σ] F and to show that this is compatible with the strong operator topology.

This file also contains several corollaries of linear_map.mk_continuous: other "easy" constructions of continuous linear maps between normed spaces.

This file is meant to be lightweight (it is imported by much of the analysis library); think twice before adding imports!

General constructions #

def linear_map.mk_continuous {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [ring 𝕜] [ring 𝕜₂] [seminormed_add_comm_group E] [seminormed_add_comm_group F] [module 𝕜 E] [module 𝕜₂ F] {σ : 𝕜 →+* 𝕜₂} (f : E →ₛₗ[σ] F) (C : ℝ) (h : ∀ (x : E), ‖⇑f x‖ ≤ C * ‖x‖) :

Construct a continuous linear map from a linear map and a bound on this linear map. The fact that the norm of the continuous linear map is then controlled is given in linear_map.mk_continuous_norm_le.

Equations

f.mk_continuous C h = {to_linear_map := f, cont := _}

def linear_map.mk_continuous_of_exists_bound {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [ring 𝕜] [ring 𝕜₂] [seminormed_add_comm_group E] [seminormed_add_comm_group F] [module 𝕜 E] [module 𝕜₂ F] {σ : 𝕜 →+* 𝕜₂} (f : E →ₛₗ[σ] F) (h : ∃ (C : ℝ), ∀ (x : E), ‖⇑f x‖ ≤ C * ‖x‖) :

Construct a continuous linear map from a linear map and the existence of a bound on this linear map. If you have an explicit bound, use linear_map.mk_continuous instead, as a norm estimate will follow automatically in linear_map.mk_continuous_norm_le.

Equations

f.mk_continuous_of_exists_bound h = {to_linear_map := f, cont := _}
_ = _

theorem continuous_of_linear_of_boundₛₗ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [ring 𝕜] [ring 𝕜₂] [seminormed_add_comm_group E] [seminormed_add_comm_group F] [module 𝕜 E] [module 𝕜₂ F] {σ : 𝕜 →+* 𝕜₂} {f : E → F} (h_add : ∀ (x y : E), f (x + y) = f x + f y) (h_smul : ∀ (c : 𝕜) (x : E), f (c • x) = ⇑σ c • f x) {C : ℝ} (h_bound : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖) :

theorem continuous_of_linear_of_bound {𝕜 : Type u_1} {E : Type u_3} {G : Type u_5} [ring 𝕜] [seminormed_add_comm_group E] [seminormed_add_comm_group G] [module 𝕜 E] [module 𝕜 G] {f : E → G} (h_add : ∀ (x y : E), f (x + y) = f x + f y) (h_smul : ∀ (c : 𝕜) (x : E), f (c • x) = c • f x) {C : ℝ} (h_bound : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖) :

@[simp, norm_cast]

theorem linear_map.mk_continuous_coe {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [ring 𝕜] [ring 𝕜₂] [seminormed_add_comm_group E] [seminormed_add_comm_group F] [module 𝕜 E] [module 𝕜₂ F] {σ : 𝕜 →+* 𝕜₂} (f : E →ₛₗ[σ] F) (C : ℝ) (h : ∀ (x : E), ‖⇑f x‖ ≤ C * ‖x‖) :

↑(f.mk_continuous C h) = f

@[simp]

theorem linear_map.mk_continuous_apply {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [ring 𝕜] [ring 𝕜₂] [seminormed_add_comm_group E] [seminormed_add_comm_group F] [module 𝕜 E] [module 𝕜₂ F] {σ : 𝕜 →+* 𝕜₂} (f : E →ₛₗ[σ] F) (C : ℝ) (h : ∀ (x : E), ‖⇑f x‖ ≤ C * ‖x‖) (x : E) :

⇑(f.mk_continuous C h) x = ⇑f x

@[simp, norm_cast]

theorem linear_map.mk_continuous_of_exists_bound_coe {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [ring 𝕜] [ring 𝕜₂] [seminormed_add_comm_group E] [seminormed_add_comm_group F] [module 𝕜 E] [module 𝕜₂ F] {σ : 𝕜 →+* 𝕜₂} (f : E →ₛₗ[σ] F) (h : ∃ (C : ℝ), ∀ (x : E), ‖⇑f x‖ ≤ C * ‖x‖) :

↑(f.mk_continuous_of_exists_bound h) = f

@[simp]

theorem linear_map.mk_continuous_of_exists_bound_apply {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [ring 𝕜] [ring 𝕜₂] [seminormed_add_comm_group E] [seminormed_add_comm_group F] [module 𝕜 E] [module 𝕜₂ F] {σ : 𝕜 →+* 𝕜₂} (f : E →ₛₗ[σ] F) (h : ∃ (C : ℝ), ∀ (x : E), ‖⇑f x‖ ≤ C * ‖x‖) (x : E) :

⇑(f.mk_continuous_of_exists_bound h) x = ⇑f x

theorem continuous_linear_map.antilipschitz_of_bound {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [ring 𝕜] [ring 𝕜₂] [seminormed_add_comm_group E] [seminormed_add_comm_group F] [module 𝕜 E] [module 𝕜₂ F] {σ : 𝕜 →+* 𝕜₂} (f : E →SL[σ] F) {K : nnreal} (h : ∀ (x : E), ‖x‖ ≤ ↑K * ‖⇑f x‖) :

antilipschitz_with K ⇑f

theorem continuous_linear_map.bound_of_antilipschitz {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [ring 𝕜] [ring 𝕜₂] [seminormed_add_comm_group E] [seminormed_add_comm_group F] [module 𝕜 E] [module 𝕜₂ F] {σ : 𝕜 →+* 𝕜₂} (f : E →SL[σ] F) {K : nnreal} (h : antilipschitz_with K ⇑f) (x : E) :

‖x‖ ≤ ↑K * ‖⇑f x‖

def linear_equiv.to_continuous_linear_equiv_of_bounds {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [ring 𝕜] [ring 𝕜₂] [seminormed_add_comm_group E] [seminormed_add_comm_group F] [module 𝕜 E] [module 𝕜₂ F] {σ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [ring_hom_inv_pair σ σ₂₁] [ring_hom_inv_pair σ₂₁ σ] (e : E ≃ₛₗ[σ] F) (C_to C_inv : ℝ) (h_to : ∀ (x : E), ‖⇑e x‖ ≤ C_to * ‖x‖) (h_inv : ∀ (x : F), ‖⇑(e.symm) x‖ ≤ C_inv * ‖x‖) :

Construct a continuous linear equivalence from a linear equivalence together with bounds in both directions.

Equations

e.to_continuous_linear_equiv_of_bounds C_to C_inv h_to h_inv = {to_linear_equiv := e, continuous_to_fun := _, continuous_inv_fun := _}

def linear_map.to_continuous_linear_map₁ {𝕜 : Type u_1} {E : Type u_3} [semi_normed_ring 𝕜] [seminormed_add_comm_group E] [module 𝕜 E] [has_bounded_smul 𝕜 E] (f : 𝕜 →ₗ[𝕜] E) :

𝕜 →L[𝕜] E

Reinterpret a linear map 𝕜 →ₗ[𝕜] E as a continuous linear map. This construction is generalized to the case of any finite dimensional domain in linear_map.to_continuous_linear_map.

Equations

f.to_continuous_linear_map₁ = f.mk_continuous ‖⇑f 1‖ _

@[simp]

theorem linear_map.to_continuous_linear_map₁_coe {𝕜 : Type u_1} {E : Type u_3} [semi_normed_ring 𝕜] [seminormed_add_comm_group E] [module 𝕜 E] [has_bounded_smul 𝕜 E] (f : 𝕜 →ₗ[𝕜] E) :

↑(f.to_continuous_linear_map₁) = f

@[simp]

theorem linear_map.to_continuous_linear_map₁_apply {𝕜 : Type u_1} {E : Type u_3} [semi_normed_ring 𝕜] [seminormed_add_comm_group E] [module 𝕜 E] [has_bounded_smul 𝕜 E] (f : 𝕜 →ₗ[𝕜] E) (x : 𝕜) :

⇑(f.to_continuous_linear_map₁) x = ⇑f x

theorem continuous_linear_map.uniform_embedding_of_bound {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [ring 𝕜] [ring 𝕜₂] [normed_add_comm_group E] [normed_add_comm_group F] [module 𝕜 E] [module 𝕜₂ F] {σ : 𝕜 →+* 𝕜₂} (f : E →SL[σ] F) {K : nnreal} (hf : ∀ (x : E), ‖x‖ ≤ ↑K * ‖⇑f x‖) :

uniform_embedding ⇑f

Homotheties #

def continuous_linear_map.of_homothety {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [ring 𝕜] [ring 𝕜₂] [seminormed_add_comm_group E] [seminormed_add_comm_group F] [module 𝕜 E] [module 𝕜₂ F] {σ : 𝕜 →+* 𝕜₂} (f : E →ₛₗ[σ] F) (a : ℝ) (hf : ∀ (x : E), ‖⇑f x‖ = a * ‖x‖) :

A (semi-)linear map which is a homothety is a continuous linear map. Since the field 𝕜 need not have ℝ as a subfield, this theorem is not directly deducible from the corresponding theorem about isometries plus a theorem about scalar multiplication. Likewise for the other theorems about homotheties in this file.

Equations

continuous_linear_map.of_homothety f a hf = f.mk_continuous a _

theorem continuous_linear_equiv.homothety_inverse {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [ring 𝕜] [ring 𝕜₂] [seminormed_add_comm_group E] [seminormed_add_comm_group F] [module 𝕜 E] [module 𝕜₂ F] {σ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [ring_hom_inv_pair σ σ₂₁] [ring_hom_inv_pair σ₂₁ σ] (a : ℝ) (ha : 0 < a) (f : E ≃ₛₗ[σ] F) :

(∀ (x : E), ‖⇑f x‖ = a * ‖x‖) → ∀ (y : F), ‖⇑(f.symm) y‖ = a⁻¹ * ‖y‖

noncomputable def continuous_linear_equiv.of_homothety {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [ring 𝕜] [ring 𝕜₂] [seminormed_add_comm_group E] [seminormed_add_comm_group F] [module 𝕜 E] [module 𝕜₂ F] {σ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [ring_hom_inv_pair σ σ₂₁] [ring_hom_inv_pair σ₂₁ σ] (f : E ≃ₛₗ[σ] F) (a : ℝ) (ha : 0 < a) (hf : ∀ (x : E), ‖⇑f x‖ = a * ‖x‖) :

A linear equivalence which is a homothety is a continuous linear equivalence.

Equations

continuous_linear_equiv.of_homothety f a ha hf = f.to_continuous_linear_equiv_of_bounds a a⁻¹ _ _

The span of a single vector #

theorem continuous_linear_map.to_span_singleton_homothety (𝕜 : Type u_1) {E : Type u_3} [normed_division_ring 𝕜] [seminormed_add_comm_group E] [module 𝕜 E] [has_bounded_smul 𝕜 E] (x : E) (c : 𝕜) :

‖⇑(linear_map.to_span_singleton 𝕜 E x) c‖ = ‖x‖ * ‖c‖

theorem continuous_linear_equiv.to_span_nonzero_singleton_homothety (𝕜 : Type u_1) {E : Type u_3} [normed_division_ring 𝕜] [seminormed_add_comm_group E] [module 𝕜 E] [has_bounded_smul 𝕜 E] (x : E) (h : x ≠ 0) (c : 𝕜) :

‖⇑(linear_equiv.to_span_nonzero_singleton 𝕜 E x h) c‖ = ‖x‖ * ‖c‖

noncomputable def continuous_linear_equiv.to_span_nonzero_singleton (𝕜 : Type u_1) {E : Type u_3} [normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] (x : E) (h : x ≠ 0) :

𝕜 ≃L[𝕜] ↥(submodule.span 𝕜 {x})

Given a nonzero element x of a normed space E₁ over a field 𝕜, the natural continuous linear equivalence from E₁ to the span of x.

Equations

continuous_linear_equiv.to_span_nonzero_singleton 𝕜 x h = continuous_linear_equiv.of_homothety (linear_equiv.to_span_nonzero_singleton 𝕜 E x h) ‖x‖ _ _

noncomputable def continuous_linear_equiv.coord (𝕜 : Type u_1) {E : Type u_3} [normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] (x : E) (h : x ≠ 0) :

↥(submodule.span 𝕜 {x}) →L[𝕜] 𝕜

Given a nonzero element x of a normed space E₁ over a field 𝕜, the natural continuous linear map from the span of x to 𝕜.

Equations

continuous_linear_equiv.coord 𝕜 x h = ↑((continuous_linear_equiv.to_span_nonzero_singleton 𝕜 x h).symm)

@[simp]

theorem continuous_linear_equiv.coe_to_span_nonzero_singleton_symm (𝕜 : Type u_1) {E : Type u_3} [normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] {x : E} (h : x ≠ 0) :

⇑((continuous_linear_equiv.to_span_nonzero_singleton 𝕜 x h).symm) = ⇑(continuous_linear_equiv.coord 𝕜 x h)

@[simp]

theorem continuous_linear_equiv.coord_to_span_nonzero_singleton (𝕜 : Type u_1) {E : Type u_3} [normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] {x : E} (h : x ≠ 0) (c : 𝕜) :

⇑(continuous_linear_equiv.coord 𝕜 x h) (⇑(continuous_linear_equiv.to_span_nonzero_singleton 𝕜 x h) c) = c

@[simp]

theorem continuous_linear_equiv.to_span_nonzero_singleton_coord (𝕜 : Type u_1) {E : Type u_3} [normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] {x : E} (h : x ≠ 0) (y : ↥(submodule.span 𝕜 {x})) :

⇑(continuous_linear_equiv.to_span_nonzero_singleton 𝕜 x h) (⇑(continuous_linear_equiv.coord 𝕜 x h) y) = y

@[simp]

theorem continuous_linear_equiv.coord_self (𝕜 : Type u_1) {E : Type u_3} [normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] (x : E) (h : x ≠ 0) :

⇑(continuous_linear_equiv.coord 𝕜 x h) ⟨x, _⟩ = 1