norm_sub_sq — Mathlib

English

For real inner product spaces, ‖x+y‖^2 = ‖x‖^2 + 2 Re ⟪x, y⟫ + ‖y‖^2.

Русский

Для вещественных пространств: ‖x+y‖^2 = ‖x‖^2 + 2 Re ⟪x, y⟫ + ‖y‖^2.

LaTeX

$$$\|x+y\|^2 = \|x\|^2 + 2 \Re\langle x, y\rangle + \|y\|^2$$$

Lean4

/-- Expand the square -/
theorem norm_sub_sq (x y : E) : ‖x - y‖ ^ 2 = ‖x‖ ^ 2 - 2 * re ⟪x, y⟫ + ‖y‖ ^ 2 := by
  rw [sub_eq_add_neg, @norm_add_sq 𝕜 _ _ _ _ x (-y), norm_neg, inner_neg_right, map_neg, mul_neg, sub_eq_add_neg]

Похожие утверждения