English
An auxiliary inequality for Cauchy–Schwarz: 0 ≤ ∥x∥^2 t^2 + 2 Re ⟨x,y⟩ t + ∥y∥^2 for all t ∈ ℝ.
Русский
Вспомогательное неравенство для неравенства Цейча–Шварца: для любого t ∈ ℝ выполняется 0 ≤ ∥x∥^2 t^2 + 2 Re ⟨x,y⟩ t + ∥y∥^2.
LaTeX
$$$0 \\le \\|x\\|^2 t^2 + 2 \\operatorname{Re} \\langle x,y \\rangle t + \\|y\\|^2$$$
Lean4
/-- An auxiliary equality useful to prove the **Cauchy–Schwarz inequality**. Here we use the
standard argument involving the discriminant of quadratic form. -/
theorem cauchy_schwarz_aux' (x y : F) (t : ℝ) : 0 ≤ normSqF x * t * t + 2 * re ⟪x, y⟫ * t + normSqF y := by
calc
0 ≤ re ⟪(ofReal t : 𝕜) • x + y, (ofReal t : 𝕜) • x + y⟫ := inner_self_nonneg
_ = re (⟪(ofReal t : 𝕜) • x, (ofReal t : 𝕜) • x⟫ + ⟪(ofReal t : 𝕜) • x, y⟫ + ⟪y, (ofReal t : 𝕜) • x⟫ + ⟪y, y⟫) := by
rw [inner_add_add_self ((ofReal t : 𝕜) • x) y]
_ =
re ⟪(ofReal t : 𝕜) • x, (ofReal t : 𝕜) • x⟫ + re ⟪(ofReal t : 𝕜) • x, y⟫ + re ⟪y, (ofReal t : 𝕜) • x⟫ +
re ⟪y, y⟫ :=
by simp only [map_add]
_ = normSq x * t * t + re (⟪x, y⟫ * t) + re (⟪y, x⟫ * t) + re ⟪y, y⟫ := by
rw [re_inner_smul_ofReal_smul_self, inner_smul_ofReal_left, inner_smul_ofReal_right]
_ = normSq x * t * t + re ⟪x, y⟫ * t + re ⟪y, x⟫ * t + re ⟪y, y⟫ := by
rw [mul_comm ⟪x, y⟫ _, RCLike.re_ofReal_mul, mul_comm t _, mul_comm ⟪y, x⟫ _, RCLike.re_ofReal_mul, mul_comm t _]
_ = normSq x * t * t + re ⟪x, y⟫ * t + re ⟪y, x⟫ * t + normSq y := by rw [← normSq]
_ = normSq x * t * t + re ⟪x, y⟫ * t + re ⟪x, y⟫ * t + normSq y := by rw [inner_re_symm]
_ = normSq x * t * t + 2 * re ⟪x, y⟫ * t + normSq y := by ring
