Exact central-binomial valuation distributions for odd primes

For the odd prime p = 2 * half + 1, this module identifies fixed-length base-p words with the integers below p ^ length. Kummer's theorem turns the word carry count into the exact value of ν_p (centralBinom n), so the transfer recurrence becomes an arithmetic distribution theorem.

def OddPrimeValuationDistribution.oddCarryWordValue {half length : ℕ} (word : List.Vector (Fin (oddBase half)) length) : ℕ

Natural value of a fixed-length word in the odd base 2 * half + 1.

Equations

• OddPrimeValuationDistribution.oddCarryWordValue word = Nat.ofDigits (OddPrimeValuationDistribution.oddBase half) (OddPrimeValuationDistribution.oddCarryWordDigits word)

theorem OddPrimeValuationDistribution.oddCarryWordValue_lt {half length : ℕ} (hhalf : 0 < half) (word : List.Vector (Fin (oddBase half)) length) : oddCarryWordValue word < oddBase half ^ length

def OddPrimeValuationDistribution.oddCarryWordValueFin {half length : ℕ} (hhalf : 0 < half) (word : List.Vector (Fin (oddBase half)) length) : Fin (oddBase half ^ length)

The word value packaged in the corresponding complete finite block.

Equations

• OddPrimeValuationDistribution.oddCarryWordValueFin hhalf word = ⟨OddPrimeValuationDistribution.oddCarryWordValue word, ⋯⟩

theorem OddPrimeValuationDistribution.oddCarryWordValueFin_injective (half : ℕ) (hhalf : 0 < half) (length : ℕ) : Function.Injective (oddCarryWordValueFin hhalf)

noncomputable def OddPrimeValuationDistribution.oddCarryWordValueEquiv (half : ℕ) (hhalf : 0 < half) (length : ℕ) : List.Vector (Fin (oddBase half)) length ≃ Fin (oddBase half ^ length)

Positional notation is a bijection from fixed-length odd-base words to the corresponding complete block of natural numbers.

Equations

• OddPrimeValuationDistribution.oddCarryWordValueEquiv half hhalf length = Equiv.ofBijective (OddPrimeValuationDistribution.oddCarryWordValueFin hhalf) ⋯

theorem OddPrimeValuationDistribution.padicValNat_oddPrime_centralBinom_word_eq_carryCount (half : ℕ) (hhalf : 0 < half) [Fact (Nat.Prime (oddBase half))] {length : ℕ} (word : List.Vector (Fin (oddBase half)) length) : padicValNat (oddBase half) (oddCarryWordValue word).centralBinom = oddDoubleCarryCountAux half (oddCarryWordDigits word) 0

noncomputable def OddPrimeValuationDistribution.oddPrimeValuationPolynomial (half length : ℕ) : Polynomial ℕ

Polynomial distribution of exact odd-prime valuations on the complete block 0 ≤ n < p ^ length.

Equations

• One or more equations did not get rendered due to their size.

theorem OddPrimeValuationDistribution.oddPrimeValuationPolynomial_eq_carryPolynomial (half : ℕ) (hhalf : 0 < half) [Fact (Nat.Prime (oddBase half))] (length : ℕ) : oddPrimeValuationPolynomial half length = oddCarryPolynomial half length

The odd-prime valuation distribution is exactly the doubling-carry distribution.

@[reducible, inline]

abbrev OddPrimeValuationDistribution.OddPrimeBlockWithValuation (half length value : ℕ) : Type

Integers in a complete odd-prime block with a prescribed exact central-binomial valuation.

Equations

• One or more equations did not get rendered due to their size.

theorem OddPrimeValuationDistribution.coeff_oddPrimeValuationPolynomial (half length value : ℕ) : (oddPrimeValuationPolynomial half length).coeff value = Fintype.card (OddPrimeBlockWithValuation half length value)

Literal coefficient interpretation of the odd-prime valuation polynomial.

theorem OddPrimeValuationDistribution.oddPrimeValuationPolynomial_recurrence (half : ℕ) (hhalf : 0 < half) [Fact (Nat.Prime (oddBase half))] (length : ℕ) : oddPrimeValuationPolynomial half (length + 2) + ↑(oddBase half) * Polynomial.X * oddPrimeValuationPolynomial half length = ↑(half + 1) * (1 + Polynomial.X) * oddPrimeValuationPolynomial half (length + 1)

Headline exact-distribution recurrence for every odd prime p = 2 * half + 1.