English
A polarization identity expresses an inner product in terms of a bilinear form evaluated at linear combinations of vectors.
Русский
Поляризационная формула выражает скалярное произведение через билинейную форму на линейных сочетаниях векторов.
LaTeX
$$$ \langle Ty, x \rangle_\mathbb{C} = \frac{\langle T(x+y), x+y \rangle_\mathbb{C} - \langle T(x-y), x-y \rangle_\mathbb{C} + i \langle T(x + i y), x + i y \rangle_\mathbb{C} - i \langle T(x - i y), x - i y \rangle_\mathbb{C}}{4}. $$$
Lean4
/-- A complex polarization identity, with a linear map. -/
theorem inner_map_polarization (T : V →ₗ[ℂ] V) (x y : V) :
⟪T y, x⟫_ℂ =
(⟪T (x + y), x + y⟫_ℂ - ⟪T (x - y), x - y⟫_ℂ + Complex.I * ⟪T (x + Complex.I • y), x + Complex.I • y⟫_ℂ -
Complex.I * ⟪T (x - Complex.I • y), x - Complex.I • y⟫_ℂ) /
4 :=
by
simp only [map_add, map_sub, inner_add_left, inner_add_right, LinearMap.map_smul, inner_smul_left, inner_smul_right,
Complex.conj_I, ← pow_two, Complex.I_sq, inner_sub_left, inner_sub_right, mul_add, ← mul_assoc, mul_neg, neg_neg,
one_mul, neg_one_mul, mul_sub, sub_sub]
ring
