English
For all x,y ∈ E, ‖⟪x,y⟫‖ ≤ ‖x‖ · ‖y‖.
Русский
Для всех x,y ∈ E верно ‖⟪x,y⟫‖ ≤ ‖x‖ · ‖y‖.
LaTeX
$$$\\\\|\\\\langle x, y \\\\rangle_A\\\\| \\\\leq \\\\|x\\\\| \\\\cdot \\\\|y\\\\|$$$
Lean4
/-- The Cauchy-Schwarz inequality for Hilbert C⋆-modules. -/
theorem norm_inner_le {x y : E} : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖ :=
by
have :=
calc
‖⟪x, y⟫‖ ^ 2 = ‖⟪x, y⟫ * ⟪y, x⟫‖ := by rw [← star_inner x, CStarRing.norm_self_mul_star, pow_two]
_ ≤ ‖‖x‖ ^ 2 • ⟪y, y⟫‖ :=
by
refine CStarAlgebra.norm_le_norm_of_nonneg_of_le ?_ inner_mul_inner_swap_le
rw [← star_inner x]
exact mul_star_self_nonneg ⟪x, y⟫_A
_ = ‖x‖ ^ 2 * ‖⟪y, y⟫‖ := by simp [norm_smul]
_ = ‖x‖ ^ 2 * ‖y‖ ^ 2 := by simp only [norm_eq_sqrt_norm_inner_self (A := A), norm_nonneg, Real.sq_sqrt]
_ = (‖x‖ * ‖y‖) ^ 2 := by simp only [mul_pow]
refine (pow_le_pow_iff_left₀ (norm_nonneg ⟪x, y⟫_A) ?_ (by simp)).mp this
exact mul_nonneg (CStarModule.norm_nonneg A) (CStarModule.norm_nonneg A)
