English
A variant of the polarization identity with a bilinear map, giving a similar decomposition of inner products.
Русский
Вариант поляризационной формулы для билинейной отображения, аналогично разложению скалярного произведения.
LaTeX
$$$ \langle T x, y \rangle = \frac{\langle T(x+y), x+y \rangle - \langle T(x-y), x-y \rangle - i \langle T(x + i y), x + i y \rangle + i \langle T(x - i y), x - i y \rangle}{4}. $$$
Lean4
theorem inner_map_polarization' (T : V →ₗ[ℂ] V) (x y : V) :
⟪T x, y⟫_ℂ =
(⟪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
