Operator norm on the space of continuous linear maps
Define the operator norm on the space of continuous linear maps between normed spaces, and prove its basic properties. In particular, show that this space is itself a normed space.
theorem
linear_map.lipschitz_of_bound
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(f : E →ₗ[𝕜] F)
(C : ℝ) :
(∀ (x : E), ∥⇑f x∥ ≤ C * ∥x∥) → lipschitz_with (nnreal.of_real C) ⇑f
theorem
linear_map.antilipschitz_of_bound
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(f : E →ₗ[𝕜] F)
{K : nnreal} :
theorem
linear_map.uniform_continuous_of_bound
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(f : E →ₗ[𝕜] F)
(C : ℝ) :
theorem
linear_map.continuous_of_bound
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(f : E →ₗ[𝕜] F)
(C : ℝ) :
def
linear_map.mk_continuous
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(f : E →ₗ[𝕜] F)
(C : ℝ) :
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.to_continuous_linear_map₁
{𝕜 : Type u_1}
{E : Type u_2}
[normed_group E]
[normed_field 𝕜]
[normed_space 𝕜 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∥ _
def
linear_map.mk_continuous_of_exists_bound
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(f : E →ₗ[𝕜] F) :
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 := _}
- _ = _
@[simp]
theorem
linear_map.mk_continuous_coe
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 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}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(f : E →ₗ[𝕜] F)
(C : ℝ)
(h : ∀ (x : E), ∥⇑f x∥ ≤ C * ∥x∥)
(x : E) :
⇑(f.mk_continuous C h) x = ⇑f x
@[simp]
theorem
linear_map.mk_continuous_of_exists_bound_coe
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 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}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(f : E →ₗ[𝕜] F)
(h : ∃ (C : ℝ), ∀ (x : E), ∥⇑f x∥ ≤ C * ∥x∥)
(x : E) :
⇑(f.mk_continuous_of_exists_bound h) x = ⇑f x
@[simp]
theorem
linear_map.to_continuous_linear_map₁_coe
{𝕜 : Type u_1}
{E : Type u_2}
[normed_group E]
[normed_field 𝕜]
[normed_space 𝕜 E]
(f : 𝕜 →ₗ[𝕜] E) :
↑(f.to_continuous_linear_map₁) = f
@[simp]
theorem
linear_map.to_continuous_linear_map₁_apply
{𝕜 : Type u_1}
{E : Type u_2}
[normed_group E]
[normed_field 𝕜]
[normed_space 𝕜 E]
(f : 𝕜 →ₗ[𝕜] E)
(x : 𝕜) :
⇑(f.to_continuous_linear_map₁) x = ⇑f x
theorem
linear_map.continuous_iff_is_closed_ker
{𝕜 : Type u_1}
{E : Type u_2}
[normed_group E]
[normed_field 𝕜]
[normed_space 𝕜 E]
{f : E →ₗ[𝕜] 𝕜} :
theorem
linear_map.bound_of_continuous
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(f : E →ₗ[𝕜] F) :
A continuous linear map between normed spaces is bounded when the field is nondiscrete.
The continuity ensures boundedness on a ball of some radius δ. The nondiscreteness is then
used to rescale any element into an element of norm in [δ/C, δ], whose image has a controlled norm.
The norm control for the original element follows by rescaling.
theorem
continuous_linear_map.bound
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(f : E →L[𝕜] F) :
theorem
continuous_linear_map.is_O_id
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(f : E →L[𝕜] F)
(l : filter E) :
asymptotics.is_O ⇑f (λ (x : E), x) l
theorem
continuous_linear_map.is_O_comp
{𝕜 : Type u_1}
{F : Type u_3}
{G : Type u_4}
[normed_group F]
[normed_group G]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 F]
[normed_space 𝕜 G]
{α : Type u_2}
(g : F →L[𝕜] G)
(f : α → F)
(l : filter α) :
asymptotics.is_O (λ (x' : α), ⇑g (f x')) f l
theorem
continuous_linear_map.is_O_sub
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(f : E →L[𝕜] F)
(l : filter E)
(x : E) :
asymptotics.is_O (λ (x' : E), ⇑f (x' - x)) (λ (x' : E), x' - x) l
def
continuous_linear_map.of_homothety
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(f : E →ₗ[𝕜] F)
(a : ℝ) :
A 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_map.to_span_singleton_homothety
(𝕜 : Type u_1)
{E : Type u_2}
[normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
(x : E)
(c : 𝕜) :
def
continuous_linear_map.to_span_singleton
(𝕜 : Type u_1)
{E : Type u_2}
[normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E] :
Given an element x of a normed space E over a field 𝕜, the natural continuous
linear map from E to the span of x.
Equations
def
continuous_linear_map.op_norm
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F] :
The operator norm of a continuous linear map is the inf of all its bounds.
@[instance]
def
continuous_linear_map.has_op_norm
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F] :
Equations
theorem
continuous_linear_map.norm_def
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(f : E →L[𝕜] F) :
theorem
continuous_linear_map.bounds_nonempty
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
{f : E →L[𝕜] F} :
theorem
continuous_linear_map.bounds_bdd_below
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
{f : E →L[𝕜] F} :
theorem
continuous_linear_map.op_norm_nonneg
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(f : E →L[𝕜] F) :
theorem
continuous_linear_map.le_op_norm
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(f : E →L[𝕜] F)
(x : E) :
The fundamental property of the operator norm: ∥f x∥ ≤ ∥f∥ * ∥x∥.
theorem
continuous_linear_map.le_op_norm_of_le
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(f : E →L[𝕜] F)
{c : ℝ}
{x : E} :
theorem
continuous_linear_map.lipschitz
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(f : E →L[𝕜] F) :
lipschitz_with ⟨∥f∥, _⟩ ⇑f
continuous linear maps are Lipschitz continuous.
theorem
continuous_linear_map.ratio_le_op_norm
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(f : E →L[𝕜] F)
(x : E) :
theorem
continuous_linear_map.unit_le_op_norm
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(f : E →L[𝕜] F)
(x : E) :
The image of the unit ball under a continuous linear map is bounded.
theorem
continuous_linear_map.op_norm_le_bound
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(f : E →L[𝕜] F)
{M : ℝ} :
If one controls the norm of every A x, then one controls the norm of A.
theorem
continuous_linear_map.op_norm_le_of_lipschitz
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
{f : E →L[𝕜] F}
{K : nnreal} :
theorem
continuous_linear_map.op_norm_add_le
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(f g : E →L[𝕜] F) :
The operator norm satisfies the triangle inequality.
theorem
continuous_linear_map.op_norm_zero_iff
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(f : E →L[𝕜] F) :
An operator is zero iff its norm vanishes.
theorem
continuous_linear_map.norm_id_le
{𝕜 : Type u_1}
{E : Type u_2}
[normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E] :
∥continuous_linear_map.id 𝕜 E∥ ≤ 1
The norm of the identity is at most 1. It is in fact 1, except when the space is trivial
where it is 0. It means that one can not do better than an inequality in general.
theorem
continuous_linear_map.norm_id
{𝕜 : Type u_1}
{E : Type u_2}
[normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[nontrivial E] :
∥continuous_linear_map.id 𝕜 E∥ = 1
If a space is non-trivial, then the norm of the identity equals 1.
@[simp]
theorem
continuous_linear_map.norm_id_field
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜] :
∥continuous_linear_map.id 𝕜 𝕜∥ = 1
@[simp]
theorem
continuous_linear_map.op_norm_smul_le
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(c : 𝕜)
(f : E →L[𝕜] F) :
theorem
continuous_linear_map.op_norm_neg
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(f : E →L[𝕜] F) :
@[instance]
def
continuous_linear_map.to_normed_group
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F] :
normed_group (E →L[𝕜] F)
Continuous linear maps themselves form a normed space with respect to the operator norm.
Equations
- continuous_linear_map.to_normed_group = normed_group.of_core (E →L[𝕜] F) continuous_linear_map.to_normed_group._proof_1
@[instance]
def
continuous_linear_map.to_normed_space
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F] :
normed_space 𝕜 (E →L[𝕜] F)
theorem
continuous_linear_map.op_norm_comp_le
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[normed_group E]
[normed_group F]
[normed_group G]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
[normed_space 𝕜 G]
(h : F →L[𝕜] G)
(f : E →L[𝕜] F) :
The operator norm is submultiplicative.
@[instance]
def
continuous_linear_map.to_normed_ring
{𝕜 : Type u_1}
{E : Type u_2}
[normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E] :
normed_ring (E →L[𝕜] E)
Continuous linear maps form a normed ring with respect to the operator norm.
Equations
@[instance]
def
continuous_linear_map.to_normed_algebra
{𝕜 : Type u_1}
{E : Type u_2}
[normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[nontrivial E] :
normed_algebra 𝕜 (E →L[𝕜] E)
For a nonzero normed space E, continuous linear endomorphisms form a normed algebra with
respect to the operator norm.
theorem
continuous_linear_map.uniform_continuous
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(f : E →L[𝕜] F) :
A continuous linear map is automatically uniformly continuous.
theorem
continuous_linear_map.isometry_iff_norm_image_eq_norm
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
{f : E →L[𝕜] F} :
A continuous linear map is an isometry if and only if it preserves the norm.
theorem
continuous_linear_map.homothety_norm
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(hE : 0 < vector_space.dim 𝕜 E)
(f : E →L[𝕜] F)
{a : ℝ} :
theorem
continuous_linear_map.to_span_singleton_norm
{𝕜 : Type u_1}
{E : Type u_2}
[normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
(x : E) :
theorem
continuous_linear_map.uniform_embedding_of_bound
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(f : E →L[𝕜] F)
{K : nnreal} :
theorem
continuous_linear_map.antilipschitz_of_uniform_embedding
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(f : E →L[𝕜] F) :
uniform_embedding ⇑f → (∃ (K : nnreal), antilipschitz_with K ⇑f)
If a continuous linear map is a uniform embedding, then it is expands the distances by a positive factor.
@[instance]
def
continuous_linear_map.complete_space
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
[complete_space F] :
complete_space (E →L[𝕜] F)
If the target space is complete, the space of continuous linear maps with its norm is also complete.
Equations
def
continuous_linear_map.extend
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[normed_group E]
[normed_group F]
[normed_group G]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
[normed_space 𝕜 G]
(f : E →L[𝕜] F)
[complete_space F]
(e : E →L[𝕜] G) :
dense_range ⇑e → uniform_inducing ⇑e → (G →L[𝕜] F)
Extension of a continuous linear map f : E →L[𝕜] F, with E a normed space and F a complete
normed space, along a uniform and dense embedding e : E →L[𝕜] G.
theorem
continuous_linear_map.extend_unique
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[normed_group E]
[normed_group F]
[normed_group G]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
[normed_space 𝕜 G]
(f : E →L[𝕜] F)
[complete_space F]
(e : E →L[𝕜] G)
(h_dense : dense_range ⇑e)
(h_e : uniform_inducing ⇑e)
(g : G →L[𝕜] F) :
@[simp]
theorem
continuous_linear_map.extend_zero
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[normed_group E]
[normed_group F]
[normed_group G]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
[normed_space 𝕜 G]
[complete_space F]
(e : E →L[𝕜] G)
(h_dense : dense_range ⇑e)
(h_e : uniform_inducing ⇑e) :
theorem
continuous_linear_map.op_norm_extend_le
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[normed_group E]
[normed_group F]
[normed_group G]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
[normed_space 𝕜 G]
(f : E →L[𝕜] F)
[complete_space F]
(e : E →L[𝕜] G)
(h_dense : dense_range ⇑e)
{N : nnreal}
(h_e : ∀ (x : E), ∥x∥ ≤ ↑N * ∥⇑e x∥) :
If a dense embedding e : E →L[𝕜] G expands the norm by a constant factor N⁻¹, then the norm
of the extension of f along e is bounded by N * ∥f∥.
theorem
linear_map.mk_continuous_norm_le
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(f : E →ₗ[𝕜] F)
{C : ℝ}
(hC : 0 ≤ C)
(h : ∀ (x : E), ∥⇑f x∥ ≤ C * ∥x∥) :
∥f.mk_continuous C h∥ ≤ C
If a continuous linear map is constructed from a linear map via the constructor mk_continuous,
then its norm is bounded by the bound given to the constructor if it is nonnegative.
@[simp]
theorem
continuous_linear_map.smul_right_norm
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
{c : E →L[𝕜] 𝕜}
{f : F} :
The norm of the tensor product of a scalar linear map and of an element of a normed space is the product of the norms.
def
continuous_linear_map.lmul_left
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
(𝕜' : Type u_5)
[normed_ring 𝕜']
[normed_algebra 𝕜 𝕜'] :
Left-multiplication in a normed algebra, considered as a continuous linear map.
Equations
- continuous_linear_map.lmul_left 𝕜 𝕜' = λ (x : 𝕜'), (algebra.lmul_left 𝕜 𝕜' x).mk_continuous ∥x∥ _
def
continuous_linear_map.lmul_right
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
(𝕜' : Type u_5)
[normed_ring 𝕜']
[normed_algebra 𝕜 𝕜'] :
Right-multiplication in a normed algebra, considered as a continuous linear map.
Equations
- continuous_linear_map.lmul_right 𝕜 𝕜' = λ (x : 𝕜'), (algebra.lmul_right 𝕜 𝕜' x).mk_continuous ∥x∥ _
def
continuous_linear_map.lmul_left_right
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
(𝕜' : Type u_5)
[normed_ring 𝕜']
[normed_algebra 𝕜 𝕜'] :
Simultaneous left- and right-multiplication in a normed algebra, considered as a continuous linear map.
Equations
- continuous_linear_map.lmul_left_right 𝕜 𝕜' vw = (continuous_linear_map.lmul_right 𝕜 𝕜' vw.snd).comp (continuous_linear_map.lmul_left 𝕜 𝕜' vw.fst)
@[simp]
theorem
continuous_linear_map.lmul_left_apply
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
(𝕜' : Type u_5)
[normed_ring 𝕜']
[normed_algebra 𝕜 𝕜']
(x y : 𝕜') :
⇑(continuous_linear_map.lmul_left 𝕜 𝕜' x) y = x * y
@[simp]
theorem
continuous_linear_map.lmul_right_apply
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
(𝕜' : Type u_5)
[normed_ring 𝕜']
[normed_algebra 𝕜 𝕜']
(x y : 𝕜') :
⇑(continuous_linear_map.lmul_right 𝕜 𝕜' x) y = y * x
@[simp]
theorem
continuous_linear_map.lmul_left_right_apply
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
(𝕜' : Type u_5)
[normed_ring 𝕜']
[normed_algebra 𝕜 𝕜']
(vw : 𝕜' × 𝕜')
(x : 𝕜') :
def
continuous_linear_map.restrict_scalars
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
{𝕜' : Type u_5}
[normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{E' : Type u_6}
[normed_group E']
[normed_space 𝕜' E']
{F' : Type u_7}
[normed_group F']
[normed_space 𝕜' F'] :
(E' →L[𝕜'] F') → (semimodule.restrict_scalars 𝕜 𝕜' E' →L[𝕜] semimodule.restrict_scalars 𝕜 𝕜' F')
𝕜-linear continuous function induced by a 𝕜'-linear continuous function when 𝕜' is a
normed algebra over 𝕜.
Equations
- continuous_linear_map.restrict_scalars 𝕜 f = {to_linear_map := {to_fun := (linear_map.restrict_scalars 𝕜 f.to_linear_map).to_fun, map_add' := _, map_smul' := _}, cont := _}
@[simp]
theorem
continuous_linear_map.restrict_scalars_coe_eq_coe
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
{𝕜' : Type u_5}
[normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{E' : Type u_6}
[normed_group E']
[normed_space 𝕜' E']
{F' : Type u_7}
[normed_group F']
[normed_space 𝕜' F']
(f : E' →L[𝕜'] F') :
@[simp]
theorem
continuous_linear_map.restrict_scalars_coe_eq_coe'
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
{𝕜' : Type u_5}
[normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{E' : Type u_6}
[normed_group E']
[normed_space 𝕜' E']
{F' : Type u_7}
[normed_group F']
[normed_space 𝕜' F']
(f : E' →L[𝕜'] F') :
@[instance]
def
continuous_linear_map.has_scalar_extend_scalars
{𝕜 : Type u_1}
{E : Type u_2}
[normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
{𝕜' : Type u_5}
[normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{F' : Type u_6}
[normed_group F']
[normed_space 𝕜' F'] :
has_scalar 𝕜' (E →L[𝕜] semimodule.restrict_scalars 𝕜 𝕜' F')
Equations
- continuous_linear_map.has_scalar_extend_scalars = {smul := λ (c : 𝕜') (f : E →L[𝕜] semimodule.restrict_scalars 𝕜 𝕜' F'), (c • f.to_linear_map).mk_continuous (∥c∥ * ∥f∥) _}
@[instance]
def
continuous_linear_map.module_extend_scalars
{𝕜 : Type u_1}
{E : Type u_2}
[normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
{𝕜' : Type u_5}
[normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{F' : Type u_6}
[normed_group F']
[normed_space 𝕜' F'] :
module 𝕜' (E →L[𝕜] semimodule.restrict_scalars 𝕜 𝕜' F')
Equations
- continuous_linear_map.module_extend_scalars = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := continuous_linear_map.has_scalar_extend_scalars _inst_11, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
@[instance]
def
continuous_linear_map.normed_space_extend_scalars
{𝕜 : Type u_1}
{E : Type u_2}
[normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
{𝕜' : Type u_5}
[normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{F' : Type u_6}
[normed_group F']
[normed_space 𝕜' F'] :
normed_space 𝕜' (E →L[𝕜] semimodule.restrict_scalars 𝕜 𝕜' F')
Equations
def
continuous_linear_map.smul_algebra_right
{𝕜 : Type u_1}
{E : Type u_2}
[normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
{𝕜' : Type u_5}
[normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{F' : Type u_6}
[normed_group F']
[normed_space 𝕜' F'] :
(E →L[𝕜] 𝕜') → semimodule.restrict_scalars 𝕜 𝕜' F' → (E →L[𝕜] semimodule.restrict_scalars 𝕜 𝕜' F')
When f is a continuous linear map taking values in S, then λb, f b • x is a
continuous linear map.
Equations
- f.smul_algebra_right x = {to_linear_map := {to_fun := (smul_algebra_right f.to_linear_map x).to_fun, map_add' := _, map_smul' := _}, cont := _}
@[simp]
theorem
continuous_linear_map.smul_algebra_right_apply
{𝕜 : Type u_1}
{E : Type u_2}
[normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
{𝕜' : Type u_5}
[normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{F' : Type u_6}
[normed_group F']
[normed_space 𝕜' F']
(f : E →L[𝕜] 𝕜')
(x : semimodule.restrict_scalars 𝕜 𝕜' F')
(c : E) :
⇑(f.smul_algebra_right x) c = ⇑f c • x
theorem
continuous_linear_map.has_sum
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
{ι : Type u_5}
{f : ι → E}
(φ : E →L[𝕜] F)
{x : E} :
Applying a continuous linear map commutes with taking an (infinite) sum.
theorem
continuous_linear_map.has_sum_of_summable
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
{ι : Type u_5}
{f : ι → E}
(φ : E →L[𝕜] F) :
theorem
continuous_linear_equiv.lipschitz
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(e : E ≃L[𝕜] F) :
lipschitz_with (nnnorm ↑e) ⇑e
theorem
continuous_linear_equiv.antilipschitz
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(e : E ≃L[𝕜] F) :
antilipschitz_with (nnnorm ↑(e.symm)) ⇑e
theorem
continuous_linear_equiv.is_O_comp
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(e : E ≃L[𝕜] F)
{α : Type u_4}
(f : α → E)
(l : filter α) :
asymptotics.is_O (λ (x' : α), ⇑e (f x')) f l
theorem
continuous_linear_equiv.is_O_sub
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(e : E ≃L[𝕜] F)
(l : filter E)
(x : E) :
asymptotics.is_O (λ (x' : E), ⇑e (x' - x)) (λ (x' : E), x' - x) l
theorem
continuous_linear_equiv.is_O_comp_rev
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(e : E ≃L[𝕜] F)
{α : Type u_4}
(f : α → E)
(l : filter α) :
asymptotics.is_O f (λ (x' : α), ⇑e (f x')) l
theorem
continuous_linear_equiv.is_O_sub_rev
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(e : E ≃L[𝕜] F)
(l : filter E)
(x : E) :
asymptotics.is_O (λ (x' : E), x' - x) (λ (x' : E), ⇑e (x' - x)) l
theorem
continuous_linear_equiv.uniform_embedding
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(e : E ≃L[𝕜] F) :
A continuous linear equiv is a uniform embedding.
theorem
continuous_linear_equiv.one_le_norm_mul_norm_symm
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(e : E ≃L[𝕜] F)
[nontrivial E] :
theorem
continuous_linear_equiv.norm_pos
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(e : E ≃L[𝕜] F)
[nontrivial E] :
theorem
continuous_linear_equiv.norm_symm_pos
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(e : E ≃L[𝕜] F)
[nontrivial E] :
theorem
continuous_linear_equiv.subsingleton_or_norm_symm_pos
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(e : E ≃L[𝕜] F) :
theorem
continuous_linear_equiv.subsingleton_or_nnnorm_symm_pos
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(e : E ≃L[𝕜] F) :
theorem
continuous_linear_equiv.homothety_inverse
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(a : ℝ)
(ha : 0 < a)
(f : E ≃ₗ[𝕜] F)
(a_1 : ∀ (x : E), ∥⇑f x∥ = a * ∥x∥)
(y : F) :
def
continuous_linear_equiv.of_homothety
(𝕜 : Type u_1)
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(f : E ≃ₗ[𝕜] F)
(a : ℝ) :
A linear equivalence which is a homothety is a continuous linear equivalence.
Equations
- continuous_linear_equiv.of_homothety 𝕜 f a ha hf = {to_linear_equiv := f, continuous_to_fun := _, continuous_inv_fun := _}
theorem
continuous_linear_equiv.to_span_nonzero_singleton_homothety
(𝕜 : Type u_1)
{E : Type u_2}
[normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
(x : E)
(h : x ≠ 0)
(c : 𝕜) :
def
continuous_linear_equiv.to_span_nonzero_singleton
(𝕜 : Type u_1)
{E : Type u_2}
[normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
(x : E) :
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
def
continuous_linear_equiv.coord
(𝕜 : Type u_1)
{E : Type u_2}
[normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
(x : E) :
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 𝕜.
theorem
continuous_linear_equiv.coord_norm
(𝕜 : Type u_1)
{E : Type u_2}
[normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
(x : E)
(h : x ≠ 0) :
theorem
continuous_linear_equiv.coord_self
(𝕜 : Type u_1)
{E : Type u_2}
[normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
(x : E)
(h : x ≠ 0) :
⇑(continuous_linear_equiv.coord 𝕜 x h) ⟨x, _⟩ = 1
@[instance]
def
continuous_linear_equiv.automorphism_group
(𝕜 : Type u_1)
(E : Type u_2)
[normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E] :
The continuous linear equivalences from E to itself form a group under composition.
Equations
- continuous_linear_equiv.automorphism_group 𝕜 E = {mul := λ (f g : E ≃L[𝕜] E), g.trans f, mul_assoc := _, one := continuous_linear_equiv.refl 𝕜 E normed_space.to_semimodule, one_mul := _, mul_one := _, inv := λ (f : E ≃L[𝕜] E), f.symm, mul_left_inv := _}
def
continuous_linear_equiv.of_unit
{𝕜 : Type u_1}
{E : Type u_2}
[normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E] :
An invertible continuous linear map f determines a continuous equivalence from E to itself.
Equations
- continuous_linear_equiv.of_unit f = {to_linear_equiv := {to_fun := ⇑(f.val), map_add' := _, map_smul' := _, inv_fun := ⇑(f.inv), left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
def
continuous_linear_equiv.to_unit
{𝕜 : Type u_1}
{E : Type u_2}
[normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E] :
A continuous equivalence from E to itself determines an invertible continuous linear map.
def
continuous_linear_equiv.units_equiv
(𝕜 : Type u_1)
(E : Type u_2)
[normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E] :
The units of the algebra of continuous 𝕜-linear endomorphisms of E is multiplicatively
equivalent to the type of continuous linear equivalences between E and itself.
Equations
- continuous_linear_equiv.units_equiv 𝕜 E = {to_fun := continuous_linear_equiv.of_unit _inst_5, inv_fun := continuous_linear_equiv.to_unit _inst_5, left_inv := _, right_inv := _, map_mul' := _}
@[simp]
theorem
continuous_linear_equiv.units_equiv_to_continuous_linear_map
(𝕜 : Type u_1)
(E : Type u_2)
[normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
(f : units (E →L[𝕜] E)) :
↑(⇑(continuous_linear_equiv.units_equiv 𝕜 E) f) = ↑f
theorem
linear_equiv.uniform_embedding
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 F]
(e : E ≃ₗ[𝕜] F) :
continuous ⇑e → continuous ⇑(e.symm) → uniform_embedding ⇑e
@[simp]
theorem
continuous_linear_map.lmul_left_norm
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
(𝕜' : Type u_5)
[normed_ring 𝕜']
[normed_algebra 𝕜 𝕜']
(v : 𝕜') :
@[simp]
theorem
continuous_linear_map.lmul_right_norm
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
(𝕜' : Type u_5)
[normed_ring 𝕜']
[normed_algebra 𝕜 𝕜']
(v : 𝕜') :
theorem
continuous_linear_map.lmul_left_right_norm_le
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
(𝕜' : Type u_5)
[normed_ring 𝕜']
[normed_algebra 𝕜 𝕜']
(vw : 𝕜' × 𝕜') :