English
For an orthonormal basis b and vector x, the norm of x is bounded by the cardinality of the index set and the supremum of the norms of inner products: ‖x‖ ≤ √(|ι|) sup_i ‖⟪b_i, x⟫‖.
Русский
Для ортонормированного базиса b и вектора x норму ‖x‖ можно оценить через число элементов базиса и супремум норм скалярных произведений: ‖x‖ ≤ √(|ι|) sup_i ‖⟪b_i, x⟫‖.
LaTeX
$$$\|x\| \leq \sqrt{\lvert ι \rvert} \cdot \Big( \sup_i \|\langle b_i, x \rangle\| \Big)$$
Lean4
theorem norm_le_card_mul_iSup_norm_inner (b : OrthonormalBasis ι 𝕜 E) (x : E) :
‖x‖ ≤ √(Fintype.card ι) * ⨆ i, ‖⟪b i, x⟫‖ := by
calc
‖x‖
_ = √(∑ i, ‖⟪b i, x⟫‖ ^ 2) := by rw [sum_sq_norm_inner_right, Real.sqrt_sq (by positivity)]
_ ≤ √(∑ _ : ι, (⨆ j, ‖⟪b j, x⟫‖) ^ 2) := by
gcongr with i
exact le_ciSup (f := fun j ↦ ‖⟪b j, x⟫‖) (by simp) i
_ = √(Fintype.card ι) * ⨆ i, ‖⟪b i, x⟫‖ :=
by
simp only [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, Nat.cast_nonneg, Real.sqrt_mul]
congr
rw [Real.sqrt_sq]
cases isEmpty_or_nonempty ι
· simp
· exact le_ciSup_of_le (by simp) (Nonempty.some inferInstance) (by positivity)
