opNorm_eq_of_bounds — Mathlib

English

If there exists M ≥ 0 bounding ∥f x∥ ≤ M ∥x∥ for all x, and M is the least such bound, then ∥f∥ = M.

Русский

Если существует минимальная граница M ≥ 0 такая, что ∥f x∥ ≤ M ∥x∥ для всех x, тогда ∥f∥ = M.

LaTeX

$$$\\|f\\| = M \\quad\\text{при } M \\ge 0, \\forall x, \\|f x\\| \\le M \\|x\\| \\text{ и минимальности } M$$$

Lean4

theorem opNorm_eq_of_bounds {φ : E →SL[σ₁₂] F} {M : ℝ} (M_nonneg : 0 ≤ M) (h_above : ∀ x, ‖φ x‖ ≤ M * ‖x‖)
    (h_below : ∀ N ≥ 0, (∀ x, ‖φ x‖ ≤ N * ‖x‖) → M ≤ N) : ‖φ‖ = M :=
  le_antisymm (φ.opNorm_le_bound M_nonneg h_above)
    ((le_csInf_iff ContinuousLinearMap.bounds_bddBelow ⟨M, M_nonneg, h_above⟩).mpr fun N ⟨N_nonneg, hN⟩ =>
      h_below N N_nonneg hN)

Похожие утверждения