Operator norm on the space of continuous linear maps #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 seminormed_add_comm_group and we specialize to normed_add_comm_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 σ].
theorem
norm_image_of_norm_zero
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
{𝓕 : Type u_10}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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 nontrivially
normed. The continuity ensures boundedness on a ball of some radius ε. The nontriviality of the
norm 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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
(f : E →SL[σ₁₂] F) :
def
linear_isometry.to_span_singleton
(𝕜 : Type u_1)
(E : Type u_4)
[seminormed_add_comm_group E]
[nontrivially_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}
[seminormed_add_comm_group E]
[nontrivially_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}
[seminormed_add_comm_group E]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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_bound'
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
(f : E →SL[σ₁₂] F)
{M : ℝ}
(hMp : 0 ≤ M)
(hM : ∀ (x : E), ‖x‖ ≠ 0 → ‖⇑f x‖ ≤ M * ‖x‖) :
If one controls the norm of every A x, ‖x‖ ≠ 0, 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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
(f : E →SL[σ₁₂] F) :
theorem
continuous_linear_map.op_norm_nonneg
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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_le_of_unit_norm
{E : Type u_4}
{F : Type u_6}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[normed_space ℝ E]
[normed_space ℝ F]
{f : E →L[ℝ] F}
{C : ℝ}
(hC : 0 ≤ C)
(hf : ∀ (x : E), ‖x‖ = 1 → ‖⇑f x‖ ≤ C) :
For a continuous real linear map f, if one controls the norm of every f x, ‖x‖ = 1, then
one controls the norm of f.
theorem
continuous_linear_map.op_norm_add_le
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[nontrivially_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}
[seminormed_add_comm_group E]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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]
noncomputable
def
continuous_linear_map.tmp_seminormed_add_comm_group
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂] :
seminormed_add_comm_group (E →SL[σ₁₂] F)
Continuous linear maps themselves form a seminormed space with respect to
the operator norm. This is only a temporary definition because we want to replace the topology
with continuous_linear_map.topological_space to avoid diamond issues.
See Note [forgetful inheritance]
Equations
@[protected]
noncomputable
def
continuous_linear_map.tmp_pseudo_metric_space
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂] :
pseudo_metric_space (E →SL[σ₁₂] F)
The pseudo_metric_space structure on E →SL[σ₁₂] F coming from
continuous_linear_map.tmp_seminormed_add_comm_group.
See Note [forgetful inheritance]
@[protected]
noncomputable
def
continuous_linear_map.tmp_uniform_space
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂] :
uniform_space (E →SL[σ₁₂] F)
The uniform_space structure on E →SL[σ₁₂] F coming from
continuous_linear_map.tmp_seminormed_add_comm_group.
See Note [forgetful inheritance]
@[protected]
noncomputable
def
continuous_linear_map.tmp_topological_space
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂] :
topological_space (E →SL[σ₁₂] F)
The topological_space structure on E →SL[σ₁₂] F coming from
continuous_linear_map.tmp_seminormed_add_comm_group.
See Note [forgetful inheritance]
@[protected]
theorem
continuous_linear_map.tmp_topological_add_group
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂] :
topological_add_group (E →SL[σ₁₂] F)
@[protected]
theorem
continuous_linear_map.tmp_closed_ball_div_subset
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
{a b : ℝ}
(ha : 0 < a)
(hb : 0 < b) :
metric.closed_ball 0 (a / b) ⊆ {f : E →SL[σ₁₂] F | ∀ (x : E), x ∈ metric.closed_ball 0 b → ⇑f x ∈ metric.closed_ball 0 a}
@[protected]
theorem
continuous_linear_map.tmp_topology_eq
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂] :
@[protected]
theorem
continuous_linear_map.tmp_uniform_space_eq
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂] :
@[protected, instance]
noncomputable
def
continuous_linear_map.to_pseudo_metric_space
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂] :
pseudo_metric_space (E →SL[σ₁₂] F)
Equations
- continuous_linear_map.to_pseudo_metric_space = continuous_linear_map.tmp_pseudo_metric_space.replace_uniformity continuous_linear_map.to_pseudo_metric_space._proof_1
@[protected, instance]
noncomputable
def
continuous_linear_map.to_seminormed_add_comm_group
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂] :
seminormed_add_comm_group (E →SL[σ₁₂] F)
Continuous linear maps themselves form a seminormed space with respect to the operator norm.
Equations
- continuous_linear_map.to_seminormed_add_comm_group = {to_has_norm := seminormed_add_comm_group.to_has_norm continuous_linear_map.tmp_seminormed_add_comm_group, to_add_comm_group := continuous_linear_map.add_comm_group seminormed_add_comm_group.to_topological_add_group, to_pseudo_metric_space := continuous_linear_map.to_pseudo_metric_space _inst_17, dist_eq := _}
theorem
continuous_linear_map.nnnorm_def
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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_bound'
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
(f : E →SL[σ₁₂] F)
(M : nnreal)
(hM : ∀ (x : E), ‖x‖₊ ≠ 0 → ‖⇑f x‖₊ ≤ M * ‖x‖₊) :
If one controls the norm of every A x, ‖x‖₊ ≠ 0, then one controls the norm of A.
theorem
continuous_linear_map.op_nnnorm_le_of_unit_nnnorm
{E : Type u_4}
{F : Type u_6}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[normed_space ℝ E]
[normed_space ℝ F]
{f : E →L[ℝ] F}
{C : nnreal}
(hf : ∀ (x : E), ‖x‖₊ = 1 → ‖⇑f x‖₊ ≤ C) :
For a continuous real linear map f, if one controls the norm of every f x, ‖x‖₊ = 1, then
one controls the norm of f.
theorem
continuous_linear_map.op_nnnorm_le_of_lipschitz
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[seminormed_add_comm_group G]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[seminormed_add_comm_group G]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[nontrivially_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}
[seminormed_add_comm_group E]
[nontrivially_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 := seminormed_add_comm_group.to_has_norm continuous_linear_map.to_seminormed_add_comm_group, to_ring := {add := add_comm_group.add seminormed_add_comm_group.to_add_comm_group, add_assoc := _, zero := add_comm_group.zero seminormed_add_comm_group.to_add_comm_group, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul seminormed_add_comm_group.to_add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg seminormed_add_comm_group.to_add_comm_group, sub := add_comm_group.sub seminormed_add_comm_group.to_add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul seminormed_add_comm_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 := seminormed_add_comm_group.to_pseudo_metric_space continuous_linear_map.to_seminormed_add_comm_group, dist_eq := _, norm_mul := _}
@[protected, instance]
noncomputable
def
continuous_linear_map.to_normed_algebra
{𝕜 : Type u_1}
{E : Type u_4}
[seminormed_add_comm_group E]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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.exists_mul_lt_apply_of_lt_op_nnnorm
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
(f : E →SL[σ₁₂] F)
{r : nnreal}
(hr : r < ‖f‖₊) :
theorem
continuous_linear_map.exists_mul_lt_of_lt_op_norm
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
(f : E →SL[σ₁₂] F)
{r : ℝ}
(hr₀ : 0 ≤ r)
(hr : r < ‖f‖) :
theorem
continuous_linear_map.exists_lt_apply_of_lt_op_nnnorm
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_3}
{F : Type u_4}
[normed_add_comm_group E]
[seminormed_add_comm_group F]
[densely_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[ring_hom_isometric σ₁₂]
(f : E →SL[σ₁₂] F)
{r : nnreal}
(hr : r < ‖f‖₊) :
theorem
continuous_linear_map.exists_lt_apply_of_lt_op_norm
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_3}
{F : Type u_4}
[normed_add_comm_group E]
[seminormed_add_comm_group F]
[densely_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[ring_hom_isometric σ₁₂]
(f : E →SL[σ₁₂] F)
{r : ℝ}
(hr : r < ‖f‖) :
theorem
continuous_linear_map.Sup_unit_ball_eq_nnnorm
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_3}
{F : Type u_4}
[normed_add_comm_group E]
[seminormed_add_comm_group F]
[densely_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[ring_hom_isometric σ₁₂]
(f : E →SL[σ₁₂] F) :
has_Sup.Sup ((λ (x : E), ‖⇑f x‖₊) '' metric.ball 0 1) = ‖f‖₊
theorem
continuous_linear_map.Sup_unit_ball_eq_norm
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_3}
{F : Type u_4}
[normed_add_comm_group E]
[seminormed_add_comm_group F]
[densely_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[ring_hom_isometric σ₁₂]
(f : E →SL[σ₁₂] F) :
has_Sup.Sup ((λ (x : E), ‖⇑f x‖) '' metric.ball 0 1) = ‖f‖
theorem
continuous_linear_map.Sup_closed_unit_ball_eq_nnnorm
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_3}
{F : Type u_4}
[normed_add_comm_group E]
[seminormed_add_comm_group F]
[densely_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[ring_hom_isometric σ₁₂]
(f : E →SL[σ₁₂] F) :
has_Sup.Sup ((λ (x : E), ‖⇑f x‖₊) '' metric.closed_ball 0 1) = ‖f‖₊
theorem
continuous_linear_map.Sup_closed_unit_ball_eq_norm
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_3}
{F : Type u_4}
[normed_add_comm_group E]
[seminormed_add_comm_group F]
[densely_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[ring_hom_isometric σ₁₂]
(f : E →SL[σ₁₂] F) :
has_Sup.Sup ((λ (x : E), ‖⇑f x‖) '' metric.closed_ball 0 1) = ‖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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[seminormed_add_comm_group G]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[seminormed_add_comm_group G]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[seminormed_add_comm_group G]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group Fₗ]
[seminormed_add_comm_group Gₗ]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group Fₗ]
[seminormed_add_comm_group Gₗ]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group Fₗ]
[seminormed_add_comm_group Gₗ]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group F]
[seminormed_add_comm_group G]
[nontrivially_normed_field 𝕜₂]
[nontrivially_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}
[seminormed_add_comm_group F]
[seminormed_add_comm_group G]
[nontrivially_normed_field 𝕜₂]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[seminormed_add_comm_group G]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[seminormed_add_comm_group G]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[seminormed_add_comm_group G]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[seminormed_add_comm_group G]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[seminormed_add_comm_group G]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[seminormed_add_comm_group G]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[seminormed_add_comm_group G]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[seminormed_add_comm_group G]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[seminormed_add_comm_group G]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[seminormed_add_comm_group G]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[nontrivially_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)
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[seminormed_add_comm_group G]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[seminormed_add_comm_group G]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[seminormed_add_comm_group G]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[nontrivially_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)
[seminormed_add_comm_group E]
[seminormed_add_comm_group Fₗ]
[seminormed_add_comm_group Gₗ]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group Fₗ]
[seminormed_add_comm_group Gₗ]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group Fₗ]
[seminormed_add_comm_group Gₗ]
[nontrivially_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)
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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)
[seminormed_add_comm_group E]
[seminormed_add_comm_group Fₗ]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group Fₗ]
[nontrivially_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)
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[seminormed_add_comm_group G]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[nontrivially_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 _
theorem
continuous_linear_map.norm_compSL_le
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
(E : Type u_4)
(F : Type u_6)
(G : Type u_8)
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[seminormed_add_comm_group G]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[nontrivially_normed_field 𝕜₃]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[normed_space 𝕜₃ G]
(σ₁₂ : 𝕜 →+* 𝕜₂)
(σ₂₃ : 𝕜₂ →+* 𝕜₃)
{σ₁₃ : 𝕜 →+* 𝕜₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[ring_hom_isometric σ₂₃]
[ring_hom_isometric σ₁₃]
[ring_hom_isometric σ₁₂] :
‖continuous_linear_map.compSL E F G σ₁₂ σ₂₃‖ ≤ 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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[seminormed_add_comm_group G]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[seminormed_add_comm_group G]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[seminormed_add_comm_group G]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[nontrivially_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)
[seminormed_add_comm_group E]
[seminormed_add_comm_group Fₗ]
[seminormed_add_comm_group Gₗ]
[nontrivially_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 𝕜)
theorem
continuous_linear_map.norm_compL_le
(𝕜 : Type u_1)
(E : Type u_4)
(Fₗ : Type u_7)
(Gₗ : Type u_9)
[seminormed_add_comm_group E]
[seminormed_add_comm_group Fₗ]
[seminormed_add_comm_group Gₗ]
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ]
[normed_space 𝕜 Gₗ] :
‖continuous_linear_map.compL 𝕜 E Fₗ Gₗ‖ ≤ 1
@[simp]
theorem
continuous_linear_map.compL_apply
(𝕜 : Type u_1)
(E : Type u_4)
(Fₗ : Type u_7)
(Gₗ : Type u_9)
[seminormed_add_comm_group E]
[seminormed_add_comm_group Fₗ]
[seminormed_add_comm_group Gₗ]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group Eₗ]
[seminormed_add_comm_group Fₗ]
[seminormed_add_comm_group Gₗ]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group Eₗ]
[seminormed_add_comm_group Fₗ]
[seminormed_add_comm_group Gₗ]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group Eₗ]
[seminormed_add_comm_group Fₗ]
[seminormed_add_comm_group Gₗ]
[nontrivially_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
theorem
continuous_linear_map.norm_precompR_le
{𝕜 : Type u_1}
{E : Type u_4}
(Eₗ : Type u_5)
{Fₗ : Type u_7}
{Gₗ : Type u_9}
[seminormed_add_comm_group E]
[seminormed_add_comm_group Eₗ]
[seminormed_add_comm_group Fₗ]
[seminormed_add_comm_group Gₗ]
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Eₗ]
[normed_space 𝕜 Fₗ]
[normed_space 𝕜 Gₗ]
(L : E →L[𝕜] Fₗ →L[𝕜] Gₗ) :
theorem
continuous_linear_map.norm_precompL_le
{𝕜 : Type u_1}
{E : Type u_4}
(Eₗ : Type u_5)
{Fₗ : Type u_7}
{Gₗ : Type u_9}
[seminormed_add_comm_group E]
[seminormed_add_comm_group Eₗ]
[seminormed_add_comm_group Fₗ]
[seminormed_add_comm_group Gₗ]
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Eₗ]
[normed_space 𝕜 Fₗ]
[normed_space 𝕜 Gₗ]
(L : E →L[𝕜] Fₗ →L[𝕜] Gₗ) :
noncomputable
def
continuous_linear_map.prod_mapL
(𝕜 : Type u_1)
[nontrivially_normed_field 𝕜]
(M₁ : Type u₁)
[seminormed_add_comm_group M₁]
[normed_space 𝕜 M₁]
(M₂ : Type u₂)
[seminormed_add_comm_group M₂]
[normed_space 𝕜 M₂]
(M₃ : Type u₃)
[seminormed_add_comm_group M₃]
[normed_space 𝕜 M₃]
(M₄ : Type u₄)
[seminormed_add_comm_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)
[nontrivially_normed_field 𝕜]
{M₁ : Type u₁}
[seminormed_add_comm_group M₁]
[normed_space 𝕜 M₁]
{M₂ : Type u₂}
[seminormed_add_comm_group M₂]
[normed_space 𝕜 M₂]
{M₃ : Type u₃}
[seminormed_add_comm_group M₃]
[normed_space 𝕜 M₃]
{M₄ : Type u₄}
[seminormed_add_comm_group M₄]
[normed_space 𝕜 M₄]
(p : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄)) :
theorem
continuous.prod_mapL
(𝕜 : Type u_1)
[nontrivially_normed_field 𝕜]
{M₁ : Type u₁}
[seminormed_add_comm_group M₁]
[normed_space 𝕜 M₁]
{M₂ : Type u₂}
[seminormed_add_comm_group M₂]
[normed_space 𝕜 M₂]
{M₃ : Type u₃}
[seminormed_add_comm_group M₃]
[normed_space 𝕜 M₃]
{M₄ : Type u₄}
[seminormed_add_comm_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)
[nontrivially_normed_field 𝕜]
{M₁ : Type u₁}
[seminormed_add_comm_group M₁]
[normed_space 𝕜 M₁]
{M₂ : Type u₂}
[seminormed_add_comm_group M₂]
[normed_space 𝕜 M₂]
{M₃ : Type u₃}
[seminormed_add_comm_group M₃]
[normed_space 𝕜 M₃]
{M₄ : Type u₄}
[seminormed_add_comm_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)
[nontrivially_normed_field 𝕜]
{M₁ : Type u₁}
[seminormed_add_comm_group M₁]
[normed_space 𝕜 M₁]
{M₂ : Type u₂}
[seminormed_add_comm_group M₂]
[normed_space 𝕜 M₂]
{M₃ : Type u₃}
[seminormed_add_comm_group M₃]
[normed_space 𝕜 M₃]
{M₄ : Type u₄}
[seminormed_add_comm_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)
[nontrivially_normed_field 𝕜]
{M₁ : Type u₁}
[seminormed_add_comm_group M₁]
[normed_space 𝕜 M₁]
{M₂ : Type u₂}
[seminormed_add_comm_group M₂]
[normed_space 𝕜 M₂]
{M₃ : Type u₃}
[seminormed_add_comm_group M₃]
[normed_space 𝕜 M₃]
{M₄ : Type u₄}
[seminormed_add_comm_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.mul
(𝕜 : Type u_1)
[nontrivially_normed_field 𝕜]
(𝕜' : Type u_11)
[non_unital_semi_normed_ring 𝕜']
[normed_space 𝕜 𝕜']
[is_scalar_tower 𝕜 𝕜' 𝕜']
[smul_comm_class 𝕜 𝕜' 𝕜'] :
Multiplication in a non-unital normed algebra as a continuous bilinear map.
Equations
- continuous_linear_map.mul 𝕜 𝕜' = (linear_map.mul 𝕜 𝕜').mk_continuous₂ 1 _
@[simp]
theorem
continuous_linear_map.mul_apply'
(𝕜 : Type u_1)
[nontrivially_normed_field 𝕜]
(𝕜' : Type u_11)
[non_unital_semi_normed_ring 𝕜']
[normed_space 𝕜 𝕜']
[is_scalar_tower 𝕜 𝕜' 𝕜']
[smul_comm_class 𝕜 𝕜' 𝕜']
(x y : 𝕜') :
⇑(⇑(continuous_linear_map.mul 𝕜 𝕜') x) y = x * y
@[simp]
theorem
continuous_linear_map.op_norm_mul_apply_le
(𝕜 : Type u_1)
[nontrivially_normed_field 𝕜]
(𝕜' : Type u_11)
[non_unital_semi_normed_ring 𝕜']
[normed_space 𝕜 𝕜']
[is_scalar_tower 𝕜 𝕜' 𝕜']
[smul_comm_class 𝕜 𝕜' 𝕜']
(x : 𝕜') :
theorem
continuous_linear_map.op_norm_mul_le
(𝕜 : Type u_1)
[nontrivially_normed_field 𝕜]
(𝕜' : Type u_11)
[non_unital_semi_normed_ring 𝕜']
[normed_space 𝕜 𝕜']
[is_scalar_tower 𝕜 𝕜' 𝕜']
[smul_comm_class 𝕜 𝕜' 𝕜'] :
‖continuous_linear_map.mul 𝕜 𝕜'‖ ≤ 1
noncomputable
def
continuous_linear_map.mul_left_right
(𝕜 : Type u_1)
[nontrivially_normed_field 𝕜]
(𝕜' : Type u_11)
[non_unital_semi_normed_ring 𝕜']
[normed_space 𝕜 𝕜']
[is_scalar_tower 𝕜 𝕜' 𝕜']
[smul_comm_class 𝕜 𝕜' 𝕜'] :
Simultaneous left- and right-multiplication in a non-unital normed algebra, considered as a
continuous trilinear map. This is akin to its non-continuous version linear_map.mul_left_right,
but there is a minor difference: linear_map.mul_left_right is uncurried.
Equations
- continuous_linear_map.mul_left_right 𝕜 𝕜' = ((continuous_linear_map.compL 𝕜 𝕜' 𝕜' 𝕜').comp (continuous_linear_map.mul 𝕜 𝕜').flip).flip.comp (continuous_linear_map.mul 𝕜 𝕜')
@[simp]
theorem
continuous_linear_map.mul_left_right_apply
(𝕜 : Type u_1)
[nontrivially_normed_field 𝕜]
(𝕜' : Type u_11)
[non_unital_semi_normed_ring 𝕜']
[normed_space 𝕜 𝕜']
[is_scalar_tower 𝕜 𝕜' 𝕜']
[smul_comm_class 𝕜 𝕜' 𝕜']
(x y z : 𝕜') :
theorem
continuous_linear_map.op_norm_mul_left_right_apply_apply_le
(𝕜 : Type u_1)
[nontrivially_normed_field 𝕜]
(𝕜' : Type u_11)
[non_unital_semi_normed_ring 𝕜']
[normed_space 𝕜 𝕜']
[is_scalar_tower 𝕜 𝕜' 𝕜']
[smul_comm_class 𝕜 𝕜' 𝕜']
(x y : 𝕜') :
theorem
continuous_linear_map.op_norm_mul_left_right_apply_le
(𝕜 : Type u_1)
[nontrivially_normed_field 𝕜]
(𝕜' : Type u_11)
[non_unital_semi_normed_ring 𝕜']
[normed_space 𝕜 𝕜']
[is_scalar_tower 𝕜 𝕜' 𝕜']
[smul_comm_class 𝕜 𝕜' 𝕜']
(x : 𝕜') :
theorem
continuous_linear_map.op_norm_mul_left_right_le
(𝕜 : Type u_1)
[nontrivially_normed_field 𝕜]
(𝕜' : Type u_11)
[non_unital_semi_normed_ring 𝕜']
[normed_space 𝕜 𝕜']
[is_scalar_tower 𝕜 𝕜' 𝕜']
[smul_comm_class 𝕜 𝕜' 𝕜'] :
noncomputable
def
continuous_linear_map.mulₗᵢ
(𝕜 : Type u_1)
[nontrivially_normed_field 𝕜]
(𝕜' : Type u_11)
[semi_normed_ring 𝕜']
[normed_algebra 𝕜 𝕜']
[norm_one_class 𝕜'] :
Multiplication in a normed algebra as a linear isometry to the space of continuous linear maps.
Equations
- continuous_linear_map.mulₗᵢ 𝕜 𝕜' = {to_linear_map := ↑(continuous_linear_map.mul 𝕜 𝕜'), norm_map' := _}
@[simp]
theorem
continuous_linear_map.coe_mulₗᵢ
(𝕜 : Type u_1)
[nontrivially_normed_field 𝕜]
(𝕜' : Type u_11)
[semi_normed_ring 𝕜']
[normed_algebra 𝕜 𝕜']
[norm_one_class 𝕜'] :
⇑(continuous_linear_map.mulₗᵢ 𝕜 𝕜') = ⇑(continuous_linear_map.mul 𝕜 𝕜')
@[simp]
theorem
continuous_linear_map.op_norm_mul_apply
(𝕜 : Type u_1)
[nontrivially_normed_field 𝕜]
(𝕜' : Type u_11)
[semi_normed_ring 𝕜']
[normed_algebra 𝕜 𝕜']
[norm_one_class 𝕜']
(x : 𝕜') :
noncomputable
def
continuous_linear_map.lsmul
(𝕜 : Type u_1)
{E : Type u_4}
[seminormed_add_comm_group E]
[nontrivially_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}
[seminormed_add_comm_group E]
[nontrivially_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}
[seminormed_add_comm_group E]
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 E]
(x : E) :
theorem
continuous_linear_map.op_norm_lsmul_apply_le
{𝕜 : Type u_1}
{E : Type u_4}
[seminormed_add_comm_group E]
[nontrivially_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}
[seminormed_add_comm_group E]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group Fₗ]
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ]
{𝕜' : Type u_11}
[nontrivially_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)
[seminormed_add_comm_group E]
[seminormed_add_comm_group Fₗ]
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ]
(𝕜' : Type u_11)
[nontrivially_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ₗ 𝕜' 𝕜'' seminormed_add_comm_group.to_topological_add_group, norm_map' := _}
@[simp]
theorem
continuous_linear_map.coe_restrict_scalars_isometry
{𝕜 : Type u_1}
{E : Type u_4}
{Fₗ : Type u_7}
[seminormed_add_comm_group E]
[seminormed_add_comm_group Fₗ]
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ]
{𝕜' : Type u_11}
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group Fₗ]
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ]
{𝕜' : Type u_11}
[nontrivially_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)
[seminormed_add_comm_group E]
[seminormed_add_comm_group Fₗ]
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ]
(𝕜' : Type u_11)
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group Fₗ]
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ]
{𝕜' : Type u_11}
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group Fₗ]
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ]
{𝕜' : Type u_11}
[nontrivially_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}
[seminormed_add_comm_group E]
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 E]
(K : submodule 𝕜 E) :
@[protected]
theorem
continuous_linear_equiv.lipschitz
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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.is_O_comp_rev
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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) :
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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[seminormed_add_comm_group G]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[nontrivially_normed_field 𝕜₃]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[normed_space 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
{E' : Type u_11}
{F' : Type u_12}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
{𝕜₁' : Type u_13}
{𝕜₂' : Type u_14}
[nontrivially_normed_field 𝕜₁']
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group F]
[seminormed_add_comm_group G]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[nontrivially_normed_field 𝕜₃]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[normed_space 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
{E' : Type u_11}
{F' : Type u_12}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
{𝕜₁' : Type u_13}
{𝕜₂' : Type u_14}
[nontrivially_normed_field 𝕜₁']
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group Fₗ]
[seminormed_add_comm_group Gₗ]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group Fₗ]
[seminormed_add_comm_group Gₗ]
[nontrivially_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}
[seminormed_add_comm_group E]
[seminormed_add_comm_group Fₗ]
[seminormed_add_comm_group Gₗ]
[nontrivially_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_add_comm_group E]
[normed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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_add_comm_group E]
[normed_add_comm_group Fₗ]
[nontrivially_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
linear_map.antilipschitz_of_comap_nhds_le
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[normed_add_comm_group E]
[normed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[h : ring_hom_isometric σ₁₂]
(f : E →ₛₗ[σ₁₂] F)
(hf : filter.comap ⇑f (nhds 0) ≤ nhds 0) :
∃ (K : nnreal), antilipschitz_with K ⇑f
theorem
continuous_linear_map.op_norm_zero_iff
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[normed_add_comm_group E]
[normed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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_add_comm_group E]
[nontrivially_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_add_comm_group E]
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 E]
[nontrivial E] :
norm_one_class (E →L[𝕜] E)
@[protected, instance]
noncomputable
def
continuous_linear_map.to_normed_add_comm_group
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[normed_add_comm_group E]
[normed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂] :
normed_add_comm_group (E →SL[σ₁₂] F)
Continuous linear maps themselves form a normed space with respect to the operator norm.
Equations
- continuous_linear_map.to_normed_add_comm_group = normed_add_comm_group.of_separation continuous_linear_map.to_normed_add_comm_group._proof_1
@[protected, instance]
noncomputable
def
continuous_linear_map.to_normed_ring
{𝕜 : Type u_1}
{E : Type u_4}
[normed_add_comm_group E]
[nontrivially_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_add_comm_group.to_has_norm continuous_linear_map.to_normed_add_comm_group, to_ring := semi_normed_ring.to_ring continuous_linear_map.to_semi_normed_ring, to_metric_space := normed_add_comm_group.to_metric_space continuous_linear_map.to_normed_add_comm_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_add_comm_group E]
[normed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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.antilipschitz_of_embedding
{𝕜 : Type u_1}
{E : Type u_4}
{Fₗ : Type u_7}
[normed_add_comm_group E]
[normed_add_comm_group Fₗ]
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ]
(f : E →L[𝕜] Fₗ)
(hf : embedding ⇑f) :
∃ (K : nnreal), antilipschitz_with K ⇑f
If a continuous linear map is a topology 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_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{E' : Type u_11}
[seminormed_add_comm_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_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{E' : Type u_11}
[seminormed_add_comm_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_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{E' : Type u_11}
[seminormed_add_comm_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_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{E' : Type u_11}
[seminormed_add_comm_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_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{E' : Type u_11}
[seminormed_add_comm_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_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{E' : Type u_11}
[seminormed_add_comm_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_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{E' : Type u_11}
[seminormed_add_comm_group E']
[normed_space 𝕜 E']
[ring_hom_isometric σ₁₂]
[proper_space F]
{s : set (E' →SL[σ₁₂] F)}
(hb : metric.bounded s) :
is_compact (closure (coe_fn '' s))
Let s be a bounded set in the space of continuous (semi)linear maps E →SL[σ] F taking values
in a proper space. Then s interpreted as a set in the space of maps E → F with topology of
pointwise convergence is precompact: its closure is a compact set.
theorem
continuous_linear_map.is_compact_image_coe_of_bounded_of_closed_image
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{F : Type u_6}
[normed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{E' : Type u_11}
[seminormed_add_comm_group E']
[normed_space 𝕜 E']
[ring_hom_isometric σ₁₂]
[proper_space F]
{s : set (E' →SL[σ₁₂] F)}
(hb : metric.bounded s)
(hc : is_closed (coe_fn '' s)) :
is_compact (coe_fn '' s)
Let s be a bounded set in the space of continuous (semi)linear maps E →SL[σ] F taking values
in a proper space. If s interpreted as a set in the space of maps E → F with topology of
pointwise convergence is closed, then it is compact.
TODO: reformulate this in terms of a type synonym with the right topology.
theorem
continuous_linear_map.is_closed_image_coe_of_bounded_of_weak_closed
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{F : Type u_6}
[normed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{E' : Type u_11}
[seminormed_add_comm_group E']
[normed_space 𝕜 E']
[ring_hom_isometric σ₁₂]
{s : set (E' →SL[σ₁₂] F)}
(hb : metric.bounded s)
(hc : ∀ (f : E' →SL[σ₁₂] F), ⇑f ∈ closure (coe_fn '' s) → f ∈ s) :
If a set s of semilinear functions is bounded and is closed in the weak-* topology, then its
image under coercion to functions E → F is a closed set. We don't have a name for E →SL[σ] F
with weak-* topology in mathlib, so we use an equivalent condition (see is_closed_induced_iff').
TODO: reformulate this in terms of a type synonym with the right topology.
theorem
continuous_linear_map.is_compact_image_coe_of_bounded_of_weak_closed
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{F : Type u_6}
[normed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{E' : Type u_11}
[seminormed_add_comm_group E']
[normed_space 𝕜 E']
[ring_hom_isometric σ₁₂]
[proper_space F]
{s : set (E' →SL[σ₁₂] F)}
(hb : metric.bounded s)
(hc : ∀ (f : E' →SL[σ₁₂] F), ⇑f ∈ closure (coe_fn '' s) → f ∈ s) :
is_compact (coe_fn '' s)
If a set s of semilinear functions is bounded and is closed in the weak-* topology, then its
image under coercion to functions E → F is a compact set. We don't have a name for E →SL[σ] F
with weak-* topology in mathlib, so we use an equivalent condition (see is_closed_induced_iff').
theorem
continuous_linear_map.is_weak_closed_closed_ball
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{F : Type u_6}
[normed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{E' : Type u_11}
[seminormed_add_comm_group E']
[normed_space 𝕜 E']
[ring_hom_isometric σ₁₂]
(f₀ : E' →SL[σ₁₂] F)
(r : ℝ)
⦃f : E' →SL[σ₁₂] F⦄
(hf : ⇑f ∈ closure (coe_fn '' metric.closed_ball f₀ r)) :
f ∈ metric.closed_ball f₀ r
A closed ball is closed in the weak-* topology. We don't have a name for E →SL[σ] F with
weak-* topology in mathlib, so we use an equivalent condition (see is_closed_induced_iff').
theorem
continuous_linear_map.is_closed_image_coe_closed_ball
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[normed_add_comm_group E]
[normed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
(f₀ : E →SL[σ₁₂] F)
(r : ℝ) :
is_closed (coe_fn '' metric.closed_ball f₀ r)
The set of functions f : E → F that represent continuous linear maps f : E →SL[σ₁₂] F
at distance ≤ r from f₀ : E →SL[σ₁₂] F is closed in the topology of pointwise convergence.
This is one of the key steps in the proof of the Banach-Alaoglu theorem.
theorem
continuous_linear_map.is_compact_image_coe_closed_ball
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[normed_add_comm_group E]
[normed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
[proper_space F]
(f₀ : E →SL[σ₁₂] F)
(r : ℝ) :
is_compact (coe_fn '' metric.closed_ball f₀ r)
Banach-Alaoglu theorem. The set of functions f : E → F that represent continuous linear
maps f : E →SL[σ₁₂] F at distance ≤ r from f₀ : E →SL[σ₁₂] F is compact in the topology of
pointwise convergence. Other versions of this theorem can be found in
analysis.normed_space.weak_dual.
noncomputable
def
continuous_linear_map.extend
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
{Fₗ : Type u_7}
[normed_add_comm_group E]
[normed_add_comm_group F]
[normed_add_comm_group Fₗ]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[normed_space 𝕜 Fₗ]
{σ₁₂ : 𝕜 →+* 𝕜₂}
(f : E →SL[σ₁₂] F)
[complete_space F]
(e : E →L[𝕜] Fₗ)
(h_dense : dense_range ⇑e)
(h_e : uniform_inducing ⇑e) :
Extension of a continuous linear map f : E →SL[σ₁₂] F, with E a normed space and F a
complete normed space, along a uniform and dense embedding e : E →L[𝕜] Fₗ.
@[simp]
theorem
continuous_linear_map.extend_eq
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
{Fₗ : Type u_7}
[normed_add_comm_group E]
[normed_add_comm_group F]
[normed_add_comm_group Fₗ]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[normed_space 𝕜 Fₗ]
{σ₁₂ : 𝕜 →+* 𝕜₂}
(f : E →SL[σ₁₂] F)
[complete_space F]
(e : E →L[𝕜] Fₗ)
(h_dense : dense_range ⇑e)
(h_e : uniform_inducing ⇑e)
(x : E) :
theorem
continuous_linear_map.extend_unique
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
{Fₗ : Type u_7}
[normed_add_comm_group E]
[normed_add_comm_group F]
[normed_add_comm_group Fₗ]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[normed_space 𝕜 Fₗ]
{σ₁₂ : 𝕜 →+* 𝕜₂}
(f : E →SL[σ₁₂] F)
[complete_space F]
(e : E →L[𝕜] Fₗ)
(h_dense : dense_range ⇑e)
(h_e : uniform_inducing ⇑e)
(g : Fₗ →SL[σ₁₂] F)
(H : g.comp e = f) :
@[simp]
theorem
continuous_linear_map.extend_zero
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
{Fₗ : Type u_7}
[normed_add_comm_group E]
[normed_add_comm_group F]
[normed_add_comm_group Fₗ]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[normed_space 𝕜 Fₗ]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[complete_space F]
(e : E →L[𝕜] Fₗ)
(h_dense : dense_range ⇑e)
(h_e : uniform_inducing ⇑e) :
theorem
continuous_linear_map.op_norm_extend_le
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
{Fₗ : Type u_7}
[normed_add_comm_group E]
[normed_add_comm_group F]
[normed_add_comm_group Fₗ]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[normed_space 𝕜 Fₗ]
{σ₁₂ : 𝕜 →+* 𝕜₂}
(f : E →SL[σ₁₂] F)
[complete_space F]
(e : E →L[𝕜] Fₗ)
(h_dense : dense_range ⇑e)
{N : nnreal}
(h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖⇑e x‖)
[ring_hom_isometric σ₁₂] :
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‖.
@[simp]
theorem
linear_isometry.norm_to_continuous_linear_map
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[normed_add_comm_group E]
[normed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[nontrivial E]
[ring_hom_isometric σ₁₂]
(f : E →ₛₗᵢ[σ₁₂] F) :
theorem
linear_isometry.norm_to_continuous_linear_map_comp
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{E : Type u_4}
{F : Type u_6}
{G : Type u_8}
[normed_add_comm_group E]
[normed_add_comm_group F]
[normed_add_comm_group G]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[nontrivially_normed_field 𝕜₃]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
[normed_space 𝕜₃ G]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[ring_hom_isometric σ₁₂]
(f : F →ₛₗᵢ[σ₂₃] G)
{g : E →SL[σ₁₂] F} :
Postcomposition of a continuous linear map with a linear isometry preserves the operator norm.
theorem
continuous_linear_map.op_norm_comp_linear_isometry_equiv
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{F : Type u_6}
{G : Type u_8}
[normed_add_comm_group F]
[normed_add_comm_group G]
[nontrivially_normed_field 𝕜₂]
[nontrivially_normed_field 𝕜₃]
[normed_space 𝕜₂ F]
[normed_space 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{𝕜₂' : Type u_11}
[nontrivially_normed_field 𝕜₂']
{F' : Type u_12}
[normed_add_comm_group F']
[normed_space 𝕜₂' F']
{σ₂' : 𝕜₂' →+* 𝕜₂}
{σ₂'' : 𝕜₂ →+* 𝕜₂'}
{σ₂₃' : 𝕜₂' →+* 𝕜₃}
[ring_hom_inv_pair σ₂' σ₂'']
[ring_hom_inv_pair σ₂'' σ₂']
[ring_hom_comp_triple σ₂' σ₂₃ σ₂₃']
[ring_hom_comp_triple σ₂'' σ₂₃' σ₂₃]
[ring_hom_isometric σ₂₃]
[ring_hom_isometric σ₂']
[ring_hom_isometric σ₂'']
[ring_hom_isometric σ₂₃']
(f : F →SL[σ₂₃] G)
(g : F' ≃ₛₗᵢ[σ₂'] F) :
Precomposition with a linear isometry preserves the operator norm.
@[simp]
theorem
continuous_linear_map.norm_smul_right_apply
{𝕜 : Type u_1}
{E : Type u_4}
{Fₗ : Type u_7}
[normed_add_comm_group E]
[normed_add_comm_group Fₗ]
[nontrivially_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.
@[simp]
theorem
continuous_linear_map.nnnorm_smul_right_apply
{𝕜 : Type u_1}
{E : Type u_4}
{Fₗ : Type u_7}
[normed_add_comm_group E]
[normed_add_comm_group Fₗ]
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ]
(c : E →L[𝕜] 𝕜)
(f : Fₗ) :
The non-negative norm of the tensor product of a scalar linear map and of an element of a normed space is the product of the non-negative norms.
noncomputable
def
continuous_linear_map.smul_rightL
(𝕜 : Type u_1)
(E : Type u_4)
(Fₗ : Type u_7)
[normed_add_comm_group E]
[normed_add_comm_group Fₗ]
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ] :
continuous_linear_map.smul_right as a continuous trilinear map:
smul_rightL (c : E →L[𝕜] 𝕜) (f : F) (x : E) = c x • f.
Equations
- continuous_linear_map.smul_rightL 𝕜 E Fₗ = {to_fun := continuous_linear_map.smul_rightₗ _, map_add' := _, map_smul' := _}.mk_continuous₂ 1 _
@[simp]
theorem
continuous_linear_map.norm_smul_rightL_apply
{𝕜 : Type u_1}
{E : Type u_4}
{Fₗ : Type u_7}
[normed_add_comm_group E]
[normed_add_comm_group Fₗ]
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ]
(c : E →L[𝕜] 𝕜)
(f : Fₗ) :
@[simp]
theorem
continuous_linear_map.norm_smul_rightL
{𝕜 : Type u_1}
{E : Type u_4}
{Fₗ : Type u_7}
[normed_add_comm_group E]
[normed_add_comm_group Fₗ]
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 E]
[normed_space 𝕜 Fₗ]
(c : E →L[𝕜] 𝕜)
[nontrivial Fₗ] :
@[simp]
theorem
continuous_linear_map.op_norm_mul
(𝕜 : Type u_1)
[nontrivially_normed_field 𝕜]
(𝕜' : Type u_13)
[normed_ring 𝕜']
[normed_algebra 𝕜 𝕜']
[norm_one_class 𝕜'] :
‖continuous_linear_map.mul 𝕜 𝕜'‖ = 1
@[simp]
theorem
continuous_linear_map.op_norm_lsmul
(𝕜 : Type u_1)
{E : Type u_4}
[normed_add_comm_group E]
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 E]
(𝕜' : Type u_13)
[normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' E]
[is_scalar_tower 𝕜 𝕜' E]
[nontrivial E] :
‖continuous_linear_map.lsmul 𝕜 𝕜'‖ = 1
The norm of lsmul equals 1 in any nontrivial normed group.
This is continuous_linear_map.op_norm_lsmul_le as an equality.
theorem
submodule.norm_subtypeL
{𝕜 : Type u_1}
{E : Type u_4}
[normed_add_comm_group E]
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 E]
(K : submodule 𝕜 E)
[nontrivial ↥K] :
@[protected]
theorem
continuous_linear_equiv.antilipschitz
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[normed_add_comm_group E]
[normed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_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.one_le_norm_mul_norm_symm
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[normed_add_comm_group E]
[normed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{σ₂₁ : 𝕜₂ →+* 𝕜}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[ring_hom_isometric σ₂₁]
[ring_hom_isometric σ₁₂]
[nontrivial E]
(e : E ≃SL[σ₁₂] F) :
theorem
continuous_linear_equiv.norm_pos
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[normed_add_comm_group E]
[normed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{σ₂₁ : 𝕜₂ →+* 𝕜}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[ring_hom_isometric σ₂₁]
[ring_hom_isometric σ₁₂]
[nontrivial E]
(e : E ≃SL[σ₁₂] F) :
theorem
continuous_linear_equiv.norm_symm_pos
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[normed_add_comm_group E]
[normed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{σ₂₁ : 𝕜₂ →+* 𝕜}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[ring_hom_isometric σ₂₁]
[ring_hom_isometric σ₁₂]
[nontrivial E]
(e : E ≃SL[σ₁₂] F) :
theorem
continuous_linear_equiv.nnnorm_symm_pos
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[normed_add_comm_group E]
[normed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{σ₂₁ : 𝕜₂ →+* 𝕜}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[ring_hom_isometric σ₂₁]
[ring_hom_isometric σ₁₂]
[nontrivial E]
(e : E ≃SL[σ₁₂] F) :
theorem
continuous_linear_equiv.subsingleton_or_norm_symm_pos
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[normed_add_comm_group E]
[normed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{σ₂₁ : 𝕜₂ →+* 𝕜}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[ring_hom_isometric σ₂₁]
[ring_hom_isometric σ₁₂]
(e : E ≃SL[σ₁₂] F) :
theorem
continuous_linear_equiv.subsingleton_or_nnnorm_symm_pos
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_6}
[normed_add_comm_group E]
[normed_add_comm_group F]
[nontrivially_normed_field 𝕜]
[nontrivially_normed_field 𝕜₂]
[normed_space 𝕜 E]
[normed_space 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{σ₂₁ : 𝕜₂ →+* 𝕜}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[ring_hom_isometric σ₂₁]
[ring_hom_isometric σ₁₂]
(e : E ≃SL[σ₁₂] F) :
@[simp]
theorem
continuous_linear_equiv.coord_norm
(𝕜 : Type u_1)
{E : Type u_4}
[normed_add_comm_group E]
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 E]
(x : E)
(h : x ≠ 0) :
def
is_coercive
{E : Type u_4}
[normed_add_comm_group E]
[normed_space ℝ E]
(B : E →L[ℝ] E →L[ℝ] ℝ) :
Prop
A bounded bilinear form B in a real normed space is coercive
if there is some positive constant C such that C * ‖u‖ * ‖u‖ ≤ B u u.