(p : MvPolynomial (Fin D) ℂ) : quadForm harmCore ⟨pgLp p, pgLp_mem_core p⟩ = ∑ j : Fin D, (‖pgLp (coreD j p)‖ ^ 2 + ‖pgLp (X j * p)‖ ^ 2 / 4)

Initializing...

(p : MvPolynomial (Fin D) ℂ) : quadForm harmCore ⟨pgLp p, pgLp_mem_core p⟩ = ∑ j : Fin D, (‖pgLp (coreD j p)‖ ^ 2 + ‖pgLp (X j * p)‖ ^ 2 / 4) · Prove2Me