English
The operator norm of u is bounded by a product involving the basis cardinal and the basis operator norm.
Русский
Норма оператора u ограничена произведением, зависящим от числа базисных элементов и нормы базисного перехода.
LaTeX
$$$ \|u\| ≤ Fintype.card(ι) \cdot \|v.equivFunL.toContinuousLinearMap\| \cdot M $$$
Lean4
theorem opNNNorm_le {ι : Type*} [Fintype ι] (v : Basis ι 𝕜 E) {u : E →L[𝕜] F} (M : ℝ≥0) (hu : ∀ i, ‖u (v i)‖₊ ≤ M) :
‖u‖₊ ≤ Fintype.card ι • ‖v.equivFunL.toContinuousLinearMap‖₊ * M :=
u.opNNNorm_le_bound _ fun e => by
set φ := v.equivFunL.toContinuousLinearMap
calc
‖u e‖₊ = ‖u (∑ i, v.equivFun e i • v i)‖₊ := by rw [v.sum_equivFun]
_ = ‖∑ i, v.equivFun e i • (u <| v i)‖₊ := by simp only [equivFun_apply, map_sum, map_smul]
_ ≤ ∑ i, ‖v.equivFun e i • (u <| v i)‖₊ := (nnnorm_sum_le _ _)
_ = ∑ i, ‖v.equivFun e i‖₊ * ‖u (v i)‖₊ := by simp only [nnnorm_smul]
_ ≤ ∑ i, ‖v.equivFun e i‖₊ * M := by gcongr; apply hu
_ = (∑ i, ‖v.equivFun e i‖₊) * M := by rw [Finset.sum_mul]
_ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) * M := by
gcongr
calc
∑ i, ‖v.equivFun e i‖₊ ≤ Fintype.card ι • ‖φ e‖₊ := Pi.sum_nnnorm_apply_le_nnnorm _
_ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) := nsmul_le_nsmul_right (φ.le_opNNNorm e) _
_ = Fintype.card ι • ‖φ‖₊ * M * ‖e‖₊ := by simp only [smul_mul_assoc, mul_right_comm]
