opNorm_le — Mathlib

English

An inequality bounding the operator norm of u in terms of a finite basis v and a scalar M.

Русский

Неравенство, ограничивающее норму оператора u через базис v и число M.

LaTeX

$$$ \|u\| ≤ Fintype.card(ι) \cdot \|v.equivFunL.toContinuousLinearMap\| \cdot M $$$

Lean4

theorem opNorm_le {ι : Type*} [Fintype ι] (v : Basis ι 𝕜 E) {u : E →L[𝕜] F} {M : ℝ} (hM : 0 ≤ M)
    (hu : ∀ i, ‖u (v i)‖ ≤ M) : ‖u‖ ≤ Fintype.card ι • ‖v.equivFunL.toContinuousLinearMap‖ * M := by
  simpa using NNReal.coe_le_coe.mpr (v.opNNNorm_le ⟨M, hM⟩ hu)

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