English
The coefficient of a certain high degree in p·p̃ equals the sum of squares of the coefficients of p.
Русский
Коэффициент при определенной высокой степени в произведении p·p̃ равен сумме квадратов коэффициентов p.
LaTeX
$$$ (p \\cdot p^{\\sim}).\\mathrm{coeff}(\\operatorname{natDegree}(p) + \\operatorname{natTrailingDegree}(p)) = \\sum_{i} (\\operatorname{coeff}(p,i))^2 $$$
Lean4
theorem coeff_mul_mirror : (p * p.mirror).coeff (p.natDegree + p.natTrailingDegree) = p.sum fun _ => (· ^ 2) :=
by
rw [coeff_mul, Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk]
refine
(Finset.sum_congr rfl fun n hn => ?_).trans
(p.sum_eq_of_subset (fun _ ↦ (· ^ 2)) (fun _ ↦ zero_pow two_ne_zero) fun n hn ↦
Finset.mem_range_succ_iff.mpr ((le_natDegree_of_mem_supp n hn).trans (Nat.le_add_right _ _))).symm
rw [coeff_mirror, ← revAt_le (Finset.mem_range_succ_iff.mp hn), revAt_invol, ← sq]
