Documentation

Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm

Operator norm as an NNNorm #

Operator norm as an NNNorm, i.e. taking values in non-negative reals.

source
theorem ContinuousLinearMap.nnnorm_def {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) :
‖f‖₊ = sInf {c : NNReal | ∀ (x : E), ‖f x‖₊ ≤ c * ‖x‖₊}
source
@[simp]
theorem ContinuousLinearMap.opNNNorm_subsingleton {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [Subsingleton E] (f : E →SL[σ₁₂] F) :
‖f‖₊ = 0
source
theorem ContinuousLinearMap.opNNNorm_le_bound {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) (M : NNReal) (hM : ∀ (x : E), ‖f x‖₊ ≤ M * ‖x‖₊) :
‖f‖₊ ≤ M

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

source
theorem ContinuousLinearMap.opNNNorm_le_bound' {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) (M : NNReal) (hM : ∀ (x : E), ‖x‖₊ ≠ 0 → ‖f x‖₊ ≤ M * ‖x‖₊) :
‖f‖₊ ≤ M

If one controls the norm of every A x, ‖x‖₊ ≠ 0, then one controls the norm of A.

source
theorem ContinuousLinearMap.opNNNorm_le_of_unit_nnnorm {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [NormedAlgebra ℝ 𝕜] {f : E →SL[σ₁₂] F} {C : NNReal} (hf : ∀ (x : E), ‖x‖₊ = 1 → ‖f x‖₊ ≤ C) :
‖f‖₊ ≤ C

For a continuous real linear map f, if one controls the norm of every f x, ‖x‖₊ = 1, then one controls the norm of f.

source
theorem ContinuousLinearMap.opNNNorm_le_of_lipschitz {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {f : E →SL[σ₁₂] F} {K : NNReal} (hf : LipschitzWith K ⇑f) :
‖f‖₊ ≤ K
source
theorem ContinuousLinearMap.opNNNorm_eq_of_bounds {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {φ : E →SL[σ₁₂] F} (M : NNReal) (h_above : ∀ (x : E), ‖φ x‖₊ ≤ M * ‖x‖₊) (h_below : ∀ (N : NNReal), (∀ (x : E), ‖φ x‖₊ ≤ N * ‖x‖₊) → M ≤ N) :
‖φ‖₊ = M
source
theorem ContinuousLinearMap.opNNNorm_le_iff {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {f : E →SL[σ₁₂] F} {C : NNReal} :
‖f‖₊ ≤ C ↔ ∀ (x : E), ‖f x‖₊ ≤ C * ‖x‖₊
source
theorem ContinuousLinearMap.isLeast_opNNNorm {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) :
IsLeast {C : NNReal | ∀ (x : E), ‖f x‖₊ ≤ C * ‖x‖₊} ‖f‖₊
source
theorem ContinuousLinearMap.opNNNorm_comp_le {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomIsometric σ₁₂] [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] (h : F →SL[σ₂₃] G) (f : E →SL[σ₁₂] F) :
‖h.comp f‖₊ ≤ ‖h‖₊ * ‖f‖₊
source
theorem ContinuousLinearMap.opENorm_comp_le {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomIsometric σ₁₂] [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] (h : F →SL[σ₂₃] G) (f : E →SL[σ₁₂] F) :
‖h.comp f‖ₑ ≤ ‖h‖ₑ * ‖f‖ₑ
source
theorem ContinuousLinearMap.le_opNNNorm {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) (x : E) :
‖f x‖₊ ≤ ‖f‖₊ * ‖x‖₊
source
theorem ContinuousLinearMap.le_opENorm {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) (x : E) :
‖f x‖ₑ ≤ ‖f‖ₑ * ‖x‖ₑ
source
theorem ContinuousLinearMap.nndist_le_opNNNorm {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) (x y : E) :
nndist (f x) (f y) ≤ ‖f‖₊ * nndist x y
source
theorem ContinuousLinearMap.lipschitz {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) :
LipschitzWith ‖f‖₊ ⇑f

continuous linear maps are Lipschitz continuous.

source
theorem ContinuousLinearMap.lipschitz_apply {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (x : E) :
LipschitzWith ‖x‖₊ fun (f : E →SL[σ₁₂] F) => f x

Evaluation of a continuous linear map f at a point is Lipschitz continuous in f.

source
theorem ContinuousLinearMap.exists_mul_lt_apply_of_lt_opNNNorm {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) {r : NNReal} (hr : r < ‖f‖₊) :
∃ (x : E), r * ‖x‖₊ < ‖f x‖₊
source
theorem ContinuousLinearMap.exists_mul_lt_of_lt_opNorm {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) {r : ℝ} (hr₀ : 0 ≤ r) (hr : r < ‖f‖) :
∃ (x : E), r * ‖x‖ < ‖f x‖
source
theorem ContinuousLinearEquiv.lipschitz {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (e : E ≃SL[σ₁₂] F) :
LipschitzWith ‖↑e‖₊ ⇑e
source
theorem ContinuousLinearMap.exists_lt_apply_of_lt_opNNNorm {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [SeminormedAddCommGroup F] [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) {r : NNReal} (hr : r < ‖f‖₊) :
∃ (x : E), ‖x‖₊ < 1 ∧ r < ‖f x‖₊
source
theorem ContinuousLinearMap.exists_lt_apply_of_lt_opNorm {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [SeminormedAddCommGroup F] [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) {r : ℝ} (hr : r < ‖f‖) :
∃ (x : E), ‖x‖ < 1 ∧ r < ‖f x‖
source
theorem ContinuousLinearMap.sSup_unit_ball_eq_nnnorm {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [SeminormedAddCommGroup F] [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) :
sSup ((fun (x : E) => ‖f x‖₊) '' Metric.ball 0 1) = ‖f‖₊
source
theorem ContinuousLinearMap.sSup_unit_ball_eq_norm {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [SeminormedAddCommGroup F] [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) :
sSup ((fun (x : E) => ‖f x‖) '' Metric.ball 0 1) = ‖f‖
source
theorem ContinuousLinearMap.sSup_unitClosedBall_eq_nnnorm {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [SeminormedAddCommGroup F] [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) :
sSup ((fun (x : E) => ‖f x‖₊) '' Metric.closedBall 0 1) = ‖f‖₊
source
theorem ContinuousLinearMap.sSup_unitClosedBall_eq_norm {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [SeminormedAddCommGroup F] [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) :
sSup ((fun (x : E) => ‖f x‖) '' Metric.closedBall 0 1) = ‖f‖
source
theorem ContinuousLinearMap.exists_nnnorm_eq_one_lt_apply_of_lt_opNNNorm {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [SeminormedAddCommGroup F] [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [NormedAlgebra ℝ 𝕜] (f : E →SL[σ₁₂] F) {r : NNReal} (hr : r < ‖f‖₊) :
∃ (x : E), ‖x‖₊ = 1 ∧ r < ‖f x‖₊
source
theorem ContinuousLinearMap.sSup_sphere_eq_nnnorm {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [SeminormedAddCommGroup F] [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [NormedAlgebra ℝ 𝕜] (f : E →SL[σ₁₂] F) :
sSup ((fun (x : E) => ‖f x‖₊) '' Metric.sphere 0 1) = ‖f‖₊

When the domain is a real normed space, ContinuousLinearMap.sSup_unitClosedBall_eq_nnnorm can be tightened to take the supremum over only the Metric.sphere.

source
theorem ContinuousLinearMap.sSup_sphere_eq_norm {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [SeminormedAddCommGroup F] [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [NormedAlgebra ℝ 𝕜] (f : E →SL[σ₁₂] F) :
sSup ((fun (x : E) => ‖f x‖) '' Metric.sphere 0 1) = ‖f‖

When the domain is a real normed space, ContinuousLinearMap.sSup_unitClosedBall_eq_norm can be tightened to take the supremum over only the Metric.sphere.