Operator norm on the space of continuous linear maps #
Define the operator norm on the space of continuous (semi)linear maps between normed spaces, and prove its basic properties. In particular, show that this space is itself a normed space.
Since a lot of elementary properties don't require ∥x∥ = 0 → x = 0 we start setting up the
theory for semi_normed_group and we specialize to normed_group at the end.
Note that most of statements that apply to semilinear maps only hold when the ring homomorphism
is isometric, as expressed by the typeclass [ring_hom_isometric σ].
Most statements in this file require the field to be non-discrete,
as this is necessary to deduce an inequality ∥f x∥ ≤ C ∥x∥ from the continuity of f.
However, the other direction always holds.
In this section, we just assume that 𝕜 is a normed field.
In the remainder of the file, it will be non-discrete.
def
linear_map.mk_continuous
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[normed_field 𝕜]
[normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ 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.to_continuous_linear_map₁
{𝕜 : Type u_1}
{E : Type u_4}
[semi_normed_group E]
[normed_field 𝕜]
[normed_space 𝕜 E]
(f : 𝕜 →ₗ[𝕜] 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}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[normed_field 𝕜]
[normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ 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_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[normed_field 𝕜]
[normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ 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_4}
{G : Type u_8}
[semi_normed_group E]
[semi_normed_group G]
[normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 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_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[normed_field 𝕜]
[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}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[normed_field 𝕜]
[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, norm_cast]
theorem
linear_map.mk_continuous_of_exists_bound_coe
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[normed_field 𝕜]
[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}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[normed_field 𝕜]
[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_4}
[semi_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_4}
[semi_normed_group E]
[normed_field 𝕜]
[normed_space 𝕜 E]
(f : 𝕜 →ₗ[𝕜] E)
(x : 𝕜) :
⇑(f.to_continuous_linear_map₁) x = ⇑f x
theorem
norm_image_of_norm_zero
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
{𝓕 : Type u_10}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[semilinear_map_class 𝓕 σ₁₂ E F]
(f : 𝓕)
(hf : continuous ⇑f)
{x : E}
(hx : ∥x∥ = 0) :
If ∥x∥ = 0 and f is continuous then ∥f x∥ = 0.
theorem
semilinear_map_class.bound_of_shell_semi_normed
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
{𝓕 : Type u_10}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
[semilinear_map_class 𝓕 σ₁₂ E F]
(f : 𝓕)
{ε C : ℝ}
(ε_pos : 0 < ε)
{c : 𝕜}
(hc : 1 < ∥c∥)
(hf : ∀ (x : E), ε / ∥c∥ ≤ ∥x∥ → ∥x∥ < ε → ∥⇑f x∥ ≤ C * ∥x∥)
{x : E}
(hx : ∥x∥ ≠ 0) :
theorem
semilinear_map_class.bound_of_continuous
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
{𝓕 : Type u_10}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
[semilinear_map_class 𝓕 σ₁₂ E F]
(f : 𝓕)
(hf : continuous ⇑f) :
A continuous linear map between seminormed 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}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
(f : E →SL[σ₁₂] F) :
def
continuous_linear_map.of_homothety
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
(f : E →ₛₗ[σ₁₂] F)
(a : ℝ)
(hf : ∀ (x : E), ∥⇑f x∥ = a * ∥x∥) :
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_4}
[semi_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_4}
[semi_normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
(x : E) :
Given an element x of a normed space E over a field 𝕜, the natural continuous
linear map from 𝕜 to E by taking multiples of x.
Equations
theorem
continuous_linear_map.to_span_singleton_apply
(𝕜 : Type u_1)
{E : Type u_4}
[semi_normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
(x : E)
(r : 𝕜) :
⇑(continuous_linear_map.to_span_singleton 𝕜 x) r = r • x
theorem
continuous_linear_map.to_span_singleton_add
(𝕜 : Type u_1)
{E : Type u_4}
[semi_normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
(x y : E) :
theorem
continuous_linear_map.to_span_singleton_smul'
(𝕜 : Type u_1)
{E : Type u_4}
[semi_normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
(𝕜' : Type u_2)
[normed_field 𝕜']
[normed_space 𝕜' E]
[smul_comm_class 𝕜 𝕜' E]
(c : 𝕜')
(x : E) :
theorem
continuous_linear_map.to_span_singleton_smul
(𝕜 : Type u_1)
{E : Type u_4}
[semi_normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
(c : 𝕜)
(x : E) :
def
linear_isometry.to_span_singleton
(𝕜 : Type u_1)
(E : Type u_4)
[semi_normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
{v : E}
(hv : ∥v∥ = 1) :
Given a unit-length element x of a normed space E over a field 𝕜, the natural linear
isometry map from 𝕜 to E by taking multiples of x.
Equations
- linear_isometry.to_span_singleton 𝕜 E hv = {to_linear_map := {to_fun := (linear_map.to_span_singleton 𝕜 E v).to_fun, map_add' := _, map_smul' := _}, norm_map' := _}
@[simp]
theorem
linear_isometry.to_span_singleton_apply
{𝕜 : Type u_1}
{E : Type u_4}
[semi_normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
{v : E}
(hv : ∥v∥ = 1)
(a : 𝕜) :
⇑(linear_isometry.to_span_singleton 𝕜 E hv) a = a • v
@[simp]
theorem
linear_isometry.coe_to_span_singleton
{𝕜 : Type u_1}
{E : Type u_4}
[semi_normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
{v : E}
(hv : ∥v∥ = 1) :
noncomputable
def
continuous_linear_map.op_norm
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
(f : E →SL[σ₁₂] F) :
The operator norm of a continuous linear map is the inf of all its bounds.
@[protected, instance]
noncomputable
def
continuous_linear_map.has_op_norm
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂} :
Equations
theorem
continuous_linear_map.norm_def
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
(f : E →SL[σ₁₂] F) :
theorem
continuous_linear_map.bounds_nonempty
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
{f : E →SL[σ₁₂] F} :
theorem
continuous_linear_map.bounds_bdd_below
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{f : E →SL[σ₁₂] F} :
theorem
continuous_linear_map.op_norm_le_bound
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
(f : E →SL[σ₁₂] F)
{M : ℝ}
(hMp : 0 ≤ M)
(hM : ∀ (x : E), ∥⇑f x∥ ≤ M * ∥x∥) :
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}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{f : E →SL[σ₁₂] F}
{K : nnreal}
(hf : lipschitz_with K ⇑f) :
theorem
continuous_linear_map.op_norm_eq_of_bounds
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{φ : E →SL[σ₁₂] F}
{M : ℝ}
(M_nonneg : 0 ≤ M)
(h_above : ∀ (x : E), ∥⇑φ x∥ ≤ M * ∥x∥)
(h_below : ∀ (N : ℝ), N ≥ 0 → (∀ (x : E), ∥⇑φ x∥ ≤ N * ∥x∥) → M ≤ N) :
theorem
continuous_linear_map.op_norm_neg
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
(f : E →SL[σ₁₂] F) :
theorem
continuous_linear_map.antilipschitz_of_bound
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
(f : E →SL[σ₁₂] F)
{K : nnreal}
(h : ∀ (x : E), ∥x∥ ≤ ↑K * ∥⇑f x∥) :
theorem
continuous_linear_map.bound_of_antilipschitz
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
(f : E →SL[σ₁₂] F)
{K : nnreal}
(h : antilipschitz_with K ⇑f)
(x : E) :
theorem
continuous_linear_map.op_norm_nonneg
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
(f : E →SL[σ₁₂] F) :
theorem
continuous_linear_map.le_op_norm
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
(f : E →SL[σ₁₂] F)
(x : E) :
The fundamental property of the operator norm: ∥f x∥ ≤ ∥f∥ * ∥x∥.
theorem
continuous_linear_map.dist_le_op_norm
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
(f : E →SL[σ₁₂] F)
(x y : E) :
has_dist.dist (⇑f x) (⇑f y) ≤ ∥f∥ * has_dist.dist x y
theorem
continuous_linear_map.le_op_norm_of_le
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
(f : E →SL[σ₁₂] F)
{c : ℝ}
{x : E}
(h : ∥x∥ ≤ c) :
theorem
continuous_linear_map.le_of_op_norm_le
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
(f : E →SL[σ₁₂] F)
{c : ℝ}
(h : ∥f∥ ≤ c)
(x : E) :
theorem
continuous_linear_map.ratio_le_op_norm
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
(f : E →SL[σ₁₂] F)
(x : E) :
theorem
continuous_linear_map.unit_le_op_norm
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
(f : E →SL[σ₁₂] F)
(x : E) :
The image of the unit ball under a continuous linear map is bounded.
theorem
continuous_linear_map.op_norm_le_of_shell
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
{f : E →SL[σ₁₂] F}
{ε C : ℝ}
(ε_pos : 0 < ε)
(hC : 0 ≤ C)
{c : 𝕜}
(hc : 1 < ∥c∥)
(hf : ∀ (x : E), ε / ∥c∥ ≤ ∥x∥ → ∥x∥ < ε → ∥⇑f x∥ ≤ C * ∥x∥) :
theorem
continuous_linear_map.op_norm_le_of_ball
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
{f : E →SL[σ₁₂] F}
{ε C : ℝ}
(ε_pos : 0 < ε)
(hC : 0 ≤ C)
(hf : ∀ (x : E), x ∈ metric.ball 0 ε → ∥⇑f x∥ ≤ C * ∥x∥) :
theorem
continuous_linear_map.op_norm_le_of_nhds_zero
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
{f : E →SL[σ₁₂] F}
{C : ℝ}
(hC : 0 ≤ C)
(hf : ∀ᶠ (x : E) in nhds 0, ∥⇑f x∥ ≤ C * ∥x∥) :
theorem
continuous_linear_map.op_norm_le_of_shell'
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
{f : E →SL[σ₁₂] F}
{ε C : ℝ}
(ε_pos : 0 < ε)
(hC : 0 ≤ C)
{c : 𝕜}
(hc : ∥c∥ < 1)
(hf : ∀ (x : E), ε * ∥c∥ ≤ ∥x∥ → ∥x∥ < ε → ∥⇑f x∥ ≤ C * ∥x∥) :
theorem
continuous_linear_map.op_norm_add_le
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
(f g : E →SL[σ₁₂] F) :
The operator norm satisfies the triangle inequality.
theorem
continuous_linear_map.op_norm_zero
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂] :
The norm of the 0 operator is 0.
theorem
continuous_linear_map.norm_id_le
{𝕜 : Type u_1}
{E : Type u_4}
[semi_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_of_nontrivial_seminorm
{𝕜 : Type u_1}
{E : Type u_4}
[semi_normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
(h : ∃ (x : E), ∥x∥ ≠ 0) :
∥continuous_linear_map.id 𝕜 E∥ = 1
If there is an element with norm different from 0, then the norm of the identity equals 1.
(Since we are working with seminorms supposing that the space is non-trivial is not enough.)
theorem
continuous_linear_map.op_norm_smul_le
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
{𝕜' : Type u_3}
[normed_field 𝕜']
[normed_space 𝕜' F]
[smul_comm_class 𝕜₂ 𝕜' F]
(c : 𝕜')
(f : E →SL[σ₁₂] F) :
@[protected, instance]
noncomputable
def
continuous_linear_map.to_semi_normed_group
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂] :
semi_normed_group (E →SL[σ₁₂] F)
Continuous linear maps themselves form a seminormed space with respect to the operator norm.
Equations
- continuous_linear_map.to_semi_normed_group = semi_normed_group.of_core (E →SL[σ₁₂] F) continuous_linear_map.to_semi_normed_group._proof_1
theorem
continuous_linear_map.nnnorm_def
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
(f : E →SL[σ₁₂] F) :
theorem
continuous_linear_map.op_nnnorm_le_bound
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
(f : E →SL[σ₁₂] F)
(M : nnreal)
(hM : ∀ (x : E), ∥⇑f x∥₊ ≤ M * ∥x∥₊) :
If one controls the norm of every A x, then one controls the norm of A.
theorem
continuous_linear_map.op_nnnorm_le_of_lipschitz
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
{f : E →SL[σ₁₂] F}
{K : nnreal}
(hf : lipschitz_with K ⇑f) :
theorem
continuous_linear_map.op_nnnorm_eq_of_bounds
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
{φ : E →SL[σ₁₂] F}
(M : nnreal)
(h_above : ∀ (x : E), ∥⇑φ x∥ ≤ ↑M * ∥x∥)
(h_below : ∀ (N : nnreal), (∀ (x : E), ∥⇑φ x∥₊ ≤ N * ∥x∥₊) → M ≤ N) :
@[protected, instance]
def
continuous_linear_map.to_normed_space
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
{𝕜' : Type u_3}
[normed_field 𝕜']
[normed_space 𝕜' F]
[smul_comm_class 𝕜₂ 𝕜' F] :
normed_space 𝕜' (E →SL[σ₁₂] F)
Equations
- continuous_linear_map.to_normed_space = {to_module := continuous_linear_map.module continuous_linear_map.to_normed_space._proof_2, norm_smul_le := _}
theorem
continuous_linear_map.op_norm_comp_le
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[semi_normed_group E]
[semi_normed_group F]
[semi_normed_group G]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[nondiscrete_normed_field 𝕜₃]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[normed_space 𝕜₃ G]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[ring_hom_isometric σ₁₂]
[ring_hom_isometric σ₂₃]
(h : F →SL[σ₂₃] G)
(f : E →SL[σ₁₂] F) :
The operator norm is submultiplicative.
theorem
continuous_linear_map.op_nnnorm_comp_le
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[semi_normed_group E]
[semi_normed_group F]
[semi_normed_group G]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[nondiscrete_normed_field 𝕜₃]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[normed_space 𝕜₃ G]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[ring_hom_isometric σ₁₂]
[ring_hom_isometric σ₂₃]
(h : F →SL[σ₂₃] G)
[ring_hom_isometric σ₁₃]
(f : E →SL[σ₁₂] F) :
@[protected, instance]
noncomputable
def
continuous_linear_map.to_semi_normed_ring
{𝕜 : Type u_1}
{E : Type u_4}
[semi_normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E] :
semi_normed_ring (E →L[𝕜] E)
Continuous linear maps form a seminormed ring with respect to the operator norm.
Equations
- continuous_linear_map.to_semi_normed_ring = {to_has_norm := semi_normed_group.to_has_norm continuous_linear_map.to_semi_normed_group, to_ring := {add := add_comm_group.add semi_normed_group.to_add_comm_group, add_assoc := _, zero := add_comm_group.zero semi_normed_group.to_add_comm_group, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul semi_normed_group.to_add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg semi_normed_group.to_add_comm_group, sub := add_comm_group.sub semi_normed_group.to_add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul semi_normed_group.to_add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast continuous_linear_map.ring, nat_cast := ring.nat_cast continuous_linear_map.ring, one := ring.one continuous_linear_map.ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul continuous_linear_map.ring, mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow continuous_linear_map.ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}, to_pseudo_metric_space := semi_normed_group.to_pseudo_metric_space continuous_linear_map.to_semi_normed_group, dist_eq := _, norm_mul := _}
@[protected, instance]
noncomputable
def
continuous_linear_map.to_normed_algebra
{𝕜 : Type u_1}
{E : Type u_4}
[semi_normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E] :
normed_algebra 𝕜 (E →L[𝕜] E)
For a normed space E, continuous linear endomorphisms form a normed algebra with
respect to the operator norm.
theorem
continuous_linear_map.le_op_nnnorm
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
(f : E →SL[σ₁₂] F)
(x : E) :
theorem
continuous_linear_map.nndist_le_op_nnnorm
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
(f : E →SL[σ₁₂] F)
(x y : E) :
has_nndist.nndist (⇑f x) (⇑f y) ≤ ∥f∥₊ * has_nndist.nndist x y
theorem
continuous_linear_map.lipschitz
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
(f : E →SL[σ₁₂] F) :
continuous linear maps are Lipschitz continuous.
theorem
continuous_linear_map.lipschitz_apply
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
(x : E) :
Evaluation of a continuous linear map f at a point is Lipschitz continuous in f.
theorem
continuous_linear_map.op_norm_ext
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[semi_normed_group E]
[semi_normed_group F]
[semi_normed_group G]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[nondiscrete_normed_field 𝕜₃]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[normed_space 𝕜₃ G]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[ring_hom_isometric σ₁₃]
(f : E →SL[σ₁₂] F)
(g : E →SL[σ₁₃] G)
(h : ∀ (x : E), ∥⇑f x∥ = ∥⇑g x∥) :
theorem
continuous_linear_map.op_norm_le_bound₂
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[semi_normed_group E]
[semi_normed_group F]
[semi_normed_group G]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[nondiscrete_normed_field 𝕜₃]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[normed_space 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[ring_hom_isometric σ₂₃]
(f : E →SL[σ₁₃] F →SL[σ₂₃] G)
{C : ℝ}
(h0 : 0 ≤ C)
(hC : ∀ (x : E) (y : F), ∥⇑(⇑f x) y∥ ≤ C * ∥x∥ * ∥y∥) :
theorem
continuous_linear_map.le_op_norm₂
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[semi_normed_group E]
[semi_normed_group F]
[semi_normed_group G]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[nondiscrete_normed_field 𝕜₃]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[normed_space 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[ring_hom_isometric σ₂₃]
[ring_hom_isometric σ₁₃]
(f : E →SL[σ₁₃] F →SL[σ₂₃] G)
(x : E)
(y : F) :
@[simp]
theorem
continuous_linear_map.op_norm_prod
{𝕜 : Type u_1}
{E : Type u_4}
{Fₗ : Type u_7}
{Gₗ : Type u_9}
[semi_normed_group E]
[semi_normed_group Fₗ]
[semi_normed_group Gₗ]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ]
[normed_space 𝕜 Gₗ]
(f : E →L[𝕜] Fₗ)
(g : E →L[𝕜] Gₗ) :
@[simp]
theorem
continuous_linear_map.op_nnnorm_prod
{𝕜 : Type u_1}
{E : Type u_4}
{Fₗ : Type u_7}
{Gₗ : Type u_9}
[semi_normed_group E]
[semi_normed_group Fₗ]
[semi_normed_group Gₗ]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ]
[normed_space 𝕜 Gₗ]
(f : E →L[𝕜] Fₗ)
(g : E →L[𝕜] Gₗ) :
def
continuous_linear_map.prodₗᵢ
{𝕜 : Type u_1}
{E : Type u_4}
{Fₗ : Type u_7}
{Gₗ : Type u_9}
[semi_normed_group E]
[semi_normed_group Fₗ]
[semi_normed_group Gₗ]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ]
[normed_space 𝕜 Gₗ]
(R : Type u_2)
[semiring R]
[module R Fₗ]
[module R Gₗ]
[has_continuous_const_smul R Fₗ]
[has_continuous_const_smul R Gₗ]
[smul_comm_class 𝕜 R Fₗ]
[smul_comm_class 𝕜 R Gₗ] :
continuous_linear_map.prod as a linear_isometry_equiv.
Equations
- continuous_linear_map.prodₗᵢ R = {to_linear_equiv := continuous_linear_map.prodₗ R continuous_linear_map.prodₗᵢ._proof_22, norm_map' := _}
@[simp]
theorem
continuous_linear_map.op_norm_subsingleton
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
(f : E →SL[σ₁₂] F)
[subsingleton E] :
theorem
continuous_linear_map.is_O_with_id
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
(f : E →SL[σ₁₂] F)
(l : filter E) :
asymptotics.is_O_with ∥f∥ l ⇑f (λ (x : E), x)
theorem
continuous_linear_map.is_O_id
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
(f : E →SL[σ₁₂] F)
(l : filter E) :
theorem
continuous_linear_map.is_O_with_comp
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{F : Type u_6}
{G : Type u_8}
[semi_normed_group F]
[semi_normed_group G]
[nondiscrete_normed_field 𝕜₂]
[nondiscrete_normed_field 𝕜₃]
[normed_space 𝕜₂ F]
[normed_space 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
[ring_hom_isometric σ₂₃]
{α : Type u_1}
(g : F →SL[σ₂₃] G)
(f : α → F)
(l : filter α) :
asymptotics.is_O_with ∥g∥ l (λ (x' : α), ⇑g (f x')) f
theorem
continuous_linear_map.is_O_comp
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{F : Type u_6}
{G : Type u_8}
[semi_normed_group F]
[semi_normed_group G]
[nondiscrete_normed_field 𝕜₂]
[nondiscrete_normed_field 𝕜₃]
[normed_space 𝕜₂ F]
[normed_space 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
[ring_hom_isometric σ₂₃]
{α : Type u_1}
(g : F →SL[σ₂₃] G)
(f : α → F)
(l : filter α) :
theorem
continuous_linear_map.is_O_with_sub
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
(f : E →SL[σ₁₂] F)
(l : filter E)
(x : E) :
theorem
continuous_linear_map.is_O_sub
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
(f : E →SL[σ₁₂] F)
(l : filter E)
(x : E) :
theorem
linear_isometry.norm_to_continuous_linear_map_le
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
(f : E →ₛₗᵢ[σ₁₂] F) :
theorem
linear_map.mk_continuous_norm_le
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[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.
theorem
linear_map.mk_continuous_norm_le'
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
(f : E →ₛₗ[σ₁₂] F)
{C : ℝ}
(h : ∀ (x : E), ∥⇑f x∥ ≤ C * ∥x∥) :
∥f.mk_continuous C h∥ ≤ linear_order.max C 0
If a continuous linear map is constructed from a linear map via the constructor mk_continuous,
then its norm is bounded by the bound or zero if bound is negative.
noncomputable
def
linear_map.mk_continuous₂
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[semi_normed_group E]
[semi_normed_group F]
[semi_normed_group G]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[nondiscrete_normed_field 𝕜₃]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[normed_space 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[ring_hom_isometric σ₂₃]
(f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G)
(C : ℝ)
(hC : ∀ (x : E) (y : F), ∥⇑(⇑f x) y∥ ≤ C * ∥x∥ * ∥y∥) :
Create a bilinear map (represented as a map E →L[𝕜] F →L[𝕜] G) from the corresponding linear
map and a bound on the norm of the image. The linear map can be constructed using
linear_map.mk₂.
Equations
- f.mk_continuous₂ C hC = {to_fun := λ (x : E), (⇑f x).mk_continuous (C * ∥x∥) _, map_add' := _, map_smul' := _}.mk_continuous (linear_order.max C 0) _
@[simp]
theorem
linear_map.mk_continuous₂_apply
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[semi_normed_group E]
[semi_normed_group F]
[semi_normed_group G]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[nondiscrete_normed_field 𝕜₃]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[normed_space 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[ring_hom_isometric σ₂₃]
(f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G)
{C : ℝ}
(hC : ∀ (x : E) (y : F), ∥⇑(⇑f x) y∥ ≤ C * ∥x∥ * ∥y∥)
(x : E)
(y : F) :
theorem
linear_map.mk_continuous₂_norm_le'
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[semi_normed_group E]
[semi_normed_group F]
[semi_normed_group G]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[nondiscrete_normed_field 𝕜₃]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[normed_space 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[ring_hom_isometric σ₂₃]
(f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G)
{C : ℝ}
(hC : ∀ (x : E) (y : F), ∥⇑(⇑f x) y∥ ≤ C * ∥x∥ * ∥y∥) :
∥f.mk_continuous₂ C hC∥ ≤ linear_order.max C 0
theorem
linear_map.mk_continuous₂_norm_le
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[semi_normed_group E]
[semi_normed_group F]
[semi_normed_group G]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[nondiscrete_normed_field 𝕜₃]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[normed_space 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[ring_hom_isometric σ₂₃]
(f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G)
{C : ℝ}
(h0 : 0 ≤ C)
(hC : ∀ (x : E) (y : F), ∥⇑(⇑f x) y∥ ≤ C * ∥x∥ * ∥y∥) :
∥f.mk_continuous₂ C hC∥ ≤ C
noncomputable
def
continuous_linear_map.flip
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[semi_normed_group E]
[semi_normed_group F]
[semi_normed_group G]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[nondiscrete_normed_field 𝕜₃]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[normed_space 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[ring_hom_isometric σ₂₃]
[ring_hom_isometric σ₁₃]
(f : E →SL[σ₁₃] F →SL[σ₂₃] G) :
Flip the order of arguments of a continuous bilinear map.
For a version bundled as linear_isometry_equiv, see
continuous_linear_map.flipL.
Equations
- f.flip = (linear_map.mk₂'ₛₗ σ₂₃ σ₁₃ (λ (y : F) (x : E), ⇑(⇑f x) y) _ _ _ _).mk_continuous₂ ∥f∥ _
@[simp]
theorem
continuous_linear_map.flip_apply
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[semi_normed_group E]
[semi_normed_group F]
[semi_normed_group G]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[nondiscrete_normed_field 𝕜₃]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[normed_space 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[ring_hom_isometric σ₂₃]
[ring_hom_isometric σ₁₃]
(f : E →SL[σ₁₃] F →SL[σ₂₃] G)
(x : E)
(y : F) :
@[simp]
theorem
continuous_linear_map.flip_flip
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[semi_normed_group E]
[semi_normed_group F]
[semi_normed_group G]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[nondiscrete_normed_field 𝕜₃]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[normed_space 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[ring_hom_isometric σ₂₃]
[ring_hom_isometric σ₁₃]
(f : E →SL[σ₁₃] F →SL[σ₂₃] G) :
@[simp]
theorem
continuous_linear_map.op_norm_flip
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[semi_normed_group E]
[semi_normed_group F]
[semi_normed_group G]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[nondiscrete_normed_field 𝕜₃]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[normed_space 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[ring_hom_isometric σ₂₃]
[ring_hom_isometric σ₁₃]
(f : E →SL[σ₁₃] F →SL[σ₂₃] G) :
@[simp]
theorem
continuous_linear_map.flip_add
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[semi_normed_group E]
[semi_normed_group F]
[semi_normed_group G]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[nondiscrete_normed_field 𝕜₃]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[normed_space 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[ring_hom_isometric σ₂₃]
[ring_hom_isometric σ₁₃]
(f g : E →SL[σ₁₃] F →SL[σ₂₃] G) :
@[simp]
theorem
continuous_linear_map.flip_smul
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[semi_normed_group E]
[semi_normed_group F]
[semi_normed_group G]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[nondiscrete_normed_field 𝕜₃]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[normed_space 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[ring_hom_isometric σ₂₃]
[ring_hom_isometric σ₁₃]
(c : 𝕜₃)
(f : E →SL[σ₁₃] F →SL[σ₂₃] G) :
noncomputable
def
continuous_linear_map.flipₗᵢ'
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
(E : Type u_4)
(F : Type u_6)
(G : Type u_8)
[semi_normed_group E]
[semi_normed_group F]
[semi_normed_group G]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[nondiscrete_normed_field 𝕜₃]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[normed_space 𝕜₃ G]
(σ₂₃ : 𝕜₂ →+* 𝕜₃)
(σ₁₃ : 𝕜 →+* 𝕜₃)
[ring_hom_isometric σ₂₃]
[ring_hom_isometric σ₁₃] :
Flip the order of arguments of a continuous bilinear map.
This is a version bundled as a linear_isometry_equiv.
For an unbundled version see continuous_linear_map.flip.
Equations
- continuous_linear_map.flipₗᵢ' E F G σ₂₃ σ₁₃ = {to_linear_equiv := {to_fun := continuous_linear_map.flip _inst_18, map_add' := _, map_smul' := _, inv_fun := continuous_linear_map.flip _inst_17, left_inv := _, right_inv := _}, norm_map' := _}
@[simp]
theorem
continuous_linear_map.flipₗᵢ'_symm
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[semi_normed_group E]
[semi_normed_group F]
[semi_normed_group G]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[nondiscrete_normed_field 𝕜₃]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[normed_space 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[ring_hom_isometric σ₂₃]
[ring_hom_isometric σ₁₃] :
(continuous_linear_map.flipₗᵢ' E F G σ₂₃ σ₁₃).symm = continuous_linear_map.flipₗᵢ' F E G σ₁₃ σ₂₃
@[simp]
theorem
continuous_linear_map.coe_flipₗᵢ'
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[semi_normed_group E]
[semi_normed_group F]
[semi_normed_group G]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[nondiscrete_normed_field 𝕜₃]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[normed_space 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[ring_hom_isometric σ₂₃]
[ring_hom_isometric σ₁₃] :
⇑(continuous_linear_map.flipₗᵢ' E F G σ₂₃ σ₁₃) = continuous_linear_map.flip
noncomputable
def
continuous_linear_map.flipₗᵢ
(𝕜 : Type u_1)
(E : Type u_4)
(Fₗ : Type u_7)
(Gₗ : Type u_9)
[semi_normed_group E]
[semi_normed_group Fₗ]
[semi_normed_group Gₗ]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ]
[normed_space 𝕜 Gₗ] :
Flip the order of arguments of a continuous bilinear map.
This is a version bundled as a linear_isometry_equiv.
For an unbundled version see continuous_linear_map.flip.
Equations
- continuous_linear_map.flipₗᵢ 𝕜 E Fₗ Gₗ = {to_linear_equiv := {to_fun := continuous_linear_map.flip _, map_add' := _, map_smul' := _, inv_fun := continuous_linear_map.flip _, left_inv := _, right_inv := _}, norm_map' := _}
@[simp]
theorem
continuous_linear_map.flipₗᵢ_symm
{𝕜 : Type u_1}
{E : Type u_4}
{Fₗ : Type u_7}
{Gₗ : Type u_9}
[semi_normed_group E]
[semi_normed_group Fₗ]
[semi_normed_group Gₗ]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ]
[normed_space 𝕜 Gₗ] :
(continuous_linear_map.flipₗᵢ 𝕜 E Fₗ Gₗ).symm = continuous_linear_map.flipₗᵢ 𝕜 Fₗ E Gₗ
@[simp]
theorem
continuous_linear_map.coe_flipₗᵢ
{𝕜 : Type u_1}
{E : Type u_4}
{Fₗ : Type u_7}
{Gₗ : Type u_9}
[semi_normed_group E]
[semi_normed_group Fₗ]
[semi_normed_group Gₗ]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ]
[normed_space 𝕜 Gₗ] :
⇑(continuous_linear_map.flipₗᵢ 𝕜 E Fₗ Gₗ) = continuous_linear_map.flip
noncomputable
def
continuous_linear_map.apply'
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
(F : Type u_6)
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
(σ₁₂ : 𝕜 →+* 𝕜₂)
[ring_hom_isometric σ₁₂] :
The continuous semilinear map obtained by applying a continuous semilinear map at a given vector.
This is the continuous version of linear_map.applyₗ.
Equations
- continuous_linear_map.apply' F σ₁₂ = (continuous_linear_map.id 𝕜₂ (E →SL[σ₁₂] F)).flip
@[simp]
theorem
continuous_linear_map.apply_apply'
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
(v : E)
(f : E →SL[σ₁₂] F) :
⇑(⇑(continuous_linear_map.apply' F σ₁₂) v) f = ⇑f v
noncomputable
def
continuous_linear_map.apply
(𝕜 : Type u_1)
{E : Type u_4}
(Fₗ : Type u_7)
[semi_normed_group E]
[semi_normed_group Fₗ]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ] :
The continuous semilinear map obtained by applying a continuous semilinear map at a given vector.
This is the continuous version of linear_map.applyₗ.
Equations
- continuous_linear_map.apply 𝕜 Fₗ = (continuous_linear_map.id 𝕜 (E →L[𝕜] Fₗ)).flip
@[simp]
theorem
continuous_linear_map.apply_apply
{𝕜 : Type u_1}
{E : Type u_4}
{Fₗ : Type u_7}
[semi_normed_group E]
[semi_normed_group Fₗ]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ]
(v : E)
(f : E →L[𝕜] Fₗ) :
⇑(⇑(continuous_linear_map.apply 𝕜 Fₗ) v) f = ⇑f v
noncomputable
def
continuous_linear_map.compSL
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
(E : Type u_4)
(F : Type u_6)
(G : Type u_8)
[semi_normed_group E]
[semi_normed_group F]
[semi_normed_group G]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[nondiscrete_normed_field 𝕜₃]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[normed_space 𝕜₃ G]
(σ₁₂ : 𝕜 →+* 𝕜₂)
(σ₂₃ : 𝕜₂ →+* 𝕜₃)
{σ₁₃ : 𝕜 →+* 𝕜₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[ring_hom_isometric σ₂₃]
[ring_hom_isometric σ₁₃]
[ring_hom_isometric σ₁₂] :
Composition of continuous semilinear maps as a continuous semibilinear map.
Equations
- continuous_linear_map.compSL E F G σ₁₂ σ₂₃ = (linear_map.mk₂'ₛₗ (ring_hom.id 𝕜₃) σ₂₃ continuous_linear_map.comp _ _ _ _).mk_continuous₂ 1 _
@[simp]
theorem
continuous_linear_map.compSL_apply
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[semi_normed_group E]
[semi_normed_group F]
[semi_normed_group G]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[nondiscrete_normed_field 𝕜₃]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[normed_space 𝕜₃ G]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[ring_hom_isometric σ₂₃]
[ring_hom_isometric σ₁₃]
[ring_hom_isometric σ₁₂]
(f : F →SL[σ₂₃] G)
(g : E →SL[σ₁₂] F) :
⇑(⇑(continuous_linear_map.compSL E F G σ₁₂ σ₂₃) f) g = f.comp g
theorem
continuous.const_clm_comp
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[semi_normed_group E]
[semi_normed_group F]
[semi_normed_group G]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[nondiscrete_normed_field 𝕜₃]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[normed_space 𝕜₃ G]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[ring_hom_isometric σ₂₃]
[ring_hom_isometric σ₁₃]
[ring_hom_isometric σ₁₂]
{X : Type u_5}
[topological_space X]
{f : X → (E →SL[σ₁₂] F)}
(hf : continuous f)
(g : F →SL[σ₂₃] G) :
continuous (λ (x : X), g.comp (f x))
theorem
continuous.clm_comp_const
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[semi_normed_group E]
[semi_normed_group F]
[semi_normed_group G]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[nondiscrete_normed_field 𝕜₃]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[normed_space 𝕜₃ G]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[ring_hom_isometric σ₂₃]
[ring_hom_isometric σ₁₃]
[ring_hom_isometric σ₁₂]
{X : Type u_5}
[topological_space X]
{g : X → (F →SL[σ₂₃] G)}
(hg : continuous g)
(f : E →SL[σ₁₂] F) :
continuous (λ (x : X), (g x).comp f)
noncomputable
def
continuous_linear_map.compL
(𝕜 : Type u_1)
(E : Type u_4)
(Fₗ : Type u_7)
(Gₗ : Type u_9)
[semi_normed_group E]
[semi_normed_group Fₗ]
[semi_normed_group Gₗ]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ]
[normed_space 𝕜 Gₗ] :
Composition of continuous linear maps as a continuous bilinear map.
Equations
- continuous_linear_map.compL 𝕜 E Fₗ Gₗ = continuous_linear_map.compSL E Fₗ Gₗ (ring_hom.id 𝕜) (ring_hom.id 𝕜)
@[simp]
theorem
continuous_linear_map.compL_apply
(𝕜 : Type u_1)
(E : Type u_4)
(Fₗ : Type u_7)
(Gₗ : Type u_9)
[semi_normed_group E]
[semi_normed_group Fₗ]
[semi_normed_group Gₗ]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ]
[normed_space 𝕜 Gₗ]
(f : Fₗ →L[𝕜] Gₗ)
(g : E →L[𝕜] Fₗ) :
⇑(⇑(continuous_linear_map.compL 𝕜 E Fₗ Gₗ) f) g = f.comp g
noncomputable
def
continuous_linear_map.precompR
{𝕜 : Type u_1}
{E : Type u_4}
(Eₗ : Type u_5)
{Fₗ : Type u_7}
{Gₗ : Type u_9}
[semi_normed_group E]
[semi_normed_group Eₗ]
[semi_normed_group Fₗ]
[semi_normed_group Gₗ]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Eₗ]
[normed_space 𝕜 Fₗ]
[normed_space 𝕜 Gₗ]
(L : E →L[𝕜] Fₗ →L[𝕜] Gₗ) :
Apply L(x,-) pointwise to bilinear maps, as a continuous bilinear map
Equations
- continuous_linear_map.precompR Eₗ L = (continuous_linear_map.compL 𝕜 Eₗ Fₗ Gₗ).comp L
@[simp]
theorem
continuous_linear_map.precompR_apply
{𝕜 : Type u_1}
{E : Type u_4}
(Eₗ : Type u_5)
{Fₗ : Type u_7}
{Gₗ : Type u_9}
[semi_normed_group E]
[semi_normed_group Eₗ]
[semi_normed_group Fₗ]
[semi_normed_group Gₗ]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Eₗ]
[normed_space 𝕜 Fₗ]
[normed_space 𝕜 Gₗ]
(L : E →L[𝕜] Fₗ →L[𝕜] Gₗ)
(ᾰ : E) :
⇑(continuous_linear_map.precompR Eₗ L) ᾰ = ⇑(continuous_linear_map.compL 𝕜 Eₗ Fₗ Gₗ) (⇑L ᾰ)
noncomputable
def
continuous_linear_map.precompL
{𝕜 : Type u_1}
{E : Type u_4}
(Eₗ : Type u_5)
{Fₗ : Type u_7}
{Gₗ : Type u_9}
[semi_normed_group E]
[semi_normed_group Eₗ]
[semi_normed_group Fₗ]
[semi_normed_group Gₗ]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Eₗ]
[normed_space 𝕜 Fₗ]
[normed_space 𝕜 Gₗ]
(L : E →L[𝕜] Fₗ →L[𝕜] Gₗ) :
Apply L(-,y) pointwise to bilinear maps, as a continuous bilinear map
Equations
noncomputable
def
continuous_linear_map.prod_mapL
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
(M₁ : Type u₁)
[semi_normed_group M₁]
[normed_space 𝕜 M₁]
(M₂ : Type u₂)
[semi_normed_group M₂]
[normed_space 𝕜 M₂]
(M₃ : Type u₃)
[semi_normed_group M₃]
[normed_space 𝕜 M₃]
(M₄ : Type u₄)
[semi_normed_group M₄]
[normed_space 𝕜 M₄] :
continuous_linear_map.prod_map as a continuous linear map.
Equations
- continuous_linear_map.prod_mapL 𝕜 M₁ M₂ M₃ M₄ = (have Φ₁ : (M₁ →L[𝕜] M₂) →L[𝕜] M₁ →L[𝕜] M₂ × M₄, from ⇑(continuous_linear_map.compL 𝕜 M₁ M₂ (M₂ × M₄)) (continuous_linear_map.inl 𝕜 M₂ M₄), have Φ₂ : (M₃ →L[𝕜] M₄) →L[𝕜] M₃ →L[𝕜] M₂ × M₄, from ⇑(continuous_linear_map.compL 𝕜 M₃ M₄ (M₂ × M₄)) (continuous_linear_map.inr 𝕜 M₂ M₄), have Φ₁' : (M₁ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄, from ⇑((continuous_linear_map.compL 𝕜 (M₁ × M₃) M₁ (M₂ × M₄)).flip) (continuous_linear_map.fst 𝕜 M₁ M₃), have Φ₂' : (M₃ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄, from ⇑((continuous_linear_map.compL 𝕜 (M₁ × M₃) M₃ (M₂ × M₄)).flip) (continuous_linear_map.snd 𝕜 M₁ M₃), have Ψ₁ : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄) →L[𝕜] M₁ →L[𝕜] M₂, from continuous_linear_map.fst 𝕜 (M₁ →L[𝕜] M₂) (M₃ →L[𝕜] M₄), have Ψ₂ : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄) →L[𝕜] M₃ →L[𝕜] M₄, from continuous_linear_map.snd 𝕜 (M₁ →L[𝕜] M₂) (M₃ →L[𝕜] M₄), Φ₁'.comp (Φ₁.comp Ψ₁) + Φ₂'.comp (Φ₂.comp Ψ₂)).copy (λ (p : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄)), p.fst.prod_map p.snd) _
@[simp]
theorem
continuous_linear_map.prod_mapL_apply
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
{M₁ : Type u₁}
[semi_normed_group M₁]
[normed_space 𝕜 M₁]
{M₂ : Type u₂}
[semi_normed_group M₂]
[normed_space 𝕜 M₂]
{M₃ : Type u₃}
[semi_normed_group M₃]
[normed_space 𝕜 M₃]
{M₄ : Type u₄}
[semi_normed_group M₄]
[normed_space 𝕜 M₄]
(p : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄)) :
theorem
continuous.prod_mapL
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
{M₁ : Type u₁}
[semi_normed_group M₁]
[normed_space 𝕜 M₁]
{M₂ : Type u₂}
[semi_normed_group M₂]
[normed_space 𝕜 M₂]
{M₃ : Type u₃}
[semi_normed_group M₃]
[normed_space 𝕜 M₃]
{M₄ : Type u₄}
[semi_normed_group M₄]
[normed_space 𝕜 M₄]
{X : Type u_11}
[topological_space X]
{f : X → (M₁ →L[𝕜] M₂)}
{g : X → (M₃ →L[𝕜] M₄)}
(hf : continuous f)
(hg : continuous g) :
continuous (λ (x : X), (f x).prod_map (g x))
theorem
continuous.prod_map_equivL
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
{M₁ : Type u₁}
[semi_normed_group M₁]
[normed_space 𝕜 M₁]
{M₂ : Type u₂}
[semi_normed_group M₂]
[normed_space 𝕜 M₂]
{M₃ : Type u₃}
[semi_normed_group M₃]
[normed_space 𝕜 M₃]
{M₄ : Type u₄}
[semi_normed_group M₄]
[normed_space 𝕜 M₄]
{X : Type u_11}
[topological_space X]
{f : X → (M₁ ≃L[𝕜] M₂)}
{g : X → (M₃ ≃L[𝕜] M₄)}
(hf : continuous (λ (x : X), ↑(f x)))
(hg : continuous (λ (x : X), ↑(g x))) :
continuous (λ (x : X), ↑((f x).prod (g x)))
theorem
continuous_on.prod_mapL
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
{M₁ : Type u₁}
[semi_normed_group M₁]
[normed_space 𝕜 M₁]
{M₂ : Type u₂}
[semi_normed_group M₂]
[normed_space 𝕜 M₂]
{M₃ : Type u₃}
[semi_normed_group M₃]
[normed_space 𝕜 M₃]
{M₄ : Type u₄}
[semi_normed_group M₄]
[normed_space 𝕜 M₄]
{X : Type u_11}
[topological_space X]
{f : X → (M₁ →L[𝕜] M₂)}
{g : X → (M₃ →L[𝕜] M₄)}
{s : set X}
(hf : continuous_on f s)
(hg : continuous_on g s) :
continuous_on (λ (x : X), (f x).prod_map (g x)) s
theorem
continuous_on.prod_map_equivL
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
{M₁ : Type u₁}
[semi_normed_group M₁]
[normed_space 𝕜 M₁]
{M₂ : Type u₂}
[semi_normed_group M₂]
[normed_space 𝕜 M₂]
{M₃ : Type u₃}
[semi_normed_group M₃]
[normed_space 𝕜 M₃]
{M₄ : Type u₄}
[semi_normed_group M₄]
[normed_space 𝕜 M₄]
{X : Type u_11}
[topological_space X]
{f : X → (M₁ ≃L[𝕜] M₂)}
{g : X → (M₃ ≃L[𝕜] M₄)}
{s : set X}
(hf : continuous_on (λ (x : X), ↑(f x)) s)
(hg : continuous_on (λ (x : X), ↑(g x)) s) :
continuous_on (λ (x : X), ↑((f x).prod (g x))) s
noncomputable
def
continuous_linear_map.lmul
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
(𝕜' : Type u_11)
[normed_ring 𝕜']
[normed_algebra 𝕜 𝕜'] :
Left multiplication in a normed algebra as a continuous bilinear map.
Equations
- continuous_linear_map.lmul 𝕜 𝕜' = (algebra.lmul 𝕜 𝕜').to_linear_map.mk_continuous₂ 1 _
@[simp]
theorem
continuous_linear_map.lmul_apply
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
(𝕜' : Type u_11)
[normed_ring 𝕜']
[normed_algebra 𝕜 𝕜']
(x y : 𝕜') :
⇑(⇑(continuous_linear_map.lmul 𝕜 𝕜') x) y = x * y
@[simp]
theorem
continuous_linear_map.op_norm_lmul_apply_le
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
(𝕜' : Type u_11)
[normed_ring 𝕜']
[normed_algebra 𝕜 𝕜']
(x : 𝕜') :
noncomputable
def
continuous_linear_map.lmulₗᵢ
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
(𝕜' : Type u_11)
[normed_ring 𝕜']
[normed_algebra 𝕜 𝕜']
[norm_one_class 𝕜'] :
Left multiplication in a normed algebra as a linear isometry to the space of continuous linear maps.
Equations
- continuous_linear_map.lmulₗᵢ 𝕜 𝕜' = {to_linear_map := ↑(continuous_linear_map.lmul 𝕜 𝕜'), norm_map' := _}
@[simp]
theorem
continuous_linear_map.coe_lmulₗᵢ
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
(𝕜' : Type u_11)
[normed_ring 𝕜']
[normed_algebra 𝕜 𝕜']
[norm_one_class 𝕜'] :
⇑(continuous_linear_map.lmulₗᵢ 𝕜 𝕜') = ⇑(continuous_linear_map.lmul 𝕜 𝕜')
@[simp]
theorem
continuous_linear_map.op_norm_lmul_apply
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
(𝕜' : Type u_11)
[normed_ring 𝕜']
[normed_algebra 𝕜 𝕜']
[norm_one_class 𝕜']
(x : 𝕜') :
noncomputable
def
continuous_linear_map.lmul_right
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
(𝕜' : Type u_11)
[normed_ring 𝕜']
[normed_algebra 𝕜 𝕜'] :
Right-multiplication in a normed algebra, considered as a continuous linear map.
Equations
@[simp]
theorem
continuous_linear_map.lmul_right_apply
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
(𝕜' : Type u_11)
[normed_ring 𝕜']
[normed_algebra 𝕜 𝕜']
(x y : 𝕜') :
⇑(⇑(continuous_linear_map.lmul_right 𝕜 𝕜') x) y = y * x
@[simp]
theorem
continuous_linear_map.op_norm_lmul_right_apply_le
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
(𝕜' : Type u_11)
[normed_ring 𝕜']
[normed_algebra 𝕜 𝕜']
(x : 𝕜') :
@[simp]
theorem
continuous_linear_map.op_norm_lmul_right_apply
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
(𝕜' : Type u_11)
[normed_ring 𝕜']
[normed_algebra 𝕜 𝕜']
[norm_one_class 𝕜']
(x : 𝕜') :
noncomputable
def
continuous_linear_map.lmul_rightₗᵢ
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
(𝕜' : Type u_11)
[normed_ring 𝕜']
[normed_algebra 𝕜 𝕜']
[norm_one_class 𝕜'] :
Right-multiplication in a normed algebra, considered as a linear isometry to the space of continuous linear maps.
Equations
- continuous_linear_map.lmul_rightₗᵢ 𝕜 𝕜' = {to_linear_map := ↑(continuous_linear_map.lmul_right 𝕜 𝕜'), norm_map' := _}
@[simp]
theorem
continuous_linear_map.coe_lmul_rightₗᵢ
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
(𝕜' : Type u_11)
[normed_ring 𝕜']
[normed_algebra 𝕜 𝕜']
[norm_one_class 𝕜'] :
noncomputable
def
continuous_linear_map.lmul_left_right
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
(𝕜' : Type u_11)
[normed_ring 𝕜']
[normed_algebra 𝕜 𝕜'] :
Simultaneous left- and right-multiplication in a normed algebra, considered as a continuous trilinear map.
Equations
- continuous_linear_map.lmul_left_right 𝕜 𝕜' = ((continuous_linear_map.compL 𝕜 𝕜' 𝕜' 𝕜').comp (continuous_linear_map.lmul_right 𝕜 𝕜')).flip.comp (continuous_linear_map.lmul 𝕜 𝕜')
@[simp]
theorem
continuous_linear_map.lmul_left_right_apply
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
(𝕜' : Type u_11)
[normed_ring 𝕜']
[normed_algebra 𝕜 𝕜']
(x y z : 𝕜') :
theorem
continuous_linear_map.op_norm_lmul_left_right_apply_apply_le
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
(𝕜' : Type u_11)
[normed_ring 𝕜']
[normed_algebra 𝕜 𝕜']
(x y : 𝕜') :
theorem
continuous_linear_map.op_norm_lmul_left_right_apply_le
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
(𝕜' : Type u_11)
[normed_ring 𝕜']
[normed_algebra 𝕜 𝕜']
(x : 𝕜') :
theorem
continuous_linear_map.op_norm_lmul_left_right_le
(𝕜 : Type u_1)
[nondiscrete_normed_field 𝕜]
(𝕜' : Type u_11)
[normed_ring 𝕜']
[normed_algebra 𝕜 𝕜'] :
noncomputable
def
continuous_linear_map.lsmul
(𝕜 : Type u_1)
{E : Type u_4}
[semi_normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
(𝕜' : Type u_11)
[normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' E]
[is_scalar_tower 𝕜 𝕜' E] :
Scalar multiplication as a continuous bilinear map.
Equations
- continuous_linear_map.lsmul 𝕜 𝕜' = (algebra.lsmul 𝕜 E).to_linear_map.mk_continuous₂ 1 _
@[simp]
theorem
continuous_linear_map.lsmul_apply
(𝕜 : Type u_1)
{E : Type u_4}
[semi_normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
(𝕜' : Type u_11)
[normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' E]
[is_scalar_tower 𝕜 𝕜' E]
(c : 𝕜')
(x : E) :
⇑(⇑(continuous_linear_map.lsmul 𝕜 𝕜') c) x = c • x
theorem
continuous_linear_map.norm_to_span_singleton
(𝕜 : Type u_1)
{E : Type u_4}
[semi_normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
(x : E) :
theorem
continuous_linear_map.op_norm_lsmul_apply_le
{𝕜 : Type u_1}
{E : Type u_4}
[semi_normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
{𝕜' : Type u_11}
[normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' E]
[is_scalar_tower 𝕜 𝕜' E]
(x : 𝕜') :
theorem
continuous_linear_map.op_norm_lsmul_le
{𝕜 : Type u_1}
{E : Type u_4}
[semi_normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
{𝕜' : Type u_11}
[normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' E]
[is_scalar_tower 𝕜 𝕜' E] :
∥continuous_linear_map.lsmul 𝕜 𝕜'∥ ≤ 1
The norm of lsmul is at most 1 in any semi-normed group.
@[simp]
theorem
continuous_linear_map.norm_restrict_scalars
{𝕜 : Type u_1}
{E : Type u_4}
{Fₗ : Type u_7}
[semi_normed_group E]
[semi_normed_group Fₗ]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ]
{𝕜' : Type u_11}
[nondiscrete_normed_field 𝕜']
[normed_algebra 𝕜' 𝕜]
[normed_space 𝕜' E]
[is_scalar_tower 𝕜' 𝕜 E]
[normed_space 𝕜' Fₗ]
[is_scalar_tower 𝕜' 𝕜 Fₗ]
(f : E →L[𝕜] Fₗ) :
def
continuous_linear_map.restrict_scalars_isometry
(𝕜 : Type u_1)
(E : Type u_4)
(Fₗ : Type u_7)
[semi_normed_group E]
[semi_normed_group Fₗ]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ]
(𝕜' : Type u_11)
[nondiscrete_normed_field 𝕜']
[normed_algebra 𝕜' 𝕜]
[normed_space 𝕜' E]
[is_scalar_tower 𝕜' 𝕜 E]
[normed_space 𝕜' Fₗ]
[is_scalar_tower 𝕜' 𝕜 Fₗ]
(𝕜'' : Type u_12)
[ring 𝕜'']
[module 𝕜'' Fₗ]
[has_continuous_const_smul 𝕜'' Fₗ]
[smul_comm_class 𝕜 𝕜'' Fₗ]
[smul_comm_class 𝕜' 𝕜'' Fₗ] :
continuous_linear_map.restrict_scalars as a linear_isometry.
Equations
- continuous_linear_map.restrict_scalars_isometry 𝕜 E Fₗ 𝕜' 𝕜'' = {to_linear_map := continuous_linear_map.restrict_scalarsₗ 𝕜 E Fₗ 𝕜' 𝕜'' normed_top_group, norm_map' := _}
@[simp]
theorem
continuous_linear_map.coe_restrict_scalars_isometry
{𝕜 : Type u_1}
{E : Type u_4}
{Fₗ : Type u_7}
[semi_normed_group E]
[semi_normed_group Fₗ]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ]
{𝕜' : Type u_11}
[nondiscrete_normed_field 𝕜']
[normed_algebra 𝕜' 𝕜]
[normed_space 𝕜' E]
[is_scalar_tower 𝕜' 𝕜 E]
[normed_space 𝕜' Fₗ]
[is_scalar_tower 𝕜' 𝕜 Fₗ]
{𝕜'' : Type u_12}
[ring 𝕜'']
[module 𝕜'' Fₗ]
[has_continuous_const_smul 𝕜'' Fₗ]
[smul_comm_class 𝕜 𝕜'' Fₗ]
[smul_comm_class 𝕜' 𝕜'' Fₗ] :
@[simp]
theorem
continuous_linear_map.restrict_scalars_isometry_to_linear_map
{𝕜 : Type u_1}
{E : Type u_4}
{Fₗ : Type u_7}
[semi_normed_group E]
[semi_normed_group Fₗ]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ]
{𝕜' : Type u_11}
[nondiscrete_normed_field 𝕜']
[normed_algebra 𝕜' 𝕜]
[normed_space 𝕜' E]
[is_scalar_tower 𝕜' 𝕜 E]
[normed_space 𝕜' Fₗ]
[is_scalar_tower 𝕜' 𝕜 Fₗ]
{𝕜'' : Type u_12}
[ring 𝕜'']
[module 𝕜'' Fₗ]
[has_continuous_const_smul 𝕜'' Fₗ]
[smul_comm_class 𝕜 𝕜'' Fₗ]
[smul_comm_class 𝕜' 𝕜'' Fₗ] :
(continuous_linear_map.restrict_scalars_isometry 𝕜 E Fₗ 𝕜' 𝕜'').to_linear_map = continuous_linear_map.restrict_scalarsₗ 𝕜 E Fₗ 𝕜' 𝕜''
noncomputable
def
continuous_linear_map.restrict_scalarsL
(𝕜 : Type u_1)
(E : Type u_4)
(Fₗ : Type u_7)
[semi_normed_group E]
[semi_normed_group Fₗ]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ]
(𝕜' : Type u_11)
[nondiscrete_normed_field 𝕜']
[normed_algebra 𝕜' 𝕜]
[normed_space 𝕜' E]
[is_scalar_tower 𝕜' 𝕜 E]
[normed_space 𝕜' Fₗ]
[is_scalar_tower 𝕜' 𝕜 Fₗ]
(𝕜'' : Type u_12)
[ring 𝕜'']
[module 𝕜'' Fₗ]
[has_continuous_const_smul 𝕜'' Fₗ]
[smul_comm_class 𝕜 𝕜'' Fₗ]
[smul_comm_class 𝕜' 𝕜'' Fₗ] :
continuous_linear_map.restrict_scalars as a continuous_linear_map.
Equations
- continuous_linear_map.restrict_scalarsL 𝕜 E Fₗ 𝕜' 𝕜'' = (continuous_linear_map.restrict_scalars_isometry 𝕜 E Fₗ 𝕜' 𝕜'').to_continuous_linear_map
@[simp]
theorem
continuous_linear_map.coe_restrict_scalarsL
{𝕜 : Type u_1}
{E : Type u_4}
{Fₗ : Type u_7}
[semi_normed_group E]
[semi_normed_group Fₗ]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ]
{𝕜' : Type u_11}
[nondiscrete_normed_field 𝕜']
[normed_algebra 𝕜' 𝕜]
[normed_space 𝕜' E]
[is_scalar_tower 𝕜' 𝕜 E]
[normed_space 𝕜' Fₗ]
[is_scalar_tower 𝕜' 𝕜 Fₗ]
{𝕜'' : Type u_12}
[ring 𝕜'']
[module 𝕜'' Fₗ]
[has_continuous_const_smul 𝕜'' Fₗ]
[smul_comm_class 𝕜 𝕜'' Fₗ]
[smul_comm_class 𝕜' 𝕜'' Fₗ] :
↑(continuous_linear_map.restrict_scalarsL 𝕜 E Fₗ 𝕜' 𝕜'') = continuous_linear_map.restrict_scalarsₗ 𝕜 E Fₗ 𝕜' 𝕜''
@[simp]
theorem
continuous_linear_map.coe_restrict_scalarsL'
{𝕜 : Type u_1}
{E : Type u_4}
{Fₗ : Type u_7}
[semi_normed_group E]
[semi_normed_group Fₗ]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ]
{𝕜' : Type u_11}
[nondiscrete_normed_field 𝕜']
[normed_algebra 𝕜' 𝕜]
[normed_space 𝕜' E]
[is_scalar_tower 𝕜' 𝕜 E]
[normed_space 𝕜' Fₗ]
[is_scalar_tower 𝕜' 𝕜 Fₗ]
{𝕜'' : Type u_12}
[ring 𝕜'']
[module 𝕜'' Fₗ]
[has_continuous_const_smul 𝕜'' Fₗ]
[smul_comm_class 𝕜 𝕜'' Fₗ]
[smul_comm_class 𝕜' 𝕜'' Fₗ] :
⇑(continuous_linear_map.restrict_scalarsL 𝕜 E Fₗ 𝕜' 𝕜'') = continuous_linear_map.restrict_scalars 𝕜'
theorem
submodule.norm_subtypeL_le
{𝕜 : Type u_1}
{E : Type u_4}
[semi_normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
(K : submodule 𝕜 E) :
@[protected]
theorem
continuous_linear_map.has_sum
{ι : Type u_11}
{R : Type u_12}
{R₂ : Type u_13}
{M : Type u_14}
{M₂ : Type u_15}
[semiring R]
[semiring R₂]
[add_comm_monoid M]
[module R M]
[add_comm_monoid M₂]
[module R₂ M₂]
[topological_space M]
[topological_space M₂]
{σ : R →+* R₂}
{f : ι → M}
(φ : M →SL[σ] M₂)
{x : M}
(hf : has_sum f x) :
Applying a continuous linear map commutes with taking an (infinite) sum.
theorem
has_sum.mapL
{ι : Type u_11}
{R : Type u_12}
{R₂ : Type u_13}
{M : Type u_14}
{M₂ : Type u_15}
[semiring R]
[semiring R₂]
[add_comm_monoid M]
[module R M]
[add_comm_monoid M₂]
[module R₂ M₂]
[topological_space M]
[topological_space M₂]
{σ : R →+* R₂}
{f : ι → M}
(φ : M →SL[σ] M₂)
{x : M}
(hf : has_sum f x) :
Alias of continuous_linear_map.has_sum.
@[protected]
theorem
continuous_linear_map.summable
{ι : Type u_11}
{R : Type u_12}
{R₂ : Type u_13}
{M : Type u_14}
{M₂ : Type u_15}
[semiring R]
[semiring R₂]
[add_comm_monoid M]
[module R M]
[add_comm_monoid M₂]
[module R₂ M₂]
[topological_space M]
[topological_space M₂]
{σ : R →+* R₂}
{f : ι → M}
(φ : M →SL[σ] M₂)
(hf : summable f) :
theorem
summable.mapL
{ι : Type u_11}
{R : Type u_12}
{R₂ : Type u_13}
{M : Type u_14}
{M₂ : Type u_15}
[semiring R]
[semiring R₂]
[add_comm_monoid M]
[module R M]
[add_comm_monoid M₂]
[module R₂ M₂]
[topological_space M]
[topological_space M₂]
{σ : R →+* R₂}
{f : ι → M}
(φ : M →SL[σ] M₂)
(hf : summable f) :
Alias of continuous_linear_map.summable.
@[protected]
theorem
continuous_linear_map.map_tsum
{ι : Type u_11}
{R : Type u_12}
{R₂ : Type u_13}
{M : Type u_14}
{M₂ : Type u_15}
[semiring R]
[semiring R₂]
[add_comm_monoid M]
[module R M]
[add_comm_monoid M₂]
[module R₂ M₂]
[topological_space M]
[topological_space M₂]
{σ : R →+* R₂}
[t2_space M₂]
{f : ι → M}
(φ : M →SL[σ] M₂)
(hf : summable f) :
@[protected]
theorem
continuous_linear_equiv.has_sum
{ι : Type u_11}
{R : Type u_12}
{R₂ : Type u_13}
{M : Type u_14}
{M₂ : Type u_15}
[semiring R]
[semiring R₂]
[add_comm_monoid M]
[module R M]
[add_comm_monoid M₂]
[module R₂ M₂]
[topological_space M]
[topological_space M₂]
{σ : R →+* R₂}
{σ' : R₂ →+* R}
[ring_hom_inv_pair σ σ']
[ring_hom_inv_pair σ' σ]
{f : ι → M}
(e : M ≃SL[σ] M₂)
{y : M₂} :
Applying a continuous linear map commutes with taking an (infinite) sum.
@[protected]
theorem
continuous_linear_equiv.summable
{ι : Type u_11}
{R : Type u_12}
{R₂ : Type u_13}
{M : Type u_14}
{M₂ : Type u_15}
[semiring R]
[semiring R₂]
[add_comm_monoid M]
[module R M]
[add_comm_monoid M₂]
[module R₂ M₂]
[topological_space M]
[topological_space M₂]
{σ : R →+* R₂}
{σ' : R₂ →+* R}
[ring_hom_inv_pair σ σ']
[ring_hom_inv_pair σ' σ]
{f : ι → M}
(e : M ≃SL[σ] M₂) :
theorem
continuous_linear_equiv.tsum_eq_iff
{ι : Type u_11}
{R : Type u_12}
{R₂ : Type u_13}
{M : Type u_14}
{M₂ : Type u_15}
[semiring R]
[semiring R₂]
[add_comm_monoid M]
[module R M]
[add_comm_monoid M₂]
[module R₂ M₂]
[topological_space M]
[topological_space M₂]
{σ : R →+* R₂}
{σ' : R₂ →+* R}
[ring_hom_inv_pair σ σ']
[ring_hom_inv_pair σ' σ]
[t2_space M]
[t2_space M₂]
{f : ι → M}
(e : M ≃SL[σ] M₂)
{y : M₂} :
@[protected]
theorem
continuous_linear_equiv.map_tsum
{ι : Type u_11}
{R : Type u_12}
{R₂ : Type u_13}
{M : Type u_14}
{M₂ : Type u_15}
[semiring R]
[semiring R₂]
[add_comm_monoid M]
[module R M]
[add_comm_monoid M₂]
[module R₂ M₂]
[topological_space M]
[topological_space M₂]
{σ : R →+* R₂}
{σ' : R₂ →+* R}
[ring_hom_inv_pair σ σ']
[ring_hom_inv_pair σ' σ]
[t2_space M]
[t2_space M₂]
{f : ι → M}
(e : M ≃SL[σ] M₂) :
@[protected]
theorem
continuous_linear_equiv.lipschitz
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{σ₂₁ : 𝕜₂ →+* 𝕜}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[ring_hom_isometric σ₁₂]
(e : E ≃SL[σ₁₂] F) :
theorem
continuous_linear_equiv.is_O_comp
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{σ₂₁ : 𝕜₂ →+* 𝕜}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[ring_hom_isometric σ₁₂]
(e : E ≃SL[σ₁₂] F)
{α : Type u_3}
(f : α → E)
(l : filter α) :
theorem
continuous_linear_equiv.is_O_sub
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{σ₂₁ : 𝕜₂ →+* 𝕜}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[ring_hom_isometric σ₁₂]
(e : E ≃SL[σ₁₂] F)
(l : filter E)
(x : E) :
theorem
continuous_linear_equiv.homothety_inverse
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{σ₂₁ : 𝕜₂ →+* 𝕜}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
(a : ℝ)
(ha : 0 < a)
(f : E ≃ₛₗ[σ₁₂] F) :
def
continuous_linear_equiv.of_homothety
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ 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 = {to_linear_equiv := f, continuous_to_fun := _, continuous_inv_fun := _}
theorem
continuous_linear_equiv.is_O_comp_rev
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{σ₂₁ : 𝕜₂ →+* 𝕜}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[ring_hom_isometric σ₂₁]
(e : E ≃SL[σ₁₂] F)
{α : Type u_3}
(f : α → E)
(l : filter α) :
theorem
continuous_linear_equiv.is_O_sub_rev
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{σ₂₁ : 𝕜₂ →+* 𝕜}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[ring_hom_isometric σ₂₁]
(e : E ≃SL[σ₁₂] F)
(l : filter E)
(x : E) :
theorem
continuous_linear_equiv.to_span_nonzero_singleton_homothety
(𝕜 : Type u_1)
{E : Type u_4}
[semi_normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
(x : E)
(h : x ≠ 0)
(c : 𝕜) :
def
linear_equiv.to_continuous_linear_equiv_of_bounds
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[semi_normed_group E]
[semi_normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ 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 := _}
noncomputable
def
continuous_linear_map.bilinear_comp
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[semi_normed_group E]
[semi_normed_group F]
[semi_normed_group G]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[nondiscrete_normed_field 𝕜₃]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[normed_space 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
{E' : Type u_11}
{F' : Type u_12}
[semi_normed_group E']
[semi_normed_group F']
{𝕜₁' : Type u_13}
{𝕜₂' : Type u_14}
[nondiscrete_normed_field 𝕜₁']
[nondiscrete_normed_field 𝕜₂']
[normed_space 𝕜₁' E']
[normed_space 𝕜₂' F']
{σ₁' : 𝕜₁' →+* 𝕜}
{σ₁₃' : 𝕜₁' →+* 𝕜₃}
{σ₂' : 𝕜₂' →+* 𝕜₂}
{σ₂₃' : 𝕜₂' →+* 𝕜₃}
[ring_hom_comp_triple σ₁' σ₁₃ σ₁₃']
[ring_hom_comp_triple σ₂' σ₂₃ σ₂₃']
[ring_hom_isometric σ₂₃]
[ring_hom_isometric σ₁₃']
[ring_hom_isometric σ₂₃']
(f : E →SL[σ₁₃] F →SL[σ₂₃] G)
(gE : E' →SL[σ₁'] E)
(gF : F' →SL[σ₂'] F) :
Compose a bilinear map E →SL[σ₁₃] F →SL[σ₂₃] G with two linear maps
E' →SL[σ₁'] E and F' →SL[σ₂'] F.
@[simp]
theorem
continuous_linear_map.bilinear_comp_apply
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[semi_normed_group E]
[semi_normed_group F]
[semi_normed_group G]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[nondiscrete_normed_field 𝕜₃]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[normed_space 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
{E' : Type u_11}
{F' : Type u_12}
[semi_normed_group E']
[semi_normed_group F']
{𝕜₁' : Type u_13}
{𝕜₂' : Type u_14}
[nondiscrete_normed_field 𝕜₁']
[nondiscrete_normed_field 𝕜₂']
[normed_space 𝕜₁' E']
[normed_space 𝕜₂' F']
{σ₁' : 𝕜₁' →+* 𝕜}
{σ₁₃' : 𝕜₁' →+* 𝕜₃}
{σ₂' : 𝕜₂' →+* 𝕜₂}
{σ₂₃' : 𝕜₂' →+* 𝕜₃}
[ring_hom_comp_triple σ₁' σ₁₃ σ₁₃']
[ring_hom_comp_triple σ₂' σ₂₃ σ₂₃']
[ring_hom_isometric σ₂₃]
[ring_hom_isometric σ₁₃']
[ring_hom_isometric σ₂₃']
(f : E →SL[σ₁₃] F →SL[σ₂₃] G)
(gE : E' →SL[σ₁'] E)
(gF : F' →SL[σ₂'] F)
(x : E')
(y : F') :
noncomputable
def
continuous_linear_map.deriv₂
{𝕜 : Type u_1}
{E : Type u_4}
{Fₗ : Type u_7}
{Gₗ : Type u_9}
[semi_normed_group E]
[semi_normed_group Fₗ]
[semi_normed_group Gₗ]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ]
[normed_space 𝕜 Gₗ]
(f : E →L[𝕜] Fₗ →L[𝕜] Gₗ) :
Derivative of a continuous bilinear map f : E →L[𝕜] F →L[𝕜] G interpreted as a map E × F → G
at point p : E × F evaluated at q : E × F, as a continuous bilinear map.
Equations
- f.deriv₂ = f.bilinear_comp (continuous_linear_map.fst 𝕜 E Fₗ) (continuous_linear_map.snd 𝕜 E Fₗ) + f.flip.bilinear_comp (continuous_linear_map.snd 𝕜 E Fₗ) (continuous_linear_map.fst 𝕜 E Fₗ)
@[simp]
theorem
continuous_linear_map.coe_deriv₂
{𝕜 : Type u_1}
{E : Type u_4}
{Fₗ : Type u_7}
{Gₗ : Type u_9}
[semi_normed_group E]
[semi_normed_group Fₗ]
[semi_normed_group Gₗ]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ]
[normed_space 𝕜 Gₗ]
(f : E →L[𝕜] Fₗ →L[𝕜] Gₗ)
(p : E × Fₗ) :
theorem
continuous_linear_map.map_add_add
{𝕜 : Type u_1}
{E : Type u_4}
{Fₗ : Type u_7}
{Gₗ : Type u_9}
[semi_normed_group E]
[semi_normed_group Fₗ]
[semi_normed_group Gₗ]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ]
[normed_space 𝕜 Gₗ]
(f : E →L[𝕜] Fₗ →L[𝕜] Gₗ)
(x x' : E)
(y y' : Fₗ) :
theorem
linear_map.bound_of_shell
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
(f : E →ₛₗ[σ₁₂] F)
{ε C : ℝ}
(ε_pos : 0 < ε)
{c : 𝕜}
(hc : 1 < ∥c∥)
(hf : ∀ (x : E), ε / ∥c∥ ≤ ∥x∥ → ∥x∥ < ε → ∥⇑f x∥ ≤ C * ∥x∥)
(x : E) :
theorem
linear_map.bound_of_ball_bound
{𝕜 : Type u_1}
{E : Type u_4}
{Fₗ : Type u_7}
[normed_group E]
[normed_group Fₗ]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ]
{r : ℝ}
(r_pos : 0 < r)
(c : ℝ)
(f : E →ₗ[𝕜] Fₗ)
(h : ∀ (z : E), z ∈ metric.ball 0 r → ∥⇑f z∥ ≤ c) :
linear_map.bound_of_ball_bound' is a version of this lemma over a field satisfying is_R_or_C
that produces a concrete bound.
theorem
continuous_linear_map.op_norm_zero_iff
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
(f : E →SL[σ₁₂] F)
[ring_hom_isometric σ₁₂] :
An operator is zero iff its norm vanishes.
@[simp]
theorem
continuous_linear_map.norm_id
{𝕜 : Type u_1}
{E : Type u_4}
[normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[nontrivial E] :
∥continuous_linear_map.id 𝕜 E∥ = 1
If a normed space is non-trivial, then the norm of the identity equals 1.
@[protected, instance]
def
continuous_linear_map.norm_one_class
{𝕜 : Type u_1}
{E : Type u_4}
[normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[nontrivial E] :
norm_one_class (E →L[𝕜] E)
@[protected, instance]
noncomputable
def
continuous_linear_map.to_normed_group
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂] :
normed_group (E →SL[σ₁₂] 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 →SL[σ₁₂] F) continuous_linear_map.to_normed_group._proof_2
@[protected, instance]
noncomputable
def
continuous_linear_map.to_normed_ring
{𝕜 : Type u_1}
{E : Type u_4}
[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
- continuous_linear_map.to_normed_ring = {to_has_norm := normed_group.to_has_norm continuous_linear_map.to_normed_group, to_ring := semi_normed_ring.to_ring continuous_linear_map.to_semi_normed_ring, to_metric_space := normed_group.to_metric_space continuous_linear_map.to_normed_group, dist_eq := _, norm_mul := _}
theorem
continuous_linear_map.homothety_norm
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
[nontrivial E]
(f : E →SL[σ₁₂] F)
{a : ℝ}
(hf : ∀ (x : E), ∥⇑f x∥ = a * ∥x∥) :
theorem
continuous_linear_map.to_span_singleton_norm
{𝕜 : Type u_1}
{E : Type u_4}
[normed_group E]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
(x : E) :
theorem
continuous_linear_map.uniform_embedding_of_bound
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[normed_group E]
[normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
(f : E →SL[σ₁₂] F)
{K : nnreal}
(hf : ∀ (x : E), ∥x∥ ≤ ↑K * ∥⇑f x∥) :
theorem
continuous_linear_map.antilipschitz_of_uniform_embedding
{𝕜 : Type u_1}
{E : Type u_4}
{Fₗ : Type u_7}
[normed_group E]
[normed_group Fₗ]
[nondiscrete_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ]
(f : E →L[𝕜] Fₗ)
(hf : 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.
def
continuous_linear_map.of_mem_closure_image_coe_bounded
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{F : Type u_6}
[normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{E' : Type u_11}
[semi_normed_group E']
[normed_space 𝕜 E']
[ring_hom_isometric σ₁₂]
(f : E' → F)
{s : set (E' →SL[σ₁₂] F)}
(hs : metric.bounded s)
(hf : f ∈ closure (coe_fn '' s)) :
Construct a bundled continuous (semi)linear map from a map f : E → F and a proof of the fact
that it belongs to the closure of the image of a bounded set s : set (E →SL[σ₁₂] F) under coercion
to function. Coercion to function of the result is definitionally equal to f.
@[simp]
theorem
continuous_linear_map.of_mem_closure_image_coe_bounded_apply
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{F : Type u_6}
[normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{E' : Type u_11}
[semi_normed_group E']
[normed_space 𝕜 E']
[ring_hom_isometric σ₁₂]
(f : E' → F)
{s : set (E' →SL[σ₁₂] F)}
(hs : metric.bounded s)
(hf : f ∈ closure (coe_fn '' s)) :
def
continuous_linear_map.of_tendsto_of_bounded_range
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{F : Type u_6}
[normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{E' : Type u_11}
[semi_normed_group E']
[normed_space 𝕜 E']
[ring_hom_isometric σ₁₂]
{α : Type u_3}
{l : filter α}
[l.ne_bot]
(f : E' → F)
(g : α → (E' →SL[σ₁₂] F))
(hf : filter.tendsto (λ (a : α) (x : E'), ⇑(g a) x) l (nhds f))
(hg : metric.bounded (set.range g)) :
Let f : E → F be a map, let g : α → E →SL[σ₁₂] F be a family of continuous (semi)linear maps
that takes values in a bounded set and converges to f pointwise along a nontrivial filter. Then
f is a continuous (semi)linear map.
Equations
@[simp]
theorem
continuous_linear_map.of_tendsto_of_bounded_range_apply
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{F : Type u_6}
[normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{E' : Type u_11}
[semi_normed_group E']
[normed_space 𝕜 E']
[ring_hom_isometric σ₁₂]
{α : Type u_3}
{l : filter α}
[l.ne_bot]
(f : E' → F)
(g : α → (E' →SL[σ₁₂] F))
(hf : filter.tendsto (λ (a : α) (x : E'), ⇑(g a) x) l (nhds f))
(hg : metric.bounded (set.range g)) :
⇑(continuous_linear_map.of_tendsto_of_bounded_range f g hf hg) = f
theorem
continuous_linear_map.tendsto_of_tendsto_pointwise_of_cauchy_seq
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{F : Type u_6}
[normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{E' : Type u_11}
[semi_normed_group E']
[normed_space 𝕜 E']
[ring_hom_isometric σ₁₂]
{f : ℕ → (E' →SL[σ₁₂] F)}
{g : E' →SL[σ₁₂] F}
(hg : filter.tendsto (λ (n : ℕ) (x : E'), ⇑(f n) x) filter.at_top (nhds ⇑g))
(hf : cauchy_seq f) :
filter.tendsto f filter.at_top (nhds g)
If a Cauchy sequence of continuous linear map converges to a continuous linear map pointwise, then it converges to the same map in norm. This lemma is used to prove that the space of continuous linear maps is complete provided that the codomain is a complete space.
@[protected, instance]
def
continuous_linear_map.complete_space
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{F : Type u_6}
[normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{E' : Type u_11}
[semi_normed_group E']
[normed_space 𝕜 E']
[ring_hom_isometric σ₁₂]
[complete_space F] :
complete_space (E' →SL[σ₁₂] F)
If the target space is complete, the space of continuous linear maps with its norm is also complete. This works also if the source space is seminormed.
theorem
continuous_linear_map.is_compact_closure_image_coe_of_bounded
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{F : Type u_6}
[normed_group F]
[nondiscrete_normed_field 𝕜]
[nondiscrete_normed_field 𝕜₂]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{E' : Type u_11}
[semi_normed_group E']
[normed_space 𝕜 E']
[ring_hom_isometric σ₁₂]
[proper_space F]
{s : set (E' →SL[σ₁₂] F)}
(hb : metric.bo