mathlib3 documentation

analysis.normed_space.operator_norm

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) :
(C : ), 0 < C (x : E), f x C * x

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) :
(C : ), 0 < C (x : E), f x C * x
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) :
𝕜 →ₗᵢ[𝕜] E

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
@[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 : 𝕜) :
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.

Equations
@[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] {σ₁₂ : 𝕜 →+* 𝕜₂} :
has_norm (E →SL[σ₁₂] 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) :
f = has_Inf.Inf {c : | 0 c (x : E), f x c * x}
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} :
(c : ), c {c : | 0 c (x : E), f x c * x}
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} :
bdd_below {c : | 0 c (x : E), f x c * x}
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) :
φ = M
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) :
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.

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.

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 σ₁₂] :

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_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]

Equations
@[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 σ₁₂] :
@[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, 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 σ₁₂] :
Equations
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.

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

Continuous linear maps form a seminormed ring with respect to the operator norm.

Equations
@[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.

Equations
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) :
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) :
lipschitz_with x‖₊ (λ (f : E →SL[σ₁₂] F), f x)

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‖₊) :
(x : E), r * x‖₊ < f x‖₊
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) :
(x : E), r * x < f x
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‖₊) :
(x : E), x‖₊ < 1 r < f x‖₊
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) :
(x : E), x < 1 r < f x
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) :
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) :
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) :
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ₗ) :
f.prod g = (f, 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ₗ] :
(E →L[𝕜] Fₗ) × (E →L[𝕜] Gₗ) ≃ₗᵢ[R] E →L[𝕜] Fₗ × Gₗ

continuous_linear_map.prod as a linear_isometry_equiv.

Equations
@[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) :
f =O[l] λ (x : E), x
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 α) :
(λ (x' : α), g (f x')) =O[l] f
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) :
asymptotics.is_O_with f l (λ (x' : E), f (x' - x)) (λ (x' : E), x' - x)
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) :
(λ (x' : E), f (x' - x)) =O[l] λ (x' : E), x' - x
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) :

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

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) :
E →SL[σ₁₃] F →SL[σ₂₃] G

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
@[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) :
((f.mk_continuous₂ C hC) x) y = (f x) y
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) :
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) :
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) :
F →SL[σ₂₃] E →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
@[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) :
((f.flip) y) x = (f x) y
@[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) :
f.flip.flip = f
@[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) :
(f + g).flip = f.flip + g.flip
@[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) :
(c f).flip = c f.flip
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 σ₁₃] :
(E →SL[σ₁₃] F →SL[σ₂₃] G) ≃ₗᵢ[𝕜₃] F →SL[σ₂₃] E →SL[σ₁₃] 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
@[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 σ₁₃] :
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ₗ] :
(E →L[𝕜] Fₗ →L[𝕜] Gₗ) ≃ₗᵢ[𝕜] Fₗ →L[𝕜] E →L[𝕜] 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
@[simp]
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 σ₁₂] :
E →SL[σ₁₂] (E →SL[σ₁₂] F) →L[𝕜₂] 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
@[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) :
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ₗ] :
E →L[𝕜] (E →L[𝕜] Fₗ) →L[𝕜] 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
@[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ₗ) :
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 σ₁₂] :
(F →SL[σ₂₃] G) →L[𝕜₃] (E →SL[σ₁₂] F) →SL[σ₂₃] E →SL[σ₁₃] G

Composition of continuous semilinear maps as a continuous semibilinear map.

Equations
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ₗ] :
(Fₗ →L[𝕜] Gₗ) →L[𝕜] (E →L[𝕜] Fₗ) →L[𝕜] E →L[𝕜] Gₗ

Composition of continuous linear maps as a continuous bilinear map.

Equations
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ₗ] :
@[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ₗ) :
E →L[𝕜] (Eₗ →L[𝕜] Fₗ) →L[𝕜] Eₗ →L[𝕜] Gₗ

Apply L(x,-) pointwise to bilinear maps, as a continuous bilinear map

Equations
@[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ₗ) :
(Eₗ →L[𝕜] E) →L[𝕜] Fₗ →L[𝕜] Eₗ →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₄] :
(M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄

continuous_linear_map.prod_map as a continuous linear map.

Equations
@[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₄)) :
(continuous_linear_map.prod_mapL 𝕜 M₁ M₂ M₃ M₄) p = p.fst.prod_map p.snd
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 𝕜 𝕜' 𝕜'] :
𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜'

Multiplication in a non-unital normed algebra as a continuous bilinear map.

Equations
@[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 𝕜 𝕜' 𝕜'] :
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 𝕜 𝕜' 𝕜'] :
𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜'

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
@[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 : 𝕜') :
(((continuous_linear_map.mul_left_right 𝕜 𝕜') x) y) z = x * z * y
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 : 𝕜') :
noncomputable def continuous_linear_map.mulₗᵢ (𝕜 : Type u_1) [nontrivially_normed_field 𝕜] (𝕜' : Type u_11) [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] [norm_one_class 𝕜'] :
𝕜' →ₗᵢ[𝕜] 𝕜' →L[𝕜] 𝕜'

Multiplication in a normed algebra as a linear isometry to the space of continuous linear maps.

Equations
@[simp]
@[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] :
𝕜' →L[𝕜] E →L[𝕜] E

Scalar multiplication as a continuous bilinear map.

Equations
@[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.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] :

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ₗ] :
(E →L[𝕜] Fₗ) →ₗᵢ[𝕜''] E →L[𝕜'] Fₗ

continuous_linear_map.restrict_scalars as a linear_isometry.

Equations
@[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ₗ] :
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ₗ] :
(E →L[𝕜] Fₗ) →L[𝕜''] E →L[𝕜'] Fₗ

continuous_linear_map.restrict_scalars as a continuous_linear_map.

Equations
@[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ₗ] :
@[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ₗ] :
@[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 α) :
(λ (x' : α), e (f x')) =O[l] f
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) :
(λ (x' : E), e (x' - x)) =O[l] λ (x' : E), x' - x
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 α) :
f =O[l] λ (x' : α), e (f x')
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) :
(λ (x' : E), x' - x) =O[l] λ (x' : E), e (x' - x)
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) :
E' →SL[σ₁₃'] F' →SL[σ₂₃'] G

Compose a bilinear map E →SL[σ₁₃] F →SL[σ₂₃] G with two linear maps E' →SL[σ₁'] E and F' →SL[σ₂'] F.

Equations
@[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') :
((f.bilinear_comp gE gF) x) y = (f (gE x)) (gF y)
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ₗ) :
E × Fₗ →L[𝕜] E × 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
@[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ₗ) :
((f.deriv₂) p) = λ (q : E × Fₗ), (f p.fst) q.snd + (f q.fst) p.snd
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ₗ) :
(f (x + x')) (y + y') = (f x) y + ((f.deriv₂) (x, y)) (x', y') + (f x') y'
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) :
(C : ), (z : E), f z C * z

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) :
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 σ₁₂] :
f = 0 f = 0

An operator is zero iff its norm vanishes.

@[simp]

If a normed space is non-trivial, then the norm of the identity equals 1.

@[protected, instance]
@[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 σ₁₂] :

Continuous linear maps themselves form a normed space with respect to the operator norm.

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

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)) :
E' →SL[σ₁₂] F

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.

Equations
@[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)) :
E' →SL[σ₁₂] F

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

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

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

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

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

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

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

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) :
Fₗ →SL[σ₁₂] F

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ₗ.

Equations
@[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) :
(f.extend e h_dense h_e) (e x) = f x
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) :
f.extend e h_dense h_e = g
@[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) :
0.extend e h_dense h_e = 0
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 σ₁₂] :
f.extend e h_dense _ N * f

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ₗ] :
(E →L[𝕜] 𝕜) →L[𝕜] Fₗ →L[𝕜] E →L[𝕜] Fₗ

continuous_linear_map.smul_right as a continuous trilinear map: smul_rightL (c : E →L[𝕜] 𝕜) (f : F) (x : E) = c x • f.

Equations
@[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 𝕜'] :
@[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] :

The norm of lsmul equals 1 in any nontrivial normed group.

This is continuous_linear_map.op_norm_lsmul_le as an equality.

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

Equations