English
For any a, x, y in E, the cross-term identity holds: ⟪a,x⟫⟪a,y⟫ + ω(a,x) ω(a,y) = ||a||^2 ⟪x,y⟫.
Русский
Для любых a, x, y ∈ E выполнено тождество: ⟪a,x⟫⟪a,y⟫ + ω(a,x) ω(a,y) = ||a||^2 ⟪x,y⟫.
LaTeX
$$$\\langle a,x\\rangle \\langle a,y\\rangle + \\omega(a,x)\\omega(a,y) = \\|a\\|^2 \\langle x,y\\rangle$$$
Lean4
/-- For vectors `a x y : E`, the identity `⟪a, x⟫ * ⟪a, y⟫ + ω a x * ω a y = ‖a‖ ^ 2 * ⟪x, y⟫`. (See
`Orientation.inner_mul_inner_add_areaForm_mul_areaForm` for the "applied" form.) -/
theorem inner_mul_inner_add_areaForm_mul_areaForm' (a x : E) :
⟪a, x⟫ • innerₛₗ ℝ a + ω a x • ω a = ‖a‖ ^ 2 • innerₛₗ ℝ x :=
by
by_cases ha : a = 0
· simp [ha]
apply (o.basisRightAngleRotation a ha).ext
intro i
fin_cases i
· simp [real_inner_self_eq_norm_sq, mul_comm, real_inner_comm]
· simp [real_inner_self_eq_norm_sq, mul_comm, o.areaForm_swap a x]