English
There exists a universal bound C such that for any u, there is a bound relating the NN-norm of u to the basis norm and M.
Русский
Существует общий предел C, который обеспечивает связь между NN-нормой u и базисной нормой.
LaTeX
$$$\exists C>0,\; \forall {u},\; \forall M,\; (\forall i, \|u(v_i)\|_+ \le M) \Rightarrow \|u\|_+ ≤ C·M$$$
Lean4
/-- A weaker version of `Basis.opNNNorm_le` that abstracts away the value of `C`. -/
theorem exists_opNNNorm_le {ι : Type*} [Finite ι] (v : Basis ι 𝕜 E) :
∃ C > (0 : ℝ≥0), ∀ {u : E →L[𝕜] F} (M : ℝ≥0), (∀ i, ‖u (v i)‖₊ ≤ M) → ‖u‖₊ ≤ C * M :=
by
cases nonempty_fintype ι
exact
⟨max (Fintype.card ι • ‖v.equivFunL.toContinuousLinearMap‖₊) 1, zero_lt_one.trans_le (le_max_right _ _),
fun {u} M hu => (v.opNNNorm_le M hu).trans <| mul_le_mul_of_nonneg_right (le_max_left _ _) (zero_le M)⟩
