English
For v ∈ E, ‖v‖ = sup { ‖⟪w,v⟫_A‖ : w ∈ E, ‖w‖ ≤ 1 }.
Русский
Для v ∈ E верно ‖v‖ = sup { ‖⟪w,v⟫_A‖ : w ∈ E, ‖w‖ ≤ 1 }.
LaTeX
$$$\\\\|v\\\\| = \\operatorname{csSup} \\{ \\\\|\\\\langle w, v \\\\rangle_A\\\\| \\; | \\; w \\in E, \\\\|w\\\\| \\le 1 \\}$$$
Lean4
theorem norm_eq_csSup (v : E) : ‖v‖ = sSup {‖⟪w, v⟫_A‖ | (w : E) (_ : ‖w‖ ≤ 1)} :=
by
let instNACG : NormedAddCommGroup E := NormedAddCommGroup.ofCore (normedSpaceCore A)
let instNS : NormedSpace ℂ E := .ofCore (normedSpaceCore A)
refine Eq.symm <| IsGreatest.csSup_eq ⟨⟨‖v‖⁻¹ • v, ?_, ?_⟩, ?_⟩
· simpa only [norm_smul, norm_inv, norm_norm] using inv_mul_le_one_of_le₀ le_rfl (by positivity)
· simp [norm_smul, ← norm_sq_eq, pow_two, ← mul_assoc]
· rintro - ⟨w, hw, rfl⟩
calc
_ ≤ ‖w‖ * ‖v‖ := norm_inner_le E
_ ≤ 1 * ‖v‖ := by gcongr
_ = ‖v‖ := by simp
