mathlib documentation

analysis.normed_space.operator_norm

Operator norm on the space of continuous linear maps #

Define the operator norm on the space of continuous linear maps between normed spaces, and prove its basic properties. In particular, show that this space is itself a normed space.

Since a lot of elementary properties don't require ∥x∥ = 0 → x = 0 we start setting up the theory for semi_normed_space and we specialize to normed_space at the end.

Most statements in this file require the field to be non-discrete, as this is necessary to deduce an inequality ∥f x∥ ≤ C ∥x∥ from the continuity of f. However, the other direction always holds. In this section, we just assume that 𝕜 is a normed field. In the remainder of the file, it will be non-discrete.

theorem linear_map.lipschitz_of_bound {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →ₗ[𝕜] F) (C : ) (h : ∀ (x : E), f x C * x) :
theorem linear_map.lipschitz_of_bound_nnnorm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →ₗ[𝕜] F) (C : ℝ≥0) (h : ∀ (x : E), f x∥₊ C * x∥₊) :
theorem linear_map.antilipschitz_of_bound {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →ₗ[𝕜] F) {K : ℝ≥0} (h : ∀ (x : E), x (K) * f x) :
theorem linear_map.bound_of_antilipschitz {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →ₗ[𝕜] F) {K : ℝ≥0} (h : antilipschitz_with K f) (x : E) :
theorem linear_map.uniform_continuous_of_bound {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →ₗ[𝕜] F) (C : ) (h : ∀ (x : E), f x C * x) :
theorem linear_map.continuous_of_bound {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →ₗ[𝕜] F) (C : ) (h : ∀ (x : E), f x C * x) :
def linear_map.mk_continuous {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →ₗ[𝕜] F) (C : ) (h : ∀ (x : E), f x C * x) :
E →L[𝕜] F

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

Equations
def linear_map.to_continuous_linear_map₁ {𝕜 : Type u_1} {E : Type u_2} [semi_normed_group E] [normed_field 𝕜] [semi_normed_space 𝕜 E] (f : 𝕜 →ₗ[𝕜] E) :
𝕜 →L[𝕜] E

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

Equations
def linear_map.mk_continuous_of_exists_bound {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →ₗ[𝕜] F) (h : ∃ (C : ), ∀ (x : E), f x C * x) :
E →L[𝕜] F

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

Equations
theorem continuous_of_linear_of_bound {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] {f : E → F} (h_add : ∀ (x y : E), f (x + y) = f x + f y) (h_smul : ∀ (c : 𝕜) (x : E), f (c x) = c f x) {C : } (h_bound : ∀ (x : E), f x C * x) :
@[simp]
theorem linear_map.mk_continuous_coe {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →ₗ[𝕜] F) (C : ) (h : ∀ (x : E), f x C * x) :
@[simp]
theorem linear_map.mk_continuous_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →ₗ[𝕜] F) (C : ) (h : ∀ (x : E), f x C * x) (x : E) :
(f.mk_continuous C h) x = f x
@[simp]
theorem linear_map.mk_continuous_of_exists_bound_coe {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →ₗ[𝕜] F) (h : ∃ (C : ), ∀ (x : E), f x C * x) :
@[simp]
theorem linear_map.mk_continuous_of_exists_bound_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →ₗ[𝕜] F) (h : ∃ (C : ), ∀ (x : E), f x C * x) (x : E) :
@[simp]
theorem linear_map.to_continuous_linear_map₁_coe {𝕜 : Type u_1} {E : Type u_2} [semi_normed_group E] [normed_field 𝕜] [semi_normed_space 𝕜 E] (f : 𝕜 →ₗ[𝕜] E) :
@[simp]
theorem linear_map.to_continuous_linear_map₁_apply {𝕜 : Type u_1} {E : Type u_2} [semi_normed_group E] [normed_field 𝕜] [semi_normed_space 𝕜 E] (f : 𝕜 →ₗ[𝕜] E) (x : 𝕜) :
theorem linear_map.bound_of_shell_semi_normed {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →ₗ[𝕜] F) {ε C : } (ε_pos : 0 < ε) {c : 𝕜} (hc : 1 < c) (hf : ∀ (x : E), ε / c xx < εf x C * x) {x : E} (hx : x 0) :
theorem norm_image_of_norm_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] {f : E →ₗ[𝕜] F} (hf : continuous f) {x : E} (hx : x = 0) :

If ∥x∥ = 0 and f is continuous then ∥f x∥ = 0.

theorem linear_map.bound_of_continuous {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →ₗ[𝕜] 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 nondiscrete. The continuity ensures boundedness on a ball of some radius ε. The nondiscreteness is then used to rescale any element into an element of norm in [ε/C, ε], whose image has a controlled norm. The norm control for the original element follows by rescaling.

theorem continuous_linear_map.bound {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →L[𝕜] F) :
∃ (C : ), 0 < C ∀ (x : E), f x C * x
def continuous_linear_map.of_homothety {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →ₗ[𝕜] F) (a : ) (hf : ∀ (x : E), f x = a * x) :
E →L[𝕜] F

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

Equations
def continuous_linear_map.to_span_singleton (𝕜 : Type u_1) {E : Type u_2} [semi_normed_group E] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] (x : E) :
𝕜 →L[𝕜] E

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

Equations
theorem continuous_linear_map.to_span_singleton_apply (𝕜 : Type u_1) {E : Type u_2} [semi_normed_group E] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] (x : E) (r : 𝕜) :
theorem continuous_linear_map.to_span_singleton_smul' (𝕜 : Type u_1) {E : Type u_2} [semi_normed_group E] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] (𝕜' : Type u_3) [nondiscrete_normed_field 𝕜'] [semi_normed_space 𝕜' E] [smul_comm_class 𝕜 𝕜' E] (c : 𝕜') (x : E) :
def continuous_linear_map.op_norm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →L[𝕜] F) :

The operator norm of a continuous linear map is the inf of all its bounds.

Equations
@[instance]
def continuous_linear_map.has_op_norm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] :
has_norm (E →L[𝕜] F)
Equations
theorem continuous_linear_map.norm_def {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →L[𝕜] F) :
f = Inf {c : | 0 c ∀ (x : E), f x c * x}
theorem continuous_linear_map.bounds_nonempty {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] {f : E →L[𝕜] F} :
∃ (c : ), c {c : | 0 c ∀ (x : E), f x c * x}
theorem continuous_linear_map.bounds_bdd_below {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] {f : E →L[𝕜] F} :
bdd_below {c : | 0 c ∀ (x : E), f x c * x}
theorem continuous_linear_map.op_norm_nonneg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →L[𝕜] F) :
theorem continuous_linear_map.le_op_norm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →L[𝕜] F) (x : E) :

The fundamental property of the operator norm: ∥f x∥ ≤ ∥f∥ * ∥x∥.

theorem continuous_linear_map.le_op_norm_of_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →L[𝕜] F) {c : } {x : E} (h : x c) :
theorem continuous_linear_map.le_of_op_norm_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →L[𝕜] F) {c : } (h : f c) (x : E) :
theorem continuous_linear_map.ratio_le_op_norm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →L[𝕜] F) (x : E) :
theorem continuous_linear_map.unit_le_op_norm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →L[𝕜] F) (x : E) :

The image of the unit ball under a continuous linear map is bounded.

theorem continuous_linear_map.op_norm_le_bound {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →L[𝕜] F) {M : } (hMp : 0 M) (hM : ∀ (x : E), f x M * x) :

If one controls the norm of every A x, then one controls the norm of A.

theorem continuous_linear_map.op_norm_le_of_lipschitz {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] {f : E →L[𝕜] F} {K : ℝ≥0} (hf : lipschitz_with K f) :
theorem continuous_linear_map.op_norm_le_of_shell {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] {f : E →L[𝕜] F} {ε C : } (ε_pos : 0 < ε) (hC : 0 C) {c : 𝕜} (hc : 1 < c) (hf : ∀ (x : E), ε / c xx < εf x C * x) :
theorem continuous_linear_map.op_norm_le_of_ball {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] {f : E →L[𝕜] 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} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] {f : E →L[𝕜] F} {C : } (hC : 0 C) (hf : ∀ᶠ (x : E) in 𝓝 0, f x C * x) :
theorem continuous_linear_map.op_norm_le_of_shell' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] {f : E →L[𝕜] F} {ε C : } (ε_pos : 0 < ε) (hC : 0 C) {c : 𝕜} (hc : c < 1) (hf : ∀ (x : E), ε * c xx < εf x C * x) :
theorem continuous_linear_map.op_norm_eq_of_bounds {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] {φ : E →L[𝕜] 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_add_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f g : E →L[𝕜] F) :

The operator norm satisfies the triangle inequality.

theorem continuous_linear_map.op_norm_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] :

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.

theorem continuous_linear_map.norm_id_of_nontrivial_seminorm {𝕜 : Type u_1} {E : Type u_2} [semi_normed_group E] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] (h : ∃ (x : E), x 0) :

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} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] {𝕜' : Type u_4} [normed_field 𝕜'] [semi_normed_space 𝕜' F] [smul_comm_class 𝕜 𝕜' F] (c : 𝕜') (f : E →L[𝕜] F) :
theorem continuous_linear_map.op_norm_neg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →L[𝕜] F) :
@[instance]
def continuous_linear_map.to_semi_normed_group {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] :

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

Equations
@[instance]
def continuous_linear_map.to_semi_normed_space {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] {𝕜' : Type u_4} [normed_field 𝕜'] [semi_normed_space 𝕜' F] [smul_comm_class 𝕜 𝕜' F] :
semi_normed_space 𝕜' (E →L[𝕜] F)
Equations
theorem continuous_linear_map.op_norm_comp_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] [semi_normed_space 𝕜 G] (h : F →L[𝕜] G) (f : E →L[𝕜] F) :

The operator norm is submultiplicative.

theorem continuous_linear_map.le_op_nnnorm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →L[𝕜] F) (x : E) :
theorem continuous_linear_map.lipschitz {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →L[𝕜] F) :

continuous linear maps are Lipschitz continuous.

theorem continuous_linear_map.le_op_norm₂ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] [semi_normed_space 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) (x : E) (y : F) :
theorem continuous_linear_map.op_norm_le_bound₂ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] [semi_normed_space 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) {C : } (h0 : 0 C) (hC : ∀ (x : E) (y : F), (f x) y (C * x) * y) :
@[simp]
theorem continuous_linear_map.op_norm_prod {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] [semi_normed_space 𝕜 G] (f : E →L[𝕜] F) (g : E →L[𝕜] G) :
f.prod g = (f, g)
def continuous_linear_map.prodₗᵢ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] [semi_normed_space 𝕜 G] (R : Type u_5) [ring R] [topological_space R] [module R F] [module R G] [has_continuous_smul R F] [has_continuous_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
theorem continuous_linear_map.uniform_continuous {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →L[𝕜] F) :

A continuous linear map is automatically uniformly continuous.

@[simp]
theorem continuous_linear_map.op_norm_subsingleton {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →L[𝕜] F) [subsingleton E] :
theorem continuous_linear_map.isometry_iff_norm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →L[𝕜] F) :
isometry f ∀ (x : E), f x = x

A continuous linear map is an isometry if and only if it preserves the norm. (Note: Do you really want to use this lemma? Try using the bundled structure linear_isometry instead.)

theorem continuous_linear_map.is_O_with_id {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →L[𝕜] F) (l : filter E) :
asymptotics.is_O_with f f (λ (x : E), x) l
theorem continuous_linear_map.is_O_id {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →L[𝕜] F) (l : filter E) :
asymptotics.is_O f (λ (x : E), x) l
theorem continuous_linear_map.is_O_with_comp {𝕜 : Type u_1} {F : Type u_3} {G : Type u_4} [semi_normed_group F] [semi_normed_group G] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 F] [semi_normed_space 𝕜 G] {α : Type u_2} (g : F →L[𝕜] G) (f : α → F) (l : filter α) :
asymptotics.is_O_with g (λ (x' : α), g (f x')) f l
theorem continuous_linear_map.is_O_comp {𝕜 : Type u_1} {F : Type u_3} {G : Type u_4} [semi_normed_group F] [semi_normed_group G] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 F] [semi_normed_space 𝕜 G] {α : Type u_2} (g : F →L[𝕜] G) (f : α → F) (l : filter α) :
asymptotics.is_O (λ (x' : α), g (f x')) f l
theorem continuous_linear_map.is_O_with_sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →L[𝕜] F) (l : filter E) (x : E) :
asymptotics.is_O_with f (λ (x' : E), f (x' - x)) (λ (x' : E), x' - x) l
theorem continuous_linear_map.is_O_sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E →L[𝕜] F) (l : filter E) (x : E) :
asymptotics.is_O (λ (x' : E), f (x' - x)) (λ (x' : E), x' - x) l
theorem linear_map.mk_continuous_norm_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_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} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_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.

def linear_map.mk_continuous₂ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] [semi_normed_space 𝕜 G] (f : E →ₗ[𝕜] F →ₗ[𝕜] G) (C : ) (hC : ∀ (x : E) (y : F), (f x) y (C * x) * y) :
E →L[𝕜] F →L[𝕜] 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} {E : Type u_2} {F : Type u_3} {G : Type u_4} [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] [semi_normed_space 𝕜 G] (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} {E : Type u_2} {F : Type u_3} {G : Type u_4} [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] [semi_normed_space 𝕜 G] (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} {E : Type u_2} {F : Type u_3} {G : Type u_4} [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] [semi_normed_space 𝕜 G] (f : E →ₗ[𝕜] F →ₗ[𝕜] G) {C : } (h0 : 0 C) (hC : ∀ (x : E) (y : F), (f x) y (C * x) * y) :
def continuous_linear_map.flip {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] [semi_normed_space 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) :
F →L[𝕜] E →L[𝕜] 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} {E : Type u_2} {F : Type u_3} {G : Type u_4} [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] [semi_normed_space 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) (x : E) (y : F) :
((f.flip) y) x = (f x) y
@[simp]
theorem continuous_linear_map.flip_flip {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] [semi_normed_space 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) :
f.flip.flip = f
@[simp]
theorem continuous_linear_map.op_norm_flip {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] [semi_normed_space 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) :
@[simp]
theorem continuous_linear_map.flip_add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] [semi_normed_space 𝕜 G] (f g : E →L[𝕜] F →L[𝕜] G) :
(f + g).flip = f.flip + g.flip
@[simp]
theorem continuous_linear_map.flip_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] [semi_normed_space 𝕜 G] (c : 𝕜) (f : E →L[𝕜] F →L[𝕜] G) :
(c f).flip = c f.flip
def continuous_linear_map.flipₗᵢ (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) (G : Type u_4) [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] [semi_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]
theorem continuous_linear_map.flipₗᵢ_symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] [semi_normed_space 𝕜 G] :
@[simp]
def continuous_linear_map.apply (𝕜 : Type u_1) {E : Type u_2} (F : Type u_3) [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] :
E →L[𝕜] (E →L[𝕜] F) →L[𝕜] F

The continuous linear map obtained by applying a continuous linear 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_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (v : E) (f : E →L[𝕜] F) :
def continuous_linear_map.compL (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) (G : Type u_4) [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] [semi_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
@[simp]
theorem continuous_linear_map.compL_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] [semi_normed_space 𝕜 G] (f : F →L[𝕜] G) (g : E →L[𝕜] F) :
def continuous_linear_map.lmulₗᵢ (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] (𝕜' : Type u_5) [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :
𝕜' →ₗᵢ[𝕜] 𝕜' →L[𝕜] 𝕜'

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

Equations
def continuous_linear_map.lmul (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] (𝕜' : Type u_5) [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :
𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜'

Left multiplication in a normed algebra as a continuous bilinear map.

Equations
@[simp]
theorem continuous_linear_map.lmul_apply (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] (𝕜' : Type u_5) [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] (x y : 𝕜') :
((continuous_linear_map.lmul 𝕜 𝕜') x) y = x * y
@[simp]
theorem continuous_linear_map.coe_lmulₗᵢ (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] (𝕜' : Type u_5) [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :
@[simp]
theorem continuous_linear_map.op_norm_lmul_apply (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] (𝕜' : Type u_5) [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] (x : 𝕜') :
def continuous_linear_map.lmul_right (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] (𝕜' : Type u_5) [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :
𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜'

Right-multiplication in a normed algebra, considered as a continuous linear map.

Equations
@[simp]
theorem continuous_linear_map.lmul_right_apply (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] (𝕜' : Type u_5) [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] (x y : 𝕜') :
@[simp]
theorem continuous_linear_map.op_norm_lmul_right_apply (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] (𝕜' : Type u_5) [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] (x : 𝕜') :
def continuous_linear_map.lmul_rightₗᵢ (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] (𝕜' : Type u_5) [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :
𝕜' →ₗᵢ[𝕜] 𝕜' →L[𝕜] 𝕜'

Right-multiplication in a normed algebra, considered as a linear isometry to the space of continuous linear maps.

Equations
@[simp]
def continuous_linear_map.lmul_left_right (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] (𝕜' : Type u_5) [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :
𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜'

Simultaneous left- and right-multiplication in a normed algebra, considered as a continuous trilinear map.

Equations
@[simp]
theorem continuous_linear_map.lmul_left_right_apply (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] (𝕜' : Type u_5) [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] (x y z : 𝕜') :
(((continuous_linear_map.lmul_left_right 𝕜 𝕜') x) y) z = (x * z) * y
theorem continuous_linear_map.op_norm_lmul_left_right_apply_apply_le (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] (𝕜' : Type u_5) [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] (x y : 𝕜') :
theorem continuous_linear_map.op_norm_lmul_left_right_apply_le (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] (𝕜' : Type u_5) [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] (x : 𝕜') :
def continuous_linear_map.lsmul (𝕜 : Type u_1) {E : Type u_2} [semi_normed_group E] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] (𝕜' : Type u_5) [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] [semi_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_2} [semi_normed_group E] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] (𝕜' : Type u_5) [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] [semi_normed_space 𝕜' E] [is_scalar_tower 𝕜 𝕜' E] (c : 𝕜') (x : E) :
((continuous_linear_map.lsmul 𝕜 𝕜') c) x = c x
@[simp]
theorem continuous_linear_map.norm_restrict_scalars {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] {𝕜' : Type u_5} [nondiscrete_normed_field 𝕜'] [normed_algebra 𝕜' 𝕜] [semi_normed_space 𝕜' E] [is_scalar_tower 𝕜' 𝕜 E] [semi_normed_space 𝕜' F] [is_scalar_tower 𝕜' 𝕜 F] (f : E →L[𝕜] F) :
def continuous_linear_map.restrict_scalars_isometry (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (𝕜' : Type u_5) [nondiscrete_normed_field 𝕜'] [normed_algebra 𝕜' 𝕜] [semi_normed_space 𝕜' E] [is_scalar_tower 𝕜' 𝕜 E] [semi_normed_space 𝕜' F] [is_scalar_tower 𝕜' 𝕜 F] (𝕜'' : Type u_6) [ring 𝕜''] [topological_space 𝕜''] [module 𝕜'' F] [has_continuous_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_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] {𝕜' : Type u_5} [nondiscrete_normed_field 𝕜'] [normed_algebra 𝕜' 𝕜] [semi_normed_space 𝕜' E] [is_scalar_tower 𝕜' 𝕜 E] [semi_normed_space 𝕜' F] [is_scalar_tower 𝕜' 𝕜 F] {𝕜'' : Type u_6} [ring 𝕜''] [topological_space 𝕜''] [module 𝕜'' F] [has_continuous_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_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] {𝕜' : Type u_5} [nondiscrete_normed_field 𝕜'] [normed_algebra 𝕜' 𝕜] [semi_normed_space 𝕜' E] [is_scalar_tower 𝕜' 𝕜 E] [semi_normed_space 𝕜' F] [is_scalar_tower 𝕜' 𝕜 F] {𝕜'' : Type u_6} [ring 𝕜''] [topological_space 𝕜''] [module 𝕜'' F] [has_continuous_smul 𝕜'' F] [smul_comm_class 𝕜 𝕜'' F] [smul_comm_class 𝕜' 𝕜'' F] :
def continuous_linear_map.restrict_scalarsL (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (𝕜' : Type u_5) [nondiscrete_normed_field 𝕜'] [normed_algebra 𝕜' 𝕜] [semi_normed_space 𝕜' E] [is_scalar_tower 𝕜' 𝕜 E] [semi_normed_space 𝕜' F] [is_scalar_tower 𝕜' 𝕜 F] (𝕜'' : Type u_6) [ring 𝕜''] [topological_space 𝕜''] [module 𝕜'' F] [has_continuous_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_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] {𝕜' : Type u_5} [nondiscrete_normed_field 𝕜'] [normed_algebra 𝕜' 𝕜] [semi_normed_space 𝕜' E] [is_scalar_tower 𝕜' 𝕜 E] [semi_normed_space 𝕜' F] [is_scalar_tower 𝕜' 𝕜 F] {𝕜'' : Type u_6} [ring 𝕜''] [topological_space 𝕜''] [module 𝕜'' F] [has_continuous_smul 𝕜'' F] [smul_comm_class 𝕜 𝕜'' F] [smul_comm_class 𝕜' 𝕜'' F] :
@[simp]
theorem continuous_linear_map.coe_restrict_scalarsL' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] {𝕜' : Type u_5} [nondiscrete_normed_field 𝕜'] [normed_algebra 𝕜' 𝕜] [semi_normed_space 𝕜' E] [is_scalar_tower 𝕜' 𝕜 E] [semi_normed_space 𝕜' F] [is_scalar_tower 𝕜' 𝕜 F] {𝕜'' : Type u_6} [ring 𝕜''] [topological_space 𝕜''] [module 𝕜'' F] [has_continuous_smul 𝕜'' F] [smul_comm_class 𝕜 𝕜'' F] [smul_comm_class 𝕜' 𝕜'' F] :
theorem submodule.norm_subtypeL_le {𝕜 : Type u_1} {E : Type u_2} [semi_normed_group E] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] (K : submodule 𝕜 E) :
theorem continuous_linear_map.has_sum {ι : Type u_5} {R : Type u_6} {M : Type u_7} {M₂ : Type u_8} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M₂] [module R M₂] [topological_space M] [topological_space M₂] {f : ι → M} (φ : M →L[R] M₂) {x : M} (hf : has_sum f x) :
has_sum (λ (b : ι), φ (f b)) (φ x)

Applying a continuous linear map commutes with taking an (infinite) sum.

theorem has_sum.mapL {ι : Type u_5} {R : Type u_6} {M : Type u_7} {M₂ : Type u_8} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M₂] [module R M₂] [topological_space M] [topological_space M₂] {f : ι → M} (φ : M →L[R] M₂) {x : M} (hf : has_sum f x) :
has_sum (λ (b : ι), φ (f b)) (φ x)

Alias of continuous_linear_map.has_sum.

theorem continuous_linear_map.summable {ι : Type u_5} {R : Type u_6} {M : Type u_7} {M₂ : Type u_8} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M₂] [module R M₂] [topological_space M] [topological_space M₂] {f : ι → M} (φ : M →L[R] M₂) (hf : summable f) :
summable (λ (b : ι), φ (f b))
theorem summable.mapL {ι : Type u_5} {R : Type u_6} {M : Type u_7} {M₂ : Type u_8} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M₂] [module R M₂] [topological_space M] [topological_space M₂] {f : ι → M} (φ : M →L[R] M₂) (hf : summable f) :
summable (λ (b : ι), φ (f b))

Alias of continuous_linear_map.summable.

theorem continuous_linear_map.map_tsum {ι : Type u_5} {R : Type u_6} {M : Type u_7} {M₂ : Type u_8} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M₂] [module R M₂] [topological_space M] [topological_space M₂] [t2_space M₂] {f : ι → M} (φ : M →L[R] M₂) (hf : summable f) :
φ (∑' (z : ι), f z) = ∑' (z : ι), φ (f z)
theorem continuous_linear_equiv.has_sum {ι : Type u_5} {R : Type u_6} {M : Type u_7} {M₂ : Type u_8} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M₂] [module R M₂] [topological_space M] [topological_space M₂] {f : ι → M} (e : M ≃L[R] M₂) {y : M₂} :
has_sum (λ (b : ι), e (f b)) y has_sum f ((e.symm) y)

Applying a continuous linear map commutes with taking an (infinite) sum.

theorem continuous_linear_equiv.summable {ι : Type u_5} {R : Type u_6} {M : Type u_7} {M₂ : Type u_8} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M₂] [module R M₂] [topological_space M] [topological_space M₂] {f : ι → M} (e : M ≃L[R] M₂) :
summable (λ (b : ι), e (f b)) summable f
theorem continuous_linear_equiv.tsum_eq_iff {ι : Type u_5} {R : Type u_6} {M : Type u_7} {M₂ : Type u_8} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M₂] [module R M₂] [topological_space M] [topological_space M₂] [t2_space M] [t2_space M₂] {f : ι → M} (e : M ≃L[R] M₂) {y : M₂} :
∑' (z : ι), e (f z) = y ∑' (z : ι), f z = (e.symm) y
theorem continuous_linear_equiv.map_tsum {ι : Type u_5} {R : Type u_6} {M : Type u_7} {M₂ : Type u_8} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M₂] [module R M₂] [topological_space M] [topological_space M₂] [t2_space M] [t2_space M₂] {f : ι → M} (e : M ≃L[R] M₂) :
e (∑' (z : ι), f z) = ∑' (z : ι), e (f z)
theorem continuous_linear_equiv.lipschitz {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (e : E ≃L[𝕜] F) :
theorem continuous_linear_equiv.is_O_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (e : E ≃L[𝕜] F) {α : Type u_4} (f : α → E) (l : filter α) :
asymptotics.is_O (λ (x' : α), e (f x')) f l
theorem continuous_linear_equiv.is_O_sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (e : E ≃L[𝕜] F) (l : filter E) (x : E) :
asymptotics.is_O (λ (x' : E), e (x' - x)) (λ (x' : E), x' - x) l
theorem continuous_linear_equiv.is_O_comp_rev {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (e : E ≃L[𝕜] F) {α : Type u_4} (f : α → E) (l : filter α) :
asymptotics.is_O f (λ (x' : α), e (f x')) l
theorem continuous_linear_equiv.is_O_sub_rev {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (e : E ≃L[𝕜] F) (l : filter E) (x : E) :
asymptotics.is_O (λ (x' : E), x' - x) (λ (x' : E), e (x' - x)) l
theorem continuous_linear_equiv.homothety_inverse {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (a : ) (ha : 0 < a) (f : E ≃ₗ[𝕜] F) :
(∀ (x : E), f x = a * x)∀ (y : F), (f.symm) y = a⁻¹ * y
def continuous_linear_equiv.of_homothety {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (f : E ≃ₗ[𝕜] F) (a : ) (ha : 0 < a) (hf : ∀ (x : E), f x = a * x) :
E ≃L[𝕜] F

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

Equations
def linear_equiv.to_continuous_linear_equiv_of_bounds {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [semi_normed_group E] [semi_normed_group F] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] (e : E ≃ₗ[𝕜] F) (C_to C_inv : ) (h_to : ∀ (x : E), e x C_to * x) (h_inv : ∀ (x : F), (e.symm) x C_inv * x) :
E ≃L[𝕜] F

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

Equations
def continuous_linear_map.bilinear_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] [semi_normed_space 𝕜 G] {E' : Type u_6} {F' : Type u_7} [semi_normed_group E'] [semi_normed_group F'] [semi_normed_space 𝕜 E'] [semi_normed_space 𝕜 F'] (f : E →L[𝕜] F →L[𝕜] G) (gE : E' →L[𝕜] E) (gF : F' →L[𝕜] F) :
E' →L[𝕜] F' →L[𝕜] G

Compose a bilinear map E →L[𝕜] F →L[𝕜] G with two linear maps E' →L[𝕜] E and F' →L[𝕜] F.

Equations
@[simp]
theorem continuous_linear_map.bilinear_comp_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] [semi_normed_space 𝕜 G] {E' : Type u_6} {F' : Type u_7} [semi_normed_group E'] [semi_normed_group F'] [semi_normed_space 𝕜 E'] [semi_normed_space 𝕜 F'] (f : E →L[𝕜] F →L[𝕜] G) (gE : E' →L[𝕜] E) (gF : F' →L[𝕜] F) (x : E') (y : F') :
((f.bilinear_comp gE gF) x) y = (f (gE x)) (gF y)
def continuous_linear_map.deriv₂ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] [semi_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_2} {F : Type u_3} {G : Type u_4} [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] [semi_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₂ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F] [semi_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.continuous_iff_is_closed_ker {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [normed_field 𝕜] [normed_space 𝕜 E] {f : E →ₗ[𝕜] 𝕜} :
theorem linear_map.bound_of_shell {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [normed_group F] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (f : E →ₗ[𝕜] F) {ε C : } (ε_pos : 0 < ε) {c : 𝕜} (hc : 1 < c) (hf : ∀ (x : E), ε / c xx < εf x C * x) (x : E) :
theorem continuous_linear_map.op_norm_zero_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [normed_group F] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (f : E →L[𝕜] F) :
f = 0 f = 0

An operator is zero iff its norm vanishes.

@[simp]
theorem continuous_linear_map.norm_id {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [nontrivial E] :

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

@[instance]
def continuous_linear_map.norm_one_class {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [nontrivial E] :
@[instance]
def continuous_linear_map.to_normed_group {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [normed_group F] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] :

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

Equations
@[instance]
def continuous_linear_map.to_normed_space {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [normed_group F] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] {𝕜' : Type u_4} [normed_field 𝕜'] [normed_space 𝕜' F] [smul_comm_class 𝕜 𝕜' F] :
normed_space 𝕜' (E →L[𝕜] F)
Equations
@[instance]
def continuous_linear_map.to_normed_ring {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] :

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

Equations
@[instance]
def continuous_linear_map.to_normed_algebra {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [nontrivial E] :
normed_algebra 𝕜 (E →L[𝕜] E)

For a nonzero normed space E, continuous linear endomorphisms form a normed algebra with respect to the operator norm.

Equations
theorem continuous_linear_map.homothety_norm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [normed_group F] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] [nontrivial E] (f : E →L[𝕜] F) {a : } (hf : ∀ (x : E), f x = a * x) :
theorem continuous_linear_map.uniform_embedding_of_bound {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [normed_group F] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (f : E →L[𝕜] F) {K : ℝ≥0} (hf : ∀ (x : E), x (K) * f x) :
theorem continuous_linear_map.antilipschitz_of_uniform_embedding {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [normed_group F] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (f : E →L[𝕜] F) (hf : uniform_embedding f) :

If a continuous linear map is a uniform embedding, then it is expands the distances by a positive factor.

@[instance]
def continuous_linear_map.complete_space {𝕜 : Type u_1} {F : Type u_3} [normed_group F] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 F] {E : Type u_2} [semi_normed_group E] [semi_normed_space 𝕜 E] [complete_space 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.

def continuous_linear_map.extend {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [normed_group E] [normed_group F] [normed_group G] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] [normed_space 𝕜 G] (f : E →L[𝕜] F) [complete_space F] (e : E →L[𝕜] G) (h_dense : dense_range e) (h_e : uniform_inducing e) :
G →L[𝕜] F

Extension of a continuous linear map f : E →L[𝕜] F, with E a normed space and F a complete normed space, along a uniform and dense embedding e : E →L[𝕜] G.

Equations
theorem continuous_linear_map.extend_unique {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [normed_group E] [normed_group F] [normed_group G] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] [normed_space 𝕜 G] (f : E →L[𝕜] F) [complete_space F] (e : E →L[𝕜] G) (h_dense : dense_range e) (h_e : uniform_inducing e) (g : G →L[𝕜] F) (H : g.comp e = f) :
f.extend e h_dense h_e = g
@[simp]
theorem continuous_linear_map.extend_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [normed_group E] [normed_group F] [normed_group G] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] [normed_space 𝕜 G] [complete_space F] (e : E →L[𝕜] G) (h_dense : dense_range e) (h_e : uniform_inducing e) :
0.extend e h_dense h_e = 0
theorem continuous_linear_map.op_norm_extend_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [normed_group E] [normed_group F] [normed_group G] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] [normed_space 𝕜 G] (f : E →L[𝕜] F) [complete_space F] (e : E →L[𝕜] G) (h_dense : dense_range e) {N : ℝ≥0} (h_e : ∀ (x : E), x (N) * e x) :
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} {E : Type u_2} {F : Type u_3} [normed_group E] [normed_group F] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] [nontrivial E] (f : E →ₗᵢ[𝕜] F) :
theorem continuous_linear_map.op_norm_comp_linear_isometry_equiv {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [normed_group F] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] {G : Type u_4} [semi_normed_group G] [semi_normed_space 𝕜 G] (f : F →L[𝕜] G) (g : E ≃ₗᵢ[𝕜] 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_2} {F : Type u_3} [normed_group E] [normed_group F] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (c : E →L[𝕜] 𝕜) (f : F) :

The norm of the tensor product of a scalar linear map and of an element of a normed space is the product of the norms.

@[simp]
theorem continuous_linear_map.nnnorm_smul_right_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [normed_group F] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (c : E →L[𝕜] 𝕜) (f : F) :

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

def continuous_linear_map.smul_rightL (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [normed_group E] [normed_group F] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] :
(E →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_2} {F : Type u_3} [normed_group E] [normed_group F] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (c : E →L[𝕜] 𝕜) (f : F) :
@[simp]
theorem continuous_linear_map.norm_smul_rightL {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [normed_group F] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (c : E →L[𝕜] 𝕜) [nontrivial F] :
@[simp]
theorem continuous_linear_map.op_norm_lmul (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] (𝕜' : Type u_5) [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :
@[simp]
theorem continuous_linear_map.op_norm_lmul_right (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] (𝕜' : Type u_5) [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :
theorem submodule.norm_subtypeL {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] (K : submodule 𝕜 E) [nontrivial K] :
theorem continuous_linear_equiv.antilipschitz {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [normed_group F] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (e : E ≃L[𝕜] F) :
theorem continuous_linear_equiv.uniform_embedding {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [normed_group F] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (e : E ≃L[𝕜] F) :

A continuous linear equiv is a uniform embedding.

theorem continuous_linear_equiv.one_le_norm_mul_norm_symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [normed_group F] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (e : E ≃L[𝕜] F) [nontrivial E] :
theorem continuous_linear_equiv.norm_pos {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [normed_group F] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (e : E ≃L[𝕜] F) [nontrivial E] :
theorem continuous_linear_equiv.norm_symm_pos {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [normed_group F] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (e : E ≃L[𝕜] F) [nontrivial E] :
theorem continuous_linear_equiv.nnnorm_symm_pos {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [normed_group F] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (e : E ≃L[𝕜] F) [nontrivial E] :
theorem continuous_linear_equiv.subsingleton_or_norm_symm_pos {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [normed_group F] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (e : E ≃L[𝕜] F) :
theorem continuous_linear_equiv.subsingleton_or_nnnorm_symm_pos {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [normed_group F] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (e : E ≃L[𝕜] F) :
def continuous_linear_equiv.to_span_nonzero_singleton (𝕜 : Type u_1) {E : Type u_2} [normed_group E] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] (x : E) (h : x 0) :
𝕜 ≃L[𝕜] (submodule.span 𝕜 {x})

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

Equations
def continuous_linear_equiv.coord (𝕜 : Type u_1) {E : Type u_2} [normed_group E] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] (x : E) (h : x 0) :
(submodule.span 𝕜 {x}) →L[𝕜] 𝕜

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

Equations
@[simp]
theorem continuous_linear_equiv.coord_to_span_nonzero_singleton (𝕜 : Type u_1) {E : Type u_2} [normed_group E] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] {x : E} (h : x 0) (c : 𝕜) :
@[simp]
@[simp]
theorem continuous_linear_equiv.coord_norm (𝕜 : Type u_1) {E : Type u_2} [normed_group E] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] (x : E) (h : x 0) :
@[simp]
theorem continuous_linear_equiv.coord_self (𝕜 : Type u_1) {E : Type u_2} [normed_group E] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] (x : E) (h : x 0) :
theorem linear_equiv.uniform_embedding {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [normed_group F] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (e : E ≃ₗ[𝕜] F) (h₁ : continuous e) (h₂ : continuous (e.symm)) :