Bivariate generating function for odd-prime valuation distributions

For p = 2 * half + 1, the coefficient of T ^ k * X ^ r counts 0 ≤ n < p ^ k with ν_p (centralBinom n) = r. The theorem below is the denominator-cleared, subtraction-free form of

(1 - X * T) / (1 - (half + 1) * (1 + X) * T + p * X * T ^ 2).

noncomputable def OddPrimeValuationDistribution.oddPrimeValuationGeneratingSeries (half : ℕ) : PowerSeries (Polynomial ℕ)

Bivariate generating series for complete odd-base valuation blocks.

Equations

• OddPrimeValuationDistribution.oddPrimeValuationGeneratingSeries half = PowerSeries.mk (OddPrimeValuationDistribution.oddPrimeValuationPolynomial half)

theorem OddPrimeValuationDistribution.oddPrimeValuationGeneratingSeries_identity (half : ℕ) (hhalf : 0 < half) [Fact (Nat.Prime (oddBase half))] : oddPrimeValuationGeneratingSeries half + PowerSeries.C (↑(oddBase half) * Polynomial.X) * (PowerSeries.X ^ 2 * oddPrimeValuationGeneratingSeries half) + PowerSeries.C Polynomial.X * PowerSeries.X = 1 + PowerSeries.C (↑(half + 1) * (1 + Polynomial.X)) * (PowerSeries.X * oddPrimeValuationGeneratingSeries half)

Headline rational generating-function identity for every odd prime. The outer PowerSeries.X records block length and the inner Polynomial.X records exact valuation.