doc-next-gen

Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm

Module docstring

{"# Operator norm as an NNNorm

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

"}

ContinuousLinearMap.nnnorm_def theorem
(f : E →SL[σ₁₂] F) : ‖f‖₊ = sInf {c | ∀ x, ‖f x‖₊ ≤ c * ‖x‖₊}
Full source 
theorem nnnorm_def (f : E →SL[σ₁₂] F) : ‖f‖₊ = sInf { c | ∀ x, ‖f x‖₊ ≤ c * ‖x‖₊ } := by
  ext
  rw [NNReal.coe_sInf, coe_nnnorm, norm_def, NNReal.coe_image]
  simp_rw [← NNReal.coe_le_coe, NNReal.coe_mul, coe_nnnorm, mem_setOf_eq, NNReal.coe_mk,
    exists_prop]
Definition of Operator Seminorm for Continuous Semilinear Maps
Informal description
For a continuous semilinear map $f \colon E \to F$ between seminormed additive commutative groups, the operator seminorm $\|f\|_{\nn}$ is defined as the infimum of the set of nonnegative real numbers $c$ such that $\|f(x)\|_{\nn} \leq c \cdot \|x\|_{\nn}$ for all $x \in E$, where $\|\cdot\|_{\nn}$ denotes the nonnegative real-valued seminorm.
ContinuousLinearMap.opNNNorm_le_bound theorem
(f : E →SL[σ₁₂] F) (M : ℝ≥0) (hM : ∀ x, ‖f x‖₊ ≤ M * ‖x‖₊) : ‖f‖₊ ≤ M
Full source 
/-- If one controls the norm of every `A x`, then one controls the norm of `A`. -/
theorem opNNNorm_le_bound (f : E →SL[σ₁₂] F) (M : ℝ≥0) (hM : ∀ x, ‖f x‖₊ ≤ M * ‖x‖₊) : ‖f‖₊ ≤ M :=
  opNorm_le_bound f (zero_le M) hM
Operator Norm Bounded by Uniform Estimate in Non-Negative Reals
Informal description
Let $E$ and $F$ be seminormed additive commutative groups, and let $f \colon E \to F$ be a continuous semilinear map. For any nonnegative real number $M \geq 0$ such that $\|f(x)\| \leq M \cdot \|x\|$ holds for all $x \in E$, the operator norm of $f$ satisfies $\|f\| \leq M$.
ContinuousLinearMap.opNNNorm_le_bound' theorem
(f : E →SL[σ₁₂] F) (M : ℝ≥0) (hM : ∀ x, ‖x‖₊ ≠ 0 → ‖f x‖₊ ≤ M * ‖x‖₊) : ‖f‖₊ ≤ M
Full source 
/-- If one controls the norm of every `A x`, `‖x‖₊ ≠ 0`, then one controls the norm of `A`. -/
theorem opNNNorm_le_bound' (f : E →SL[σ₁₂] F) (M : ℝ≥0) (hM : ∀ x, ‖x‖₊‖x‖₊ ≠ 0 → ‖f x‖₊ ≤ M * ‖x‖₊) :
    ‖f‖₊ ≤ M :=
  opNorm_le_bound' f (zero_le M) fun x hx => hM x <| by rwa [← NNReal.coe_ne_zero]
Operator Norm Bound via Nonzero Vectors: $\|f\| \leq M$
Informal description
Let $E$ and $F$ be seminormed additive commutative groups, and let $\sigma_{12}$ be a ring homomorphism. For any continuous $\sigma_{12}$-semilinear map $f \colon E \to F$ and any nonnegative real number $M \geq 0$, if $\|f(x)\| \leq M \cdot \|x\|$ holds for all $x \in E$ with $\|x\| \neq 0$, then the operator norm of $f$ satisfies $\|f\| \leq M$.
ContinuousLinearMap.opNNNorm_le_of_unit_nnnorm theorem
[NormedSpace ℝ E] [NormedSpace ℝ F] {f : E →L[ℝ] F} {C : ℝ≥0} (hf : ∀ x, ‖x‖₊ = 1 → ‖f x‖₊ ≤ C) : ‖f‖₊ ≤ C
Full source 
/-- For a continuous real linear map `f`, if one controls the norm of every `f x`, `‖x‖₊ = 1`, then
one controls the norm of `f`. -/
theorem opNNNorm_le_of_unit_nnnorm [NormedSpace ℝ E] [NormedSpace ℝ F] {f : E →L[ℝ] F} {C : ℝ≥0}
    (hf : ∀ x, ‖x‖₊ = 1 → ‖f x‖₊ ≤ C) : ‖f‖₊ ≤ C :=
  opNorm_le_of_unit_norm C.coe_nonneg fun x hx => hf x <| by rwa [← NNReal.coe_eq_one]
Operator Norm Bound via Unit Vectors: $\|f\| \leq C$
Informal description
Let $E$ and $F$ be real normed spaces, and let $f \colon E \to F$ be a continuous linear map. If for every $x \in E$ with $\|x\| = 1$ we have $\|f(x)\| \leq C$ for some nonnegative real number $C \geq 0$, then the operator norm of $f$ satisfies $\|f\| \leq C$.
ContinuousLinearMap.opNNNorm_le_of_lipschitz theorem
{f : E →SL[σ₁₂] F} {K : ℝ≥0} (hf : LipschitzWith K f) : ‖f‖₊ ≤ K
Full source 
theorem opNNNorm_le_of_lipschitz {f : E →SL[σ₁₂] F} {K : ℝ≥0} (hf : LipschitzWith K f) :
    ‖f‖₊ ≤ K :=
  opNorm_le_of_lipschitz hf
Operator Norm Bound via Lipschitz Constant: $\|f\| \leq K$
Informal description
Let $E$ and $F$ be seminormed additive commutative groups, and let $f \colon E \to F$ be a continuous $\sigma_{12}$-semilinear map. If $f$ is Lipschitz continuous with constant $K \geq 0$, then the operator norm of $f$ satisfies $\|f\| \leq K$.
ContinuousLinearMap.opNNNorm_eq_of_bounds theorem
{φ : E →SL[σ₁₂] F} (M : ℝ≥0) (h_above : ∀ x, ‖φ x‖₊ ≤ M * ‖x‖₊) (h_below : ∀ N, (∀ x, ‖φ x‖₊ ≤ N * ‖x‖₊) → M ≤ N) : ‖φ‖₊ = M
Full source 
theorem opNNNorm_eq_of_bounds {φ : E →SL[σ₁₂] F} (M : ℝ≥0) (h_above : ∀ x, ‖φ x‖₊ ≤ M * ‖x‖₊)
    (h_below : ∀ N, (∀ x, ‖φ x‖₊ ≤ N * ‖x‖₊) → M ≤ N) : ‖φ‖₊ = M :=
  Subtype.ext <| opNorm_eq_of_bounds (zero_le M) h_above <| Subtype.forall'.mpr h_below
Characterization of Operator Norm via Optimal Bounds: $\|\varphi\| = M$
Informal description
Let $E$ and $F$ be seminormed additive commutative groups, and let $\varphi \colon E \to F$ be a continuous $\sigma_{12}$-semilinear map. Given a nonnegative real number $M \geq 0$ such that: 1. $\|\varphi(x)\| \leq M \cdot \|x\|$ for all $x \in E$, and 2. For any nonnegative real number $N$, if $\|\varphi(x)\| \leq N \cdot \|x\|$ for all $x \in E$, then $M \leq N$, then the operator norm of $\varphi$ satisfies $\|\varphi\| = M$.
ContinuousLinearMap.opNNNorm_le_iff theorem
{f : E →SL[σ₁₂] F} {C : ℝ≥0} : ‖f‖₊ ≤ C ↔ ∀ x, ‖f x‖₊ ≤ C * ‖x‖₊
Full source 
theorem opNNNorm_le_iff {f : E →SL[σ₁₂] F} {C : ℝ≥0} : ‖f‖₊‖f‖₊ ≤ C ↔ ∀ x, ‖f x‖₊ ≤ C * ‖x‖₊ :=
  opNorm_le_iff C.2
Operator Norm Characterization: $\|f\| \leq C \leftrightarrow \forall x, \|f(x)\| \leq C \cdot \|x\|$
Informal description
For a continuous semilinear map $f \colon E \to F$ between seminormed additive commutative groups and a nonnegative real number $C \geq 0$, the operator norm of $f$ satisfies $\|f\| \leq C$ if and only if for every $x \in E$, the norm of $f(x)$ is bounded by $C \cdot \|x\|$, i.e., $\|f(x)\| \leq C \cdot \|x\|$.
ContinuousLinearMap.isLeast_opNNNorm theorem
: IsLeast {C : ℝ≥0 | ∀ x, ‖f x‖₊ ≤ C * ‖x‖₊} ‖f‖₊
Full source 
theorem isLeast_opNNNorm : IsLeast {C : ℝ≥0 | ∀ x, ‖f x‖₊ ≤ C * ‖x‖₊} ‖f‖₊ := by
  simpa only [← opNNNorm_le_iff] using isLeast_Ici
Operator Norm is the Least Upper Bound on the Norm Ratio $\frac{\|f(x)\|}{\|x\|}$
Informal description
For a continuous linear map $f \colon E \to F$, the operator norm $\|f\|_{\text{op}}$ is the least non-negative real number $C$ such that $\|f(x)\| \leq C \|x\|$ for all $x \in E$. In other words, $\|f\|_{\text{op}}$ is the infimum of the set $\{C \in \mathbb{R}_{\geq 0} \mid \forall x \in E, \|f(x)\| \leq C \|x\|\}$.
ContinuousLinearMap.opNNNorm_comp_le theorem
[RingHomIsometric σ₁₃] (f : E →SL[σ₁₂] F) : ‖h.comp f‖₊ ≤ ‖h‖₊ * ‖f‖₊
Full source 
theorem opNNNorm_comp_le [RingHomIsometric σ₁₃] (f : E →SL[σ₁₂] F) : ‖h.comp f‖₊ ≤ ‖h‖₊ * ‖f‖₊ :=
  opNorm_comp_le h f
Submultiplicativity of Non-Negative Operator Seminorm under Composition: $\|h \circ f\|_{\mathbb{R}_{\geq 0}} \leq \|h\|_{\mathbb{R}_{\geq 0}} \cdot \|f\|_{\mathbb{R}_{\geq 0}}$
Informal description
Let $E$, $F$, and $G$ be seminormed additive commutative groups, and let $f \colon E \to F$ and $h \colon F \to G$ be continuous semilinear maps. The operator seminorm of the composition $h \circ f$ satisfies $\|h \circ f\|_{\mathbb{R}_{\geq 0}} \leq \|h\|_{\mathbb{R}_{\geq 0}} \cdot \|f\|_{\mathbb{R}_{\geq 0}}$, where $\|\cdot\|_{\mathbb{R}_{\geq 0}}$ denotes the non-negative real-valued operator seminorm.
ContinuousLinearMap.opENorm_comp_le theorem
[RingHomIsometric σ₁₃] (f : E →SL[σ₁₂] F) : ‖h.comp f‖ₑ ≤ ‖h‖ₑ * ‖f‖ₑ
Full source 
lemma opENorm_comp_le [RingHomIsometric σ₁₃] (f : E →SL[σ₁₂] F) : ‖h.comp f‖ₑ ≤ ‖h‖ₑ * ‖f‖ₑ := by
  simpa [enorm, ← ENNReal.coe_mul] using opNNNorm_comp_le h f
Submultiplicativity of Operator Seminorm under Composition: $\|h \circ f\| \leq \|h\| \cdot \|f\|$
Informal description
Let $E$, $F$, and $G$ be seminormed additive commutative groups, and let $f \colon E \to F$ and $h \colon F \to G$ be continuous semilinear maps. The operator seminorm of the composition $h \circ f$ satisfies $\|h \circ f\| \leq \|h\| \cdot \|f\|$, where $\|\cdot\|$ denotes the operator seminorm.
ContinuousLinearMap.le_opNNNorm theorem
: ‖f x‖₊ ≤ ‖f‖₊ * ‖x‖₊
Full source 
theorem le_opNNNorm : ‖f x‖₊ ≤ ‖f‖₊ * ‖x‖₊ :=
  f.le_opNorm x
Non-negative operator norm bound: $\|f(x)\|_{\mathbb{R}_{\geq 0}} \leq \|f\|_{\mathbb{R}_{\geq 0}} \cdot \|x\|_{\mathbb{R}_{\geq 0}}$
Informal description
For any continuous semilinear map $f \colon E \to F$ between seminormed additive commutative groups and any element $x \in E$, the non-negative real norm of $f(x)$ is bounded by the product of the operator norm of $f$ (as a non-negative real) and the non-negative real norm of $x$, i.e., $\|f(x)\|_{\mathbb{R}_{\geq 0}} \leq \|f\|_{\mathbb{R}_{\geq 0}} \cdot \|x\|_{\mathbb{R}_{\geq 0}}$.
ContinuousLinearMap.le_opENorm theorem
: ‖f x‖ₑ ≤ ‖f‖ₑ * ‖x‖ₑ
Full source 
lemma le_opENorm : ‖f x‖ₑ ≤ ‖f‖ₑ * ‖x‖ₑ := by dsimp [enorm]; exact mod_cast le_opNNNorm ..
Operator Norm Bound: $\|f(x)\|_e \leq \|f\|_e \cdot \|x\|_e$
Informal description
For any continuous semilinear map $f \colon E \to F$ between seminormed additive commutative groups and any element $x \in E$, the extended norm of $f(x)$ is bounded by the product of the operator norm of $f$ and the extended norm of $x$, i.e., $\|f(x)\|_e \leq \|f\|_e \cdot \|x\|_e$.
ContinuousLinearMap.nndist_le_opNNNorm theorem
(x y : E) : nndist (f x) (f y) ≤ ‖f‖₊ * nndist x y
Full source 
theorem nndist_le_opNNNorm (x y : E) : nndist (f x) (f y) ≤ ‖f‖₊ * nndist x y :=
  dist_le_opNorm f x y
Non-Negative Distance Bound via Operator Seminorm: $\text{nndist}(f(x), f(y)) \leq \|f\|_+ \cdot \text{nndist}(x, y)$
Informal description
For any continuous semilinear map $f \colon E \to F$ between seminormed additive commutative groups and any elements $x, y \in E$, the non-negative distance between $f(x)$ and $f(y)$ is bounded by the product of the operator seminorm of $f$ and the non-negative distance between $x$ and $y$, i.e., $\text{nndist}(f(x), f(y)) \leq \|f\|_+ \cdot \text{nndist}(x, y)$.
ContinuousLinearMap.lipschitz theorem
: LipschitzWith ‖f‖₊ f
Full source 
/-- continuous linear maps are Lipschitz continuous. -/
theorem lipschitz : LipschitzWith ‖f‖₊ f :=
  AddMonoidHomClass.lipschitz_of_bound_nnnorm f _ f.le_opNNNorm
Lipschitz continuity of continuous semilinear maps with operator norm bound
Informal description
Every continuous semilinear map $f \colon E \to F$ between seminormed additive commutative groups is Lipschitz continuous with Lipschitz constant $\|f\|_{\mathbb{R}_{\geq 0}}$, where $\|f\|_{\mathbb{R}_{\geq 0}}$ denotes the operator norm of $f$ as a non-negative real number.
ContinuousLinearMap.lipschitz_apply theorem
(x : E) : LipschitzWith ‖x‖₊ fun f : E →SL[σ₁₂] F => f x
Full source 
/-- Evaluation of a continuous linear map `f` at a point is Lipschitz continuous in `f`. -/
theorem lipschitz_apply (x : E) : LipschitzWith ‖x‖₊ fun f : E →SL[σ₁₂] F => f x :=
  lipschitzWith_iff_norm_sub_le.2 fun f g => ((f - g).le_opNorm x).trans_eq (mul_comm _ _)
Lipschitz Continuity of Evaluation at $x$ with Constant $\|x\|$
Informal description
For any element $x$ in a seminormed additive commutative group $E$, the map $f \mapsto f(x)$ from continuous semilinear maps $E \to F$ to $F$ is Lipschitz continuous with Lipschitz constant $\|x\|$, where $\|x\|$ denotes the norm of $x$.
ContinuousLinearMap.exists_mul_lt_apply_of_lt_opNNNorm theorem
(f : E →SL[σ₁₂] F) {r : ℝ≥0} (hr : r < ‖f‖₊) : ∃ x, r * ‖x‖₊ < ‖f x‖₊
Full source 
theorem exists_mul_lt_apply_of_lt_opNNNorm (f : E →SL[σ₁₂] F) {r : ℝ≥0} (hr : r < ‖f‖₊) :
    ∃ x, r * ‖x‖₊ < ‖f x‖₊ := by
  simpa only [not_forall, not_le, Set.mem_setOf] using
    not_mem_of_lt_csInf (nnnorm_def f ▸ hr : r < sInf { c : ℝ≥0 | ∀ x, ‖f x‖₊ ≤ c * ‖x‖₊ })
      (OrderBot.bddBelow _)
Existence of Element with Scaled Norm Below Operator Norm for Continuous Semilinear Maps
Informal description
Let $E$ and $F$ be seminormed additive commutative groups, and let $f \colon E \to F$ be a continuous semilinear map. For any nonnegative real number $r$ such that $r < \|f\|_{\nn}$, there exists an element $x \in E$ such that $r \cdot \|x\|_{\nn} < \|f(x)\|_{\nn}$, where $\|\cdot\|_{\nn}$ denotes the nonnegative real-valued seminorm.
ContinuousLinearMap.exists_mul_lt_of_lt_opNorm theorem
(f : E →SL[σ₁₂] F) {r : ℝ} (hr₀ : 0 ≤ r) (hr : r < ‖f‖) : ∃ x, r * ‖x‖ < ‖f x‖
Full source 
theorem exists_mul_lt_of_lt_opNorm (f : E →SL[σ₁₂] F) {r : ℝ} (hr₀ : 0 ≤ r) (hr : r < ‖f‖) :
    ∃ x, r * ‖x‖ < ‖f x‖ := by
  lift r to ℝ≥0 using hr₀
  exact f.exists_mul_lt_apply_of_lt_opNNNorm hr
Existence of Element with Scaled Norm Below Operator Norm for Continuous Semilinear Maps (Real Version)
Informal description
Let $E$ and $F$ be seminormed additive commutative groups, and let $f \colon E \to F$ be a continuous semilinear map. For any real number $r \geq 0$ such that $r < \|f\|$, there exists an element $x \in E$ such that $r \cdot \|x\| < \|f(x)\|$, where $\|\cdot\|$ denotes the norm.
ContinuousLinearMap.exists_lt_apply_of_lt_opNNNorm theorem
{𝕜 𝕜₂ E F : Type*} [NormedAddCommGroup E] [SeminormedAddCommGroup F] [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) {r : ℝ≥0} (hr : r < ‖f‖₊) : ∃ x : E, ‖x‖₊ < 1 ∧ r < ‖f x‖₊
Full source 
theorem exists_lt_apply_of_lt_opNNNorm {𝕜 𝕜₂ E F : Type*} [NormedAddCommGroup E]
    [SeminormedAddCommGroup F] [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂}
    [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) {r : ℝ≥0}
    (hr : r < ‖f‖₊) : ∃ x : E, ‖x‖₊ < 1 ∧ r < ‖f x‖₊ := by
  obtain ⟨y, hy⟩ := f.exists_mul_lt_apply_of_lt_opNNNorm hr
  have hy' : ‖y‖₊‖y‖₊ ≠ 0 :=
    nnnorm_ne_zero_iff.2 fun heq => by
      simp [heq, nnnorm_zero, map_zero, not_lt_zero'] at hy
  have hfy : ‖f y‖₊‖f y‖₊ ≠ 0 := (zero_le'.trans_lt hy).ne'
  rw [← inv_inv ‖f y‖₊, NNReal.lt_inv_iff_mul_lt (inv_ne_zero hfy), mul_assoc, mul_comm ‖y‖₊, ←
    mul_assoc, ← NNReal.lt_inv_iff_mul_lt hy'] at hy
  obtain ⟨k, hk₁, hk₂⟩ := NormedField.exists_lt_nnnorm_lt 𝕜 hy
  refine ⟨k • y, (nnnorm_smul k y).symm ▸ (NNReal.lt_inv_iff_mul_lt hy').1 hk₂, ?_⟩
  have : ‖σ₁₂ k‖₊ = ‖k‖₊ := Subtype.ext RingHomIsometric.is_iso
  rwa [map_smulₛₗ f, nnnorm_smul, ← div_lt_iff₀ hfy.bot_lt, div_eq_mul_inv, this]
Existence of Unit Ball Element with Norm Below Operator Norm for Continuous Semilinear Maps
Informal description
Let $E$ and $F$ be normed spaces over fields $\mathbb{K}$ and $\mathbb{K}_2$ respectively, with a ring homomorphism $\sigma_{12} \colon \mathbb{K} \to \mathbb{K}_2$ that is isometric. Given a continuous semilinear map $f \colon E \to F$ with respect to $\sigma_{12}$ and a nonnegative real number $r$ such that $r < \|f\|_{\nn}$, there exists an element $x \in E$ with $\|x\|_{\nn} < 1$ and $r < \|f(x)\|_{\nn}$, where $\|\cdot\|_{\nn}$ denotes the nonnegative real-valued seminorm.
ContinuousLinearMap.exists_lt_apply_of_lt_opNorm theorem
{𝕜 𝕜₂ E F : Type*} [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‖
Full source 
theorem exists_lt_apply_of_lt_opNorm {𝕜 𝕜₂ E F : Type*} [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‖ := by
  by_cases hr₀ : r < 0
  · exact ⟨0, by simpa using hr₀⟩
  · lift r to ℝ≥0 using not_lt.1 hr₀
    exact f.exists_lt_apply_of_lt_opNNNorm hr
Existence of Unit Ball Element with Norm Below Operator Norm for Continuous Semilinear Maps (Real Version)
Informal description
Let $E$ and $F$ be normed vector spaces over the densely normed fields $\mathbb{K}$ and $\mathbb{K}_2$ respectively, with an isometric ring homomorphism $\sigma_{12} \colon \mathbb{K} \to \mathbb{K}_2$. Given a continuous $\sigma_{12}$-semilinear map $f \colon E \to F$ and a real number $r$ such that $r < \|f\|$, there exists an element $x \in E$ with $\|x\| < 1$ and $r < \|f(x)\|$, where $\|\cdot\|$ denotes the norm on the respective spaces.
ContinuousLinearMap.sSup_unit_ball_eq_nnnorm theorem
{𝕜 𝕜₂ E F : Type*} [NormedAddCommGroup E] [SeminormedAddCommGroup F] [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) : sSup ((fun x => ‖f x‖₊) '' ball 0 1) = ‖f‖₊
Full source 
theorem sSup_unit_ball_eq_nnnorm {𝕜 𝕜₂ E F : Type*} [NormedAddCommGroup E]
    [SeminormedAddCommGroup F] [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂}
    [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) :
    sSup ((fun x => ‖f x‖₊) '' ball 0 1) = ‖f‖₊ := by
  refine csSup_eq_of_forall_le_of_forall_lt_exists_gt ((nonempty_ball.mpr zero_lt_one).image _) ?_
    fun ub hub => ?_
  · rintro - ⟨x, hx, rfl⟩
    simpa only [mul_one] using f.le_opNorm_of_le (mem_ball_zero_iff.1 hx).le
  · obtain ⟨x, hx, hxf⟩ := f.exists_lt_apply_of_lt_opNNNorm hub
    exact ⟨_, ⟨x, mem_ball_zero_iff.2 hx, rfl⟩, hxf⟩
Operator Norm as Supremum over Unit Ball: $\sup_{\|x\|_{\nn} < 1} \|f(x)\|_{\nn} = \|f\|_{\nn}$
Informal description
Let $E$ and $F$ be normed spaces over fields $\mathbb{K}$ and $\mathbb{K}_2$ respectively, with a ring homomorphism $\sigma_{12} \colon \mathbb{K} \to \mathbb{K}_2$ that is isometric. For any continuous semilinear map $f \colon E \to F$ with respect to $\sigma_{12}$, the supremum of the set $\{\|f(x)\|_{\nn} \mid x \in E, \|x\|_{\nn} < 1\}$ equals the operator norm $\|f\|_{\nn}$, where $\|\cdot\|_{\nn}$ denotes the nonnegative real-valued seminorm.
ContinuousLinearMap.sSup_unit_ball_eq_norm theorem
{𝕜 𝕜₂ E F : Type*} [NormedAddCommGroup E] [SeminormedAddCommGroup F] [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) : sSup ((fun x => ‖f x‖) '' ball 0 1) = ‖f‖
Full source 
theorem sSup_unit_ball_eq_norm {𝕜 𝕜₂ E F : Type*} [NormedAddCommGroup E] [SeminormedAddCommGroup F]
    [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [NormedSpace 𝕜 E]
    [NormedSpace 𝕜₂ F] [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) :
    sSup ((fun x => ‖f x‖) '' ball 0 1) = ‖f‖ := by
  simpa only [NNReal.coe_sSup, Set.image_image] using NNReal.coe_inj.2 f.sSup_unit_ball_eq_nnnorm
Operator Norm Characterization via Unit Ball: $\sup_{\|x\| < 1} \|f(x)\| = \|f\|$
Informal description
Let $E$ and $F$ be normed spaces over the densely normed fields $\mathbb{K}$ and $\mathbb{K}_2$ respectively, with an isometric ring homomorphism $\sigma_{12} \colon \mathbb{K} \to \mathbb{K}_2$. For any continuous $\sigma_{12}$-semilinear map $f \colon E \to F$, the supremum of the set $\{\|f(x)\| \mid x \in E, \|x\| < 1\}$ equals the operator norm $\|f\|$.
ContinuousLinearMap.sSup_unitClosedBall_eq_nnnorm theorem
{𝕜 𝕜₂ E F : Type*} [NormedAddCommGroup E] [SeminormedAddCommGroup F] [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) : sSup ((fun x => ‖f x‖₊) '' closedBall 0 1) = ‖f‖₊
Full source 
theorem sSup_unitClosedBall_eq_nnnorm {𝕜 𝕜₂ E F : Type*} [NormedAddCommGroup E]
    [SeminormedAddCommGroup F] [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂}
    [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) :
    sSup ((fun x => ‖f x‖₊) '' closedBall 0 1) = ‖f‖₊ := by
  have hbdd : ∀ y ∈ (fun x => ‖f x‖₊) '' closedBall 0 1, y ≤ ‖f‖₊ := by
    rintro - ⟨x, hx, rfl⟩
    exact f.unit_le_opNorm x (mem_closedBall_zero_iff.1 hx)
  refine le_antisymm (csSup_le ((nonempty_closedBall.mpr zero_le_one).image _) hbdd) ?_
  rw [← sSup_unit_ball_eq_nnnorm]
  exact csSup_le_csSup ⟨‖f‖₊, hbdd⟩ ((nonempty_ball.2 zero_lt_one).image _)
    (Set.image_subset _ ball_subset_closedBall)
Operator Norm as Supremum over Closed Unit Ball: $\sup_{\|x\| \leq 1} \|f(x)\|_{\mathbb{R}_{\geq 0}} = \|f\|_{\mathbb{R}_{\geq 0}}$
Informal description
Let $E$ and $F$ be normed spaces over fields $\mathbb{K}$ and $\mathbb{K}_2$ respectively, with a ring homomorphism $\sigma_{12} \colon \mathbb{K} \to \mathbb{K}_2$ that is isometric. For any continuous semilinear map $f \colon E \to F$ with respect to $\sigma_{12}$, the supremum of the set $\{\|f(x)\|_{\mathbb{R}_{\geq 0}} \mid x \in E, \|x\| \leq 1\}$ equals the operator norm $\|f\|_{\mathbb{R}_{\geq 0}}$, where $\|\cdot\|_{\mathbb{R}_{\geq 0}}$ denotes the nonnegative real-valued seminorm.
ContinuousLinearMap.sSup_unitClosedBall_eq_norm theorem
{𝕜 𝕜₂ E F : Type*} [NormedAddCommGroup E] [SeminormedAddCommGroup F] [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) : sSup ((fun x => ‖f x‖) '' closedBall 0 1) = ‖f‖
Full source 
theorem sSup_unitClosedBall_eq_norm {𝕜 𝕜₂ E F : Type*} [NormedAddCommGroup E]
    [SeminormedAddCommGroup F] [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂}
    [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) :
    sSup ((fun x => ‖f x‖) '' closedBall 0 1) = ‖f‖ := by
  simpa only [NNReal.coe_sSup, Set.image_image] using
    NNReal.coe_inj.2 f.sSup_unitClosedBall_eq_nnnorm
Operator Norm Characterization via Closed Unit Ball: $\sup_{\|x\| \leq 1} \|f(x)\| = \|f\|$
Informal description
Let $E$ and $F$ be normed spaces over the densely normed fields $\mathbb{K}$ and $\mathbb{K}_2$ respectively, with an isometric ring homomorphism $\sigma_{12} \colon \mathbb{K} \to \mathbb{K}_2$. For any continuous $\sigma_{12}$-semilinear map $f \colon E \to F$, the supremum of the set $\{\|f(x)\| \mid x \in E, \|x\| \leq 1\}$ equals the operator norm $\|f\|$.
ContinuousLinearEquiv.lipschitz theorem
: LipschitzWith ‖(e : E →SL[σ₁₂] F)‖₊ e
Full source 
protected theorem lipschitz : LipschitzWith ‖(e : E →SL[σ₁₂] F)‖₊ e :=
  (e : E →SL[σ₁₂] F).lipschitz
Lipschitz continuity of continuous linear equivalences with operator norm bound
Informal description
Every continuous linear equivalence $e \colon E \to F$ between seminormed additive commutative groups is Lipschitz continuous with Lipschitz constant $\|e\|_{\mathbb{R}_{\geq 0}}$, where $\|e\|_{\mathbb{R}_{\geq 0}}$ denotes the operator norm of $e$ as a non-negative real number.