Finite coefficient identities underlying the Gaussian counterexamples.

theorem GaussianMomentsCounterexamples.choose_neg_half (n : ℕ) : Ring.choose (-1 / 2) n = (-1) ^ n / 4 ^ n * ↑((2 * n).choose n)

The central binomial coefficients are the coefficients of the formal exponent -1/2.

theorem GaussianMomentsCounterexamples.binomial_neg_half_subst_mul : PowerSeries.subst (PowerSeries.X * (2 + PowerSeries.X)) (PowerSeries.binomialSeries ℂ (-1 / 2)) * (1 + PowerSeries.X) = 1

The formal branch of the inverse square root becomes the geometric inverse under the substitution X(2+X).

theorem GaussianMomentsCounterexamples.coeff_mul_subst_X_mul (f g h : PowerSeries ℂ) (m : ℕ) : (PowerSeries.coeff m) (g * PowerSeries.subst (PowerSeries.X * h) f) = ∑ k ∈ Finset.range (m + 1), (PowerSeries.coeff k) f * (PowerSeries.coeff (m - k)) (g * h ^ k)

Extracting a coefficient after substitution needs only finitely many input terms.

theorem GaussianMomentsCounterexamples.coefficient_identity_three (A : Polynomial ℂ) (m : ℕ) (hm : 1 ≤ m) : ∑ k ∈ Finset.range (m + 1), (-1) ^ k / 4 ^ k * ↑((2 * k).choose k) * (A * (1 + Polynomial.X) ^ m * (2 + Polynomial.X) ^ k).coeff (m - k) = (A * (1 + Polynomial.X) ^ (m - 1)).coeff m

The finite coefficient identity in the three-variable master formula.

theorem GaussianMomentsCounterexamples.choose_neg_one (n : ℕ) : Ring.choose (-1) n = (-1) ^ n

The geometric inverse series has alternating coefficients.

theorem GaussianMomentsCounterexamples.coefficient_identity_four (A : Polynomial ℂ) (m : ℕ) (hm : 1 ≤ m) : ∑ a ∈ Finset.range (m + 1), (-1) ^ a * (A * (1 + Polynomial.X) ^ m).coeff (m - a) = (A * (1 + Polynomial.X) ^ (m - 1)).coeff m

The finite coefficient identity in the four-variable master formula.

theorem GaussianMomentsCounterexamples.master_coefficient_one (m : ℕ) (hm : 1 ≤ m) : (1 * (1 + Polynomial.X) ^ (m - 1)).coeff m = 0

The master coefficient vanishes for the constant test polynomial.

theorem GaussianMomentsCounterexamples.master_coefficient_X (m : ℕ) (hm : 1 ≤ m) : (Polynomial.X * (1 + Polynomial.X) ^ (m - 1)).coeff m = 1

The master coefficient is one for the linear test polynomial.

theorem GaussianMomentsCounterexamples.three_moment_scalar (m k : ℕ) (hk : k ≤ m) : ↑(m.choose k) * ↑(m - k).factorial * (-1 / 2) ^ k * ↑(2 * k).factorial / (2 ^ k * ↑k.factorial) = ↑m.factorial * ((-1) ^ k / 4 ^ k * ↑((2 * k).choose k))

Exact factorial cancellation in the three-variable Gaussian expansion.