English
For all x,y ∈ E, ⟪x,y⟫ ⟪y,x⟫ ≤ ‖x‖^2 ⟪y,y⟫ in A.
Русский
Для любых x,y ∈ E выполняется ⟪x,y⟫ ⟪y,x⟫ ≤ ‖x‖^2 ⟪y,y⟫ в A.
LaTeX
$$$\\\\langle x, y \\\\rangle_A \\\\langle y, x \\\\rangle_A \\leq ||x||^2 \\\\\\langle y, y \\\\rangle_A$$$
Lean4
/-- The C⋆-algebra-valued Cauchy-Schwarz inequality for Hilbert C⋆-modules. -/
theorem inner_mul_inner_swap_le {x y : E} : ⟪x, y⟫ * ⟪y, x⟫ ≤ ‖x‖ ^ 2 • ⟪y, y⟫ :=
by
rcases eq_or_ne x 0 with h | h
· simp [h, CStarModule.norm_zero A (E := E)]
· have h₁ :
∀ (a : A),
(0 : A) ≤
‖x‖ ^ 2 • (a * star a) - ‖x‖ ^ 2 • (a * ⟪y, x⟫) - ‖x‖ ^ 2 • (⟪x, y⟫ * star a) +
‖x‖ ^ 2 • (‖x‖ ^ 2 • ⟪y, y⟫) :=
fun a => by
calc
(0 : A) ≤ ⟪a • x - ‖x‖ ^ 2 • y, a • x - ‖x‖ ^ 2 • y⟫_A := by exact inner_self_nonneg
_ = a * ⟪x, x⟫ * star a - ‖x‖ ^ 2 • (a * ⟪y, x⟫) - ‖x‖ ^ 2 • (⟪x, y⟫ * star a) + ‖x‖ ^ 2 • (‖x‖ ^ 2 • ⟪y, y⟫) :=
by
simp only [inner_sub_right, inner_op_smul_right, inner_sub_left, inner_op_smul_left, inner_smul_left_real,
mul_sub, mul_smul_comm, inner_smul_right_real, smul_sub, mul_assoc]
abel
_ ≤
‖x‖ ^ 2 • (a * star a) - ‖x‖ ^ 2 • (a * ⟪y, x⟫) - ‖x‖ ^ 2 • (⟪x, y⟫ * star a) +
‖x‖ ^ 2 • (‖x‖ ^ 2 • ⟪y, y⟫) :=
by
gcongr
calc
_ ≤ ‖⟪x, x⟫_A‖ • (a * star a) := CStarAlgebra.conjugate_le_norm_smul'
_ = (√‖⟪x, x⟫_A‖) ^ 2 • (a * star a) := by
rw [Real.sq_sqrt]
positivity
_ = ‖x‖ ^ 2 • (a * star a) := by rw [← norm_eq_sqrt_norm_inner_self]
specialize h₁ ⟪x, y⟫
simp only [star_inner, sub_self, zero_sub, le_neg_add_iff_add_le, add_zero] at h₁
rwa [smul_le_smul_iff_of_pos_left (pow_pos (CStarModule.norm_pos A h) _)] at h₁
