`BookProof.SqueezedGaussStates.pderiv_coordCombo_even` (i : Fin d) (a : ℕ → ℝ) (M : ℕ) (ha : a (M + 1) = 0) : pderiv i (coordCombo i a 0 M) = coordCombo i (fun k => 2 * (k + 1) * a

Initializing...

`BookProof.SqueezedGaussStates.pderiv_coordCombo_even` (i : Fin d) (a : ℕ → ℝ) (M : ℕ) (ha : a (M + 1) = 0) : pderiv i (coordCombo i a 0 M) = coordCombo i (fun k => 2 * (k + 1) * a · Prove2Me