Operator norm for maps on normed spaces #

This file contains statements about operator norm for which it really matters that the underlying space has a norm (rather than just a seminorm).

source

@[simp]

theorem LinearIsometry.norm_toContinuousLinearMap {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [NontrivialTopology E] [RingHomIsometric σ₁₂] (f : E →ₛₗᵢ[σ₁₂] F) :

‖f.toContinuousLinearMap‖ = 1

source

@[simp]

theorem LinearIsometry.nnnorm_toContinuousLinearMap {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [NontrivialTopology E] [RingHomIsometric σ₁₂] (f : E →ₛₗᵢ[σ₁₂] F) :

‖f.toContinuousLinearMap‖₊ = 1

source

@[simp]

theorem LinearIsometry.enorm_toContinuousLinearMap {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [NontrivialTopology E] [RingHomIsometric σ₁₂] (f : E →ₛₗᵢ[σ₁₂] F) :

‖f.toContinuousLinearMap‖ₑ = 1

source

theorem LinearIsometry.norm_toContinuousLinearMap_comp {𝕜 : Type u_1} {𝕜₂ : Type u_3} {𝕜₃ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_8} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomIsometric σ₁₂] (f : F →ₛₗᵢ[σ₂₃] G) {g : E →SL[σ₁₂] F} :

‖f.toContinuousLinearMap ∘SL g‖ = ‖g‖

Postcomposition of a continuous linear map with a linear isometry preserves the operator norm.

source

noncomputable def LinearIsometry.postcomp {𝕜 : Type u_1} {𝕜₂ : Type u_3} {𝕜₃ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_8} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomIsometric σ₁₂] [RingHomIsometric σ₁₃] (a : F →ₛₗᵢ[σ₂₃] G) :

(E →SL[σ₁₂] F) →ₛₗᵢ[σ₂₃] E →SL[σ₁₃] G

Composing on the left with a linear isometry gives a linear isometry between spaces of continuous linear maps.

Equations

a.postcomp = { toFun := fun (f : E →SL[σ₁₂] F) => a.toContinuousLinearMap ∘SL f, map_add' := ⋯, map_smul' := ⋯, norm_map' := ⋯ }

Instances For

source

@[simp]

theorem LinearIsometryEquiv.norm_toContinuousLinearMap {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NontrivialTopology E] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₁₂] (e : E ≃ₛₗᵢ[σ₁₂] F) :

‖↑↑e‖ = 1

source

@[simp]

theorem LinearIsometryEquiv.nnnorm_toContinuousLinearMap {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NontrivialTopology E] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₁₂] (e : E ≃ₛₗᵢ[σ₁₂] F) :

‖↑↑e‖₊ = 1

source

@[simp]

theorem LinearIsometryEquiv.enorm_toContinuousLinearMap {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NontrivialTopology E] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₁₂] (e : E ≃ₛₗᵢ[σ₁₂] F) :

‖↑↑e‖ₑ = 1

source

theorem LinearMap.bound_of_shell {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →ₛₗ[σ₁₂] F) {ε C : ℝ} (ε_pos : 0 < ε) {c : 𝕜} (hc : 1 < ‖c‖) (hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖) (x : E) :

‖f x‖ ≤ C * ‖x‖

source

theorem LinearMap.bound_of_ball_bound {𝕜 : Type u_1} {E : Type u_5} {Fₗ : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] {r : ℝ} (r_pos : 0 < r) (c : ℝ) (f : E →ₗ[𝕜] Fₗ) (h : ∀ z ∈ Metric.ball 0 r, ‖f z‖ ≤ c) :

∃ (C : ℝ), ∀ (z : E), ‖f z‖ ≤ C * ‖z‖

LinearMap.bound_of_ball_bound' is a version of this lemma over a field satisfying RCLike that produces a concrete bound.

source

theorem LinearMap.antilipschitz_of_comap_nhds_le {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [h : RingHomIsometric σ₁₂] (f : E →ₛₗ[σ₁₂] F) (hf : Filter.comap (⇑f) (nhds 0) ≤ nhds 0) :

∃ (K : NNReal), AntilipschitzWith K ⇑f

source

theorem ContinuousLinearMap.opNorm_zero_iff {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) [RingHomIsometric σ₁₂] :

‖f‖ = 0 ↔ f = 0

An operator is zero iff its norm vanishes.

source

@[implicit_reducible]

noncomputable instance ContinuousLinearMap.toNormedAddCommGroup {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] :

NormedAddCommGroup (E →SL[σ₁₂] F)

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

Equations

ContinuousLinearMap.toNormedAddCommGroup = NormedAddCommGroup.ofSeparation ⋯

source

@[implicit_reducible]

noncomputable instance ContinuousLinearMap.toNormedRing {𝕜 : Type u_1} {E : Type u_5} [NormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] :

NormedRing (E →L[𝕜] E)

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

Equations

One or more equations did not get rendered due to their size.

source

theorem ContinuousLinearMap.antilipschitz_of_isEmbedding {𝕜 : Type u_1} {E : Type u_5} {Fₗ : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] (f : E →L[𝕜] Fₗ) (hf : Topology.IsEmbedding ⇑f) :

∃ (K : NNReal), AntilipschitzWith K ⇑f

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

source

@[simp]

theorem ContinuousLinearMap.norm_smulRightL {𝕜 : Type u_1} {E : Type u_5} {Fₗ : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] (c : StrongDual 𝕜 E) [Nontrivial Fₗ] :

‖(smulRightL 𝕜 E Fₗ) c‖ = ‖c‖

source

theorem ContinuousLinearMap.norm_smulRightL_le {𝕜 : Type u_1} {E : Type u_5} {Fₗ : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] :

‖smulRightL 𝕜 E Fₗ‖ ≤ 1

Composition with isometries #

source

@[simp]

theorem ContinuousLinearMap.opNNNorm_comp_linearIsometryEquiv {𝕜₁ : Type u_2} {𝕜₂ : Type u_3} {𝕜₃ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_8} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [NontriviallyNormedField 𝕜₁] [NormedSpace 𝕜₁ E] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜₃ G] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜₁ →+* 𝕜₃} [RingHomIsometric σ₁₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomIsometric σ₂₃] (f : F →SL[σ₂₃] G) (e : E ≃ₛₗᵢ[σ₁₂] F) :

‖f ∘SL ↑↑e‖₊ = ‖f‖₊

Precomposition with a linear isometry preserves the operator norm.

source

@[simp]

theorem ContinuousLinearMap.opNNNorm_linearIsometryEquiv_comp {𝕜₁ : Type u_2} {𝕜₂ : Type u_3} {𝕜₃ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_8} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [NontriviallyNormedField 𝕜₁] [NormedSpace 𝕜₁ E] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜₃ G] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₃₂ : 𝕜₃ →+* 𝕜₂} [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃] {σ₁₃ : 𝕜₁ →+* 𝕜₃} [RingHomIsometric σ₁₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomIsometric σ₁₂] (e : F ≃ₛₗᵢ[σ₂₃] G) (f : E →SL[σ₁₂] F) :

‖↑↑e ∘SL f‖₊ = ‖f‖₊

Postcomposition with a linear isometry preserves the operator norm.

source

@[simp]

theorem ContinuousLinearMap.opNorm_comp_linearIsometryEquiv {𝕜₁ : Type u_2} {𝕜₂ : Type u_3} {𝕜₃ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_8} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [NontriviallyNormedField 𝕜₁] [NormedSpace 𝕜₁ E] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜₃ G] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜₁ →+* 𝕜₃} [RingHomIsometric σ₁₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomIsometric σ₂₃] (f : F →SL[σ₂₃] G) (e : E ≃ₛₗᵢ[σ₁₂] F) :

‖f ∘SL ↑↑e‖ = ‖f‖

Precomposition with a linear isometry preserves the operator norm.

source

@[simp]

theorem ContinuousLinearMap.opNorm_linearIsometryEquiv_comp {𝕜₁ : Type u_2} {𝕜₂ : Type u_3} {𝕜₃ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_8} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [NontriviallyNormedField 𝕜₁] [NormedSpace 𝕜₁ E] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜₃ G] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₃₂ : 𝕜₃ →+* 𝕜₂} [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃] {σ₁₃ : 𝕜₁ →+* 𝕜₃} [RingHomIsometric σ₁₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomIsometric σ₁₂] (e : F ≃ₛₗᵢ[σ₂₃] G) (f : E →SL[σ₁₂] F) :

‖↑↑e ∘SL f‖ = ‖f‖

Postcomposition with a linear isometry preserves the operator norm.

source

@[simp]

theorem ContinuousLinearMap.opNNNorm_mul_linearIsometryEquiv {𝕜 : Type u_1} {E : Type u_5} [NormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] (f : E →L[𝕜] E) (e : E ≃ₗᵢ[𝕜] E) :

‖f * ↑↑e‖₊ = ‖f‖₊

Precomposition with a linear isometry preserves the operator norm.

source

@[simp]

theorem ContinuousLinearMap.opNNNorm_linearIsometryEquiv_mul {𝕜 : Type u_1} {E : Type u_5} [NormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] (e : E ≃ₗᵢ[𝕜] E) (f : E →L[𝕜] E) :

‖↑↑e * f‖₊ = ‖f‖₊

Postcomposition with a linear isometry preserves the operator norm.

source

@[simp]

theorem ContinuousLinearMap.opNorm_mul_linearIsometryEquiv {𝕜 : Type u_1} {E : Type u_5} [NormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] (f : E →L[𝕜] E) (e : E ≃ₗᵢ[𝕜] E) :

‖f * ↑↑e‖ = ‖f‖

Precomposition with a linear isometry preserves the operator norm.

source

@[simp]

theorem ContinuousLinearMap.opNorm_linearIsometryEquiv_mul {𝕜 : Type u_1} {E : Type u_5} [NormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] (e : E ≃ₗᵢ[𝕜] E) (f : E →L[𝕜] E) :

‖↑↑e * f‖ = ‖f‖

Postcomposition with a linear isometry preserves the operator norm.

source

theorem Submodule.norm_subtypeL {𝕜 : Type u_1} {E : Type u_5} [NormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] (K : Submodule 𝕜 E) [Nontrivial ↥K] :

‖K.subtypeL‖ = 1

source

theorem ContinuousLinearEquiv.antilipschitz {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₂₁] (e : E ≃SL[σ₁₂] F) :

AntilipschitzWith ‖↑e.symm‖₊ ⇑e

source

theorem ContinuousLinearEquiv.one_le_norm_mul_norm_symm {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₂₁] [RingHomIsometric σ₁₂] [Nontrivial E] (e : E ≃SL[σ₁₂] F) :

1 ≤ ‖↑e‖ * ‖↑e.symm‖

source

theorem ContinuousLinearEquiv.norm_pos {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₂₁] [RingHomIsometric σ₁₂] [Nontrivial E] (e : E ≃SL[σ₁₂] F) :

0 < ‖↑e‖

source

theorem ContinuousLinearEquiv.norm_symm_pos {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₂₁] [RingHomIsometric σ₁₂] [Nontrivial E] (e : E ≃SL[σ₁₂] F) :

0 < ‖↑e.symm‖

source

theorem ContinuousLinearEquiv.nnnorm_symm_pos {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₂₁] [RingHomIsometric σ₁₂] [Nontrivial E] (e : E ≃SL[σ₁₂] F) :

0 < ‖↑e.symm‖₊

source

theorem ContinuousLinearEquiv.subsingleton_or_norm_symm_pos {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₂₁] [RingHomIsometric σ₁₂] (e : E ≃SL[σ₁₂] F) :

Subsingleton E ∨ 0 < ‖↑e.symm‖

source

theorem ContinuousLinearEquiv.subsingleton_or_nnnorm_symm_pos {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₂₁] [RingHomIsometric σ₁₂] (e : E ≃SL[σ₁₂] F) :

Subsingleton E ∨ 0 < ‖↑e.symm‖₊

source

@[simp]

theorem ContinuousLinearEquiv.coord_norm (𝕜 : Type u_1) {E : Type u_5} [NormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] (x : E) (h : x ≠ 0) :

‖coord 𝕜 x h‖ = ‖x‖⁻¹

source

noncomputable def IsCoercive {E : Type u_5} [SeminormedAddCommGroup E] [NormedSpace ℝ 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

IsCoercive B = ∃ (C : ℝ), 0 < C ∧ ∀ (u : E), C * ‖u‖ * ‖u‖ ≤ (B u) u

Instances For

source

theorem NormedSpace.equicontinuous_TFAE {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} {ι : Type u_9} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] (f : ι → E →SL[σ₁₂] F) :

[EquicontinuousAt (DFunLike.coe ∘ f) 0, Equicontinuous (DFunLike.coe ∘ f), UniformEquicontinuous (DFunLike.coe ∘ f), ∃ (C : ℝ), ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖, ∃ C ≥ 0, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖, ∃ (C : ℝ), ∀ (i : ι), ‖f i‖ ≤ C, ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C, BddAbove (Set.range fun (x : ι) => ‖f x‖), ⨆ (i : ι), ↑‖f i‖₊ < ⊤].TFAE

Equivalent characterizations for equicontinuity of a family of continuous linear maps between normed spaces. See also WithSeminorms.equicontinuous_TFAE for similar characterizations between spaces satisfying WithSeminorms.

source

def LinearIsometry.single {ι : Type u_9} [Fintype ι] [DecidableEq ι] (𝕜 : Type u_10) [NontriviallyNormedField 𝕜] (E : ι → Type u_11) [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] (i : ι) :

E i →ₗᵢ[𝕜] (j : ι) → E j

The injection x ↦ Pi.single i x as a linear isometry.

Equations

LinearIsometry.single 𝕜 E i = (LinearMap.single 𝕜 E i).toLinearIsometry ⋯

Instances For

source

theorem ContinuousLinearMap.norm_single_le_one {ι : Type u_9} [Fintype ι] [DecidableEq ι] (𝕜 : Type u_10) [NontriviallyNormedField 𝕜] (E : ι → Type u_11) [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] (i : ι) :

‖single 𝕜 E i‖ ≤ 1

source

theorem ContinuousLinearMap.norm_single {ι : Type u_9} [Fintype ι] [DecidableEq ι] (𝕜 : Type u_10) [NontriviallyNormedField 𝕜] (E : ι → Type u_11) [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] (i : ι) [NontrivialTopology (E i)] :

‖single 𝕜 E i‖ = 1

source

def LinearIsometry.inl (𝕜 : Type u_9) [NontriviallyNormedField 𝕜] (E : Type u_10) (F : Type u_11) [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] :

E →ₗᵢ[𝕜] E × F

The injection x ↦ LinearMap.inl E F x as a linear isometry.

Equations

LinearIsometry.inl 𝕜 E F = (LinearMap.inl 𝕜 E F).toLinearIsometry ⋯

Instances For

source

@[simp]

theorem LinearIsometry.inl_apply (𝕜 : Type u_9) [NontriviallyNormedField 𝕜] (E : Type u_10) (F : Type u_11) [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (x : E) :

(LinearIsometry.inl 𝕜 E F) x = (x, 0)

source

def LinearIsometry.inr (𝕜 : Type u_9) [NontriviallyNormedField 𝕜] (E : Type u_10) (F : Type u_11) [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] :

F →ₗᵢ[𝕜] E × F

The injection x ↦ LinearMap.inr E F x as a linear isometry.

Equations

LinearIsometry.inr 𝕜 E F = (LinearMap.inr 𝕜 E F).toLinearIsometry ⋯

Instances For

source

@[simp]

theorem LinearIsometry.inr_apply (𝕜 : Type u_9) [NontriviallyNormedField 𝕜] (E : Type u_10) (F : Type u_11) [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (y : F) :

(LinearIsometry.inr 𝕜 E F) y = (0, y)

source

theorem ContinuousLinearMap.norm_inl_le_one (𝕜 : Type u_9) [NontriviallyNormedField 𝕜] (E : Type u_10) (F : Type u_11) [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] :

‖inl 𝕜 E F‖ ≤ 1

source

theorem ContinuousLinearMap.norm_inr_le_one (𝕜 : Type u_9) [NontriviallyNormedField 𝕜] (E : Type u_10) (F : Type u_11) [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] :

‖inr 𝕜 E F‖ ≤ 1

source

theorem ContinuousLinearMap.norm_inl (𝕜 : Type u_9) [NontriviallyNormedField 𝕜] (E : Type u_10) (F : Type u_11) [SeminormedAddCommGroup E] [NontrivialTopology E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] :

‖inl 𝕜 E F‖ = 1

source

theorem ContinuousLinearMap.norm_inr (𝕜 : Type u_9) [NontriviallyNormedField 𝕜] (E : Type u_10) (F : Type u_11) [SeminormedAddCommGroup E] [NontrivialTopology E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [NontrivialTopology F] :

‖inr 𝕜 E F‖ = 1

Documentation

Mathlib.Analysis.Normed.Operator.NormedSpace

Operator norm for maps on normed spaces #

Composition with isometries #