English
For a symmetric linear map T, the polarization identity expresses ⟪T x, y⟫ in terms of values of ⟪T·, ·⟫ on sums and differences of x and y.
Русский
Для симметричного линейного отображения T поляризация выражает ⟪T x, y⟫ через значения ⟪T·, ·⟫ на суммах и разностях x и y.
LaTeX
$$$⟪T x, y⟫ = \frac{⟪T(x+y), x+y⟫ - ⟪T(x-y), x-y⟫ - i⟪T(x+i y), x+i y⟫ + i⟪T(x-iy), x-iy⟫}{4}$$$
Lean4
/-- Polarization identity for symmetric linear maps.
See `inner_map_polarization` for the complex version without the symmetric assumption. -/
theorem inner_map_polarization {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (x y : E) :
⟪T x, y⟫ =
(⟪T (x + y), x + y⟫ - ⟪T (x - y), x - y⟫ - I * ⟪T (x + (I : 𝕜) • y), x + (I : 𝕜) • y⟫ +
I * ⟪T (x - (I : 𝕜) • y), x - (I : 𝕜) • y⟫) /
4 :=
by
rcases @I_mul_I_ax 𝕜 _ with (h | h)
· simp_rw [h, zero_mul, sub_zero, add_zero, map_add, map_sub, inner_add_left, inner_add_right, inner_sub_left,
inner_sub_right, hT x, ← inner_conj_symm x (T y)]
suffices (re ⟪T y, x⟫ : 𝕜) = ⟪T y, x⟫ by
rw [conj_eq_iff_re.mpr this]
ring
rw [← re_add_im ⟪T y, x⟫]
simp_rw [h, mul_zero, add_zero]
norm_cast
· simp_rw [map_add, map_sub, inner_add_left, inner_add_right, inner_sub_left, inner_sub_right, LinearMap.map_smul,
inner_smul_left, inner_smul_right, RCLike.conj_I, mul_add, mul_sub, sub_sub, ← mul_assoc, mul_neg, h, neg_neg,
one_mul, neg_one_mul]
ring
