English
The Cauchy–Schwarz auxiliary identity: ∥⟪x,y⟫ • x − ⟪x,x⟫ • y∥^2 = ∥x∥^2 (∥x∥^2 ∥y∥^2 − ∥⟪x,y⟫∥^2).
Русский
Вспомогательное тождество Цейчина–Шварца: ∥⟨x,y⟩ x − ⟨x,x⟩ y∥^2 = ∥x∥^2 (∥x∥^2 ∥y∥^2 − ∥⟨x,y⟩∥^2).
LaTeX
$$$\\\\|\\\\langle x,y \\\\rangle \\\\cdot x - \\\\langle x,x \\\\rangle \\\\cdot y\\\\|^2 = \\\\|x\\\\|^2 \\\\bigl( \\\\|x\\\\|^2 \\\\|y\\\\|^2 - \\\\|\\\\langle x,y \\\\rangle\\\\|^2 \\bigr)$$$
Lean4
/-- Another auxiliary equality related with the **Cauchy–Schwarz inequality**: the square of the
seminorm of `⟪x, y⟫ • x - ⟪x, x⟫ • y` is equal to `‖x‖ ^ 2 * (‖x‖ ^ 2 * ‖y‖ ^ 2 - ‖⟪x, y⟫‖ ^ 2)`.
We use `InnerProductSpace.ofCore.normSq x` etc. (defeq to `is_R_or_C.re ⟪x, x⟫`) instead of
`‖x‖ ^ 2` etc. to avoid extra rewrites when applying it to an `InnerProductSpace`. -/
theorem cauchy_schwarz_aux (x y : F) :
normSqF (⟪x, y⟫ • x - ⟪x, x⟫ • y) = normSqF x * (normSqF x * normSqF y - ‖⟪x, y⟫‖ ^ 2) :=
by
rw [← @ofReal_inj 𝕜, ofReal_normSq_eq_inner_self]
simp only [inner_sub_sub_self, inner_smul_left, inner_smul_right, conj_ofReal, mul_sub,
← ofReal_normSq_eq_inner_self x, ← ofReal_normSq_eq_inner_self y]
rw [← mul_assoc, mul_conj, RCLike.conj_mul, mul_left_comm, ← inner_conj_symm y, mul_conj]
push_cast
ring
