# mathlibdocumentation

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} [normed_field 𝕜] [ E] [ F] (f : E →ₗ[𝕜] F) (C : ) (h : ∀ (x : E), f x C * x) :
theorem linear_map.antilipschitz_of_bound {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_field 𝕜] [ E] [ 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} [normed_field 𝕜] [ E] [ F] (f : E →ₗ[𝕜] F) {K : ℝ≥0} (h : f) (x : E) :
theorem linear_map.uniform_continuous_of_bound {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_field 𝕜] [ E] [ 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} [normed_field 𝕜] [ E] [ 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} [normed_field 𝕜] [ E] [ 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} [normed_field 𝕜] [ 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} [normed_field 𝕜] [ E] [ 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} [normed_field 𝕜] [ E] [ 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} [normed_field 𝕜] [ E] [ 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} [normed_field 𝕜] [ E] [ F] (f : E →ₗ[𝕜] F) (C : ) (h : ∀ (x : E), f x C * x) (x : E) :
(f.mk_continuous C h) x = f x
@[simp]
theorem linear_map.mk_continuous_of_exists_bound_coe {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_field 𝕜] [ E] [ 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} [normed_field 𝕜] [ E] [ F] (f : E →ₗ[𝕜] F) (h : ∃ (C : ), ∀ (x : E), f x C * x) (x : E) :
= f x
@[simp]
theorem linear_map.to_continuous_linear_map₁_coe {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [ E] (f : 𝕜 →ₗ[𝕜] E) :
@[simp]
theorem linear_map.to_continuous_linear_map₁_apply {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [ E] (f : 𝕜 →ₗ[𝕜] E) (x : 𝕜) :
= f x
theorem linear_map.bound_of_shell_semi_normed {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ 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} [ E] [ 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} [ E] [ 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} [ E] [ F] (f : E →L[𝕜] F) :
∃ (C : ), 0 < C ∀ (x : E), f x C * x
theorem continuous_linear_map.is_O_id {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] (f : E →L[𝕜] F) (l : filter E) :
(λ (x : E), x) l
theorem continuous_linear_map.is_O_comp {𝕜 : Type u_1} {F : Type u_3} {G : Type u_4} [ F] [ G] {α : Type u_2} (g : F →L[𝕜] G) (f : α → F) (l : filter α) :
asymptotics.is_O (λ (x' : α), g (f x')) f l
theorem continuous_linear_map.is_O_sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] (f : E →L[𝕜] F) (l : filter E) (x : E) :
asymptotics.is_O (λ (x' : E), f (x' - x)) (λ (x' : E), x' - x) l
def continuous_linear_map.of_homothety {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ 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
• = _
theorem continuous_linear_map.to_span_singleton_homothety (𝕜 : Type u_1) {E : Type u_2} [ E] (x : E) (c : 𝕜) :
def continuous_linear_map.to_span_singleton (𝕜 : Type u_1) {E : Type u_2} [ 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
def continuous_linear_map.op_norm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ 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} [ E] [ F] :
has_norm (E →L[𝕜] F)
Equations
theorem continuous_linear_map.norm_def {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ 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} [ E] [ 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} [ E] [ 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} [ E] [ F] (f : E →L[𝕜] F) :
theorem continuous_linear_map.le_op_norm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ 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} [ E] [ 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} [ E] [ F] (f : E →L[𝕜] F) {c : } (h : f c) (x : E) :
theorem continuous_linear_map.lipschitz {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] (f : E →L[𝕜] F) :

continuous linear maps are Lipschitz continuous.

theorem continuous_linear_map.ratio_le_op_norm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ 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} [ E] [ 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} [ E] [ 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} [ E] [ F] {f : E →L[𝕜] F} {K : ℝ≥0} (hf : f) :
theorem continuous_linear_map.op_norm_le_of_shell {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ 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} [ E] [ F] {f : E →L[𝕜] F} {ε C : } (ε_pos : 0 < ε) (hC : 0 C) (hf : ∀ (x : E), x ε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} [ E] [ 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} [ E] [ 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} [ E] [ 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} [ E] [ 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} [ E] [ F] :

The norm of the `0` operator is `0`.

theorem continuous_linear_map.norm_id_le {𝕜 : Type u_1} {E : Type u_2} [ E] :

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} [ 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} [ E] [ F] {𝕜' : Type u_4} [normed_field 𝕜'] [ F] [ 𝕜' F] (c : 𝕜') (f : E →L[𝕜] F) :
theorem continuous_linear_map.op_norm_neg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ 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} [ E] [ 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} [ E] [ F] {𝕜' : Type u_4} [normed_field 𝕜'] [ F] [ 𝕜' F] :
(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} [ E] [ F] [ G] (h : F →L[𝕜] G) (f : E →L[𝕜] F) :

The operator norm is submultiplicative.

@[instance]
def continuous_linear_map.to_semi_normed_ring {𝕜 : Type u_1} {E : Type u_2} [ E] :

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

Equations
theorem continuous_linear_map.le_op_norm₂ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [ E] [ F] [ 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} [ E] [ F] [ 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} [ E] [ F] [ 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} [ E] [ F] [ G] (R : Type u_5) [ring R] [ F] [ G] [ F] [ G] [ F] [ 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} [ E] [ 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} [ E] [ 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} [ E] [ F] (f : E →L[𝕜] F) :
∀ (x : E), f x = x

A continuous linear map is an isometry if and only if it preserves the norm.

theorem linear_isometry.norm_to_continuous_linear_map_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] (f : E →ₗᵢ[𝕜] F) :
theorem linear_map.mk_continuous_norm_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ 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} [ E] [ F] (f : E →ₗ[𝕜] F) {C : } (h : ∀ (x : E), f x C * x) :
h max C 0

If a continuous linear map is constructed from a linear map via the constructor `mk_continuous`, then its norm is bounded by the bound or zero if bound is negative.

def linear_map.mk_continuous₂ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [ E] [ F] [ 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} [ E] [ F] [ 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} [ E] [ F] [ G] (f : E →ₗ[𝕜] F →ₗ[𝕜] G) {C : } (hC : ∀ (x : E) (y : F), (f x) y (C * x) * y) :
hC max C 0
theorem linear_map.mk_continuous₂_norm_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [ E] [ F] [ G] (f : E →ₗ[𝕜] F →ₗ[𝕜] G) {C : } (h0 : 0 C) (hC : ∀ (x : E) (y : F), (f x) y (C * x) * y) :
hC C
def continuous_linear_map.flip {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [ E] [ F] [ 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} [ E] [ F] [ 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} [ E] [ F] [ 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} [ E] [ F] [ 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} [ E] [ F] [ 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} [ E] [ F] [ 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) [ E] [ F] [ 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} [ E] [ F] [ G] :
G).symm = G
@[simp]
theorem continuous_linear_map.coe_flipₗᵢ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [ E] [ F] [ G] :
def continuous_linear_map.apply (𝕜 : Type u_1) {E : Type u_2} (F : Type u_3) [ E] [ 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} [ E] [ F] (v : E) (f : E →L[𝕜] F) :
( v) f = f v
def continuous_linear_map.compL (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) (G : Type u_4) [ E] [ F] [ 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} [ E] [ F] [ G] (f : F →L[𝕜] G) (g : E →L[𝕜] F) :
( G) f) g = f.comp g
def continuous_linear_map.lmulₗᵢ (𝕜 : Type u_1) (𝕜' : Type u_5) [normed_ring 𝕜'] [ 𝕜'] :
𝕜' →ₗᵢ[𝕜] 𝕜' →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) (𝕜' : Type u_5) [normed_ring 𝕜'] [ 𝕜'] :
𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜'

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

Equations
@[simp]
theorem continuous_linear_map.lmul_apply (𝕜 : Type u_1) (𝕜' : Type u_5) [normed_ring 𝕜'] [ 𝕜'] (x y : 𝕜') :
( x) y = x * y
@[simp]
theorem continuous_linear_map.coe_lmulₗᵢ (𝕜 : Type u_1) (𝕜' : Type u_5) [normed_ring 𝕜'] [ 𝕜'] :
@[simp]
theorem continuous_linear_map.op_norm_lmul_apply (𝕜 : Type u_1) (𝕜' : Type u_5) [normed_ring 𝕜'] [ 𝕜'] (x : 𝕜') :
def continuous_linear_map.lmul_right (𝕜 : Type u_1) (𝕜' : Type u_5) [normed_ring 𝕜'] [ 𝕜'] :
𝕜' →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) (𝕜' : Type u_5) [normed_ring 𝕜'] [ 𝕜'] (x y : 𝕜') :
x) y = y * x
@[simp]
theorem continuous_linear_map.op_norm_lmul_right_apply (𝕜 : Type u_1) (𝕜' : Type u_5) [normed_ring 𝕜'] [ 𝕜'] (x : 𝕜') :
def continuous_linear_map.lmul_rightₗᵢ (𝕜 : Type u_1) (𝕜' : Type u_5) [normed_ring 𝕜'] [ 𝕜'] :
𝕜' →ₗᵢ[𝕜] 𝕜' →L[𝕜] 𝕜'

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

Equations
@[simp]
theorem continuous_linear_map.coe_lmul_rightₗᵢ (𝕜 : Type u_1) (𝕜' : Type u_5) [normed_ring 𝕜'] [ 𝕜'] :
def continuous_linear_map.lmul_left_right (𝕜 : Type u_1) (𝕜' : Type u_5) [normed_ring 𝕜'] [ 𝕜'] :
𝕜' →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) (𝕜' : Type u_5) [normed_ring 𝕜'] [ 𝕜'] (x y z : 𝕜') :
( x) y) z = (x * z) * y
theorem continuous_linear_map.op_norm_lmul_left_right_apply_apply_le (𝕜 : Type u_1) (𝕜' : Type u_5) [normed_ring 𝕜'] [ 𝕜'] (x y : 𝕜') :
theorem continuous_linear_map.op_norm_lmul_left_right_apply_le (𝕜 : Type u_1) (𝕜' : Type u_5) [normed_ring 𝕜'] [ 𝕜'] (x : 𝕜') :
theorem continuous_linear_map.op_norm_lmul_left_right_le (𝕜 : Type u_1) (𝕜' : Type u_5) [normed_ring 𝕜'] [ 𝕜'] :
def continuous_linear_map.lsmul (𝕜 : Type u_1) {E : Type u_2} [ E] (𝕜' : Type u_5) [normed_field 𝕜'] [ 𝕜'] [ E] [ 𝕜' E] :
𝕜' →L[𝕜] E →L[𝕜] E

Scalar multiplication as a continuous bilinear map.

Equations
• = _
@[simp]
theorem continuous_linear_map.norm_restrict_scalars {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {𝕜' : Type u_5} [ 𝕜] [ E] [ 𝕜 E] [ F] [ 𝕜 F] (f : E →L[𝕜] F) :
def continuous_linear_map.restrict_scalars_isometry (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [ E] [ F] (𝕜' : Type u_5) [ 𝕜] [ E] [ 𝕜 E] [ F] [ 𝕜 F] (𝕜'' : Type u_6) [ring 𝕜''] [topological_space 𝕜''] [module 𝕜'' F] [ F] [ 𝕜'' F] [ 𝕜'' 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} [ E] [ F] {𝕜' : Type u_5} [ 𝕜] [ E] [ 𝕜 E] [ F] [ 𝕜 F] {𝕜'' : Type u_6} [ring 𝕜''] [topological_space 𝕜''] [module 𝕜'' F] [ F] [ 𝕜'' F] [ 𝕜'' F] :
@[simp]
theorem continuous_linear_map.restrict_scalars_isometry_to_linear_map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {𝕜' : Type u_5} [ 𝕜] [ E] [ 𝕜 E] [ F] [ 𝕜 F] {𝕜'' : Type u_6} [ring 𝕜''] [topological_space 𝕜''] [module 𝕜'' F] [ F] [ 𝕜'' F] [ 𝕜'' F] :
𝕜'').to_linear_map = 𝕜''
def continuous_linear_map.restrict_scalarsL (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [ E] [ F] (𝕜' : Type u_5) [ 𝕜] [ E] [ 𝕜 E] [ F] [ 𝕜 F] (𝕜'' : Type u_6) [ring 𝕜''] [topological_space 𝕜''] [module 𝕜'' F] [ F] [ 𝕜'' F] [ 𝕜'' 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} [ E] [ F] {𝕜' : Type u_5} [ 𝕜] [ E] [ 𝕜 E] [ F] [ 𝕜 F] {𝕜'' : Type u_6} [ring 𝕜''] [topological_space 𝕜''] [module 𝕜'' F] [ F] [ 𝕜'' F] [ 𝕜'' F] :
𝕜'') = 𝕜''
@[simp]
theorem continuous_linear_map.coe_restrict_scalarsL' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {𝕜' : Type u_5} [ 𝕜] [ E] [ 𝕜 E] [ F] [ 𝕜 F] {𝕜'' : Type u_6} [ring 𝕜''] [topological_space 𝕜''] [module 𝕜'' F] [ F] [ 𝕜'' F] [ 𝕜'' F] :
theorem submodule.norm_subtypeL_le {𝕜 : Type u_1} {E : Type u_2} [ E] (K : E) :
theorem continuous_linear_map.has_sum {ι : Type u_5} {R : Type u_6} {M : Type u_7} {M₂ : Type u_8} [semiring R] [ M] [add_comm_monoid M₂] [ M₂] {f : ι → M} (φ : M →L[R] M₂) {x : M} (hf : 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] [ M] [add_comm_monoid M₂] [ M₂] {f : ι → M} (φ : M →L[R] M₂) {x : M} (hf : 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] [ M] [add_comm_monoid M₂] [ 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] [ M] [add_comm_monoid M₂] [ 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] [ M] [add_comm_monoid M₂] [ 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] [ M] [add_comm_monoid M₂] [ M₂] {f : ι → M} (e : M ≃L[R] M₂) {y : M₂} :
has_sum (λ (b : ι), e (f b)) y ((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] [ M] [add_comm_monoid M₂] [ M₂] {f : ι → M} (e : M ≃L[R] M₂) :
summable (λ (b : ι), e (f b))
theorem continuous_linear_equiv.tsum_eq_iff {ι : Type u_5} {R : Type u_6} {M : Type u_7} {M₂ : Type u_8} [semiring R] [ M] [add_comm_monoid M₂] [ 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] [ M] [add_comm_monoid M₂] [ 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} [ E] [ F] (e : E ≃L[𝕜] F) :
e
theorem continuous_linear_equiv.is_O_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ 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} [ E] [ 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} [ E] [ F] (e : E ≃L[𝕜] F) {α : Type u_4} (f : α → E) (l : filter α) :
(λ (x' : α), e (f x')) l
theorem continuous_linear_equiv.is_O_sub_rev {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ 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} [ E] [ 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} [ E] [ 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
theorem continuous_linear_equiv.to_span_nonzero_singleton_homothety (𝕜 : Type u_1) {E : Type u_2} [ E] (x : E) (h : x 0) (c : 𝕜) :
def linear_equiv.to_continuous_linear_equiv_of_bounds {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ 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} [ E] [ F] [ G] {E' : Type u_6} {F' : Type u_7} [ E'] [ 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} [ E] [ F] [ G] {E' : Type u_6} {F' : Type u_7} [ E'] [ 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} [ E] [ F] [ 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} [ E] [ F] [ 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} [ E] [ F] [ 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 𝕜] [ 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] [ E] [ 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] [ E] [ F] (f : E →L[𝕜] F) :
f = 0 f = 0

An operator is zero iff its norm vanishes.

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

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

@[simp]
theorem continuous_linear_map.norm_id_field {𝕜 : Type u_1}  :
@[simp]
theorem continuous_linear_map.norm_id_field' {𝕜 : Type u_1}  :
@[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] [ E] [ 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] [ E] [ F] {𝕜' : Type u_4} [normed_field 𝕜'] [ F] [ 𝕜' F] :
(E →L[𝕜] F)
Equations
@[instance]
def continuous_linear_map.to_normed_ring {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ 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] [ E] [nontrivial E] :
(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] [ E] [ F] [nontrivial E] (f : E →L[𝕜] F) {a : } (hf : ∀ (x : E), f x = a * x) :
theorem continuous_linear_map.to_span_singleton_norm {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] (x : E) :
theorem continuous_linear_map.uniform_embedding_of_bound {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [normed_group F] [ E] [ 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] [ E] [ F] (f : E →L[𝕜] F) (hf : uniform_embedding f) :
∃ (K : ℝ≥0),

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] [ F] {E : Type u_2} [ E]  :

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] [ E] [ F] [ G] (f : E →L[𝕜] 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] [ E] [ F] [ G] (f : E →L[𝕜] 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] [ E] [ F] [ G] (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] [ E] [ F] [ G] (f : E →L[𝕜] 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] [ E] [ 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] [ E] [ F] {G : Type u_4} [ 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] [ E] [ F] (c : E →L[𝕜] 𝕜) (f : F) :

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

def continuous_linear_map.smul_rightL (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [normed_group E] [normed_group F] [ E] [ 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] [ E] [ 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] [ E] [ F] (c : E →L[𝕜] 𝕜) [nontrivial F] :
@[simp]
theorem continuous_linear_map.op_norm_lmul (𝕜 : Type u_1) (𝕜' : Type u_5) [normed_ring 𝕜'] [ 𝕜'] :
@[simp]
theorem continuous_linear_map.op_norm_lmul_right (𝕜 : Type u_1) (𝕜' : Type u_5) [normed_ring 𝕜'] [ 𝕜'] :
theorem submodule.norm_subtypeL {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] (K : 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] [ E] [ F] (e : E ≃L[𝕜] F) :
e
theorem continuous_linear_equiv.uniform_embedding {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [normed_group F] [ E] [ 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] [ E] [ 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] [ E] [ 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] [ E] [ 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] [ E] [ 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] [ E] [ 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] [ E] [ F] (e : E ≃L[𝕜] F) :
def continuous_linear_equiv.to_span_nonzero_singleton (𝕜 : Type u_1) {E : Type u_2} [normed_group E] [ E] (x : E) (h : x 0) :
𝕜 ≃L[𝕜] {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] [ E] (x : E) (h : x 0) :
{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.coe_to_span_nonzero_singleton_symm (𝕜 : Type u_1) {E : Type u_2} [normed_group E] [ E] {x : E} (h : x 0) :
@[simp]
theorem continuous_linear_equiv.coord_to_span_nonzero_singleton (𝕜 : Type u_1) {E : Type u_2} [normed_group E] [ E] {x : E} (h : x 0) (c : 𝕜) :
= c
@[simp]
theorem continuous_linear_equiv.to_span_nonzero_singleton_coord (𝕜 : Type u_1) {E : Type u_2} [normed_group E] [ E] {x : E} (h : x 0) (y : {x})) :
( y) = y
@[simp]
theorem continuous_linear_equiv.coord_norm (𝕜 : Type u_1) {E : Type u_2} [normed_group E] [ E] (x : E) (h : x 0) :
@[simp]
theorem continuous_linear_equiv.coord_self (𝕜 : Type u_1) {E : Type u_2} [normed_group E] [ E] (x : E) (h : x 0) :
x, _⟩ = 1
theorem linear_equiv.uniform_embedding {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [normed_group F] [ E] [ F] (e : E ≃ₗ[𝕜] F) (h₁ : continuous e) (h₂ : continuous (e.symm)) :