Documentation

LeanPool.OddPrimeValuationDistribution.CarryPolynomial

Carry polynomials in an arbitrary odd base #

The coefficient of X ^ r in the length-k polynomial counts odd-base digit words whose doubling creates exactly r carries. Splitting the digit set at the carry threshold gives a two-state transfer matrix and its scalar second-order recurrence.

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

Convert an odd-base word to natural digits.

Equations
Instances For
    source
    noncomputable def OddPrimeValuationDistribution.oddCarryPolynomialFrom (half carry length : ℕ) :
    Polynomial ℕ

    Odd-base carry-count enumerator from an arbitrary incoming carry.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def OddPrimeValuationDistribution.oddCarryPolynomial (half length : ℕ) :
      Polynomial ℕ

      Odd-base carry-count enumerator from incoming carry zero.

      Equations
      Instances For
        source
        def OddPrimeValuationDistribution.oddCarryWordsSuccEquiv (half length : ℕ) :
        List.Vector (Fin (oddBase half)) (length + 1) ≃ (_ : Fin (oddBase half)) × List.Vector (Fin (oddBase half)) length

        Peeling the least significant digit from an odd-base word.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem OddPrimeValuationDistribution.oddCarryPolynomialFrom_zero (half carry : ℕ) :
          oddCarryPolynomialFrom half carry 0 = 1
          source
          theorem OddPrimeValuationDistribution.oddCarryPolynomialFrom_succ (half carry length : ℕ) :
          oddCarryPolynomialFrom half carry (length + 1) = ∑ digit : Fin (oddBase half), Polynomial.X ^ oddDoubleCarryStep half carry ↑digit * oddCarryPolynomialFrom half (oddDoubleCarryStep half carry ↑digit) length
          source
          def OddPrimeValuationDistribution.oddZeroCarryDigitSplitEquiv (half : ℕ) :
          Fin (oddBase half) ≃ Fin (half + 1) ⊕ Fin half

          Split digits into the half + 1 no-carry choices and half carry choices when the incoming carry is zero.

          Equations
          Instances For
            source
            def OddPrimeValuationDistribution.oddOneCarryDigitSplitEquiv (half : ℕ) :
            Fin (oddBase half) ≃ Fin half ⊕ Fin (half + 1)

            Split digits into the half no-carry choices and half + 1 carry choices when the incoming carry is one.

            Equations
            Instances For
              source
              @[simp]
              theorem OddPrimeValuationDistribution.oddZeroCarryDigitSplitEquiv_symm_inl_val (half : ℕ) (digit : Fin (half + 1)) :
              ↑((oddZeroCarryDigitSplitEquiv half).symm (Sum.inl digit)) = ↑digit
              source
              @[simp]
              theorem OddPrimeValuationDistribution.oddZeroCarryDigitSplitEquiv_symm_inr_val (half : ℕ) (digit : Fin half) :
              ↑((oddZeroCarryDigitSplitEquiv half).symm (Sum.inr digit)) = half + 1 + ↑digit
              source
              @[simp]
              theorem OddPrimeValuationDistribution.oddOneCarryDigitSplitEquiv_symm_inl_val (half : ℕ) (digit : Fin half) :
              ↑((oddOneCarryDigitSplitEquiv half).symm (Sum.inl digit)) = ↑digit
              source
              @[simp]
              theorem OddPrimeValuationDistribution.oddOneCarryDigitSplitEquiv_symm_inr_val (half : ℕ) (digit : Fin (half + 1)) :
              ↑((oddOneCarryDigitSplitEquiv half).symm (Sum.inr digit)) = half + ↑digit
              source
              theorem OddPrimeValuationDistribution.oddDoubleCarryStep_zero_split_inl (half : ℕ) (digit : Fin (half + 1)) :
              oddDoubleCarryStep half 0 ↑((oddZeroCarryDigitSplitEquiv half).symm (Sum.inl digit)) = 0
              source
              theorem OddPrimeValuationDistribution.oddDoubleCarryStep_zero_split_inr (half : ℕ) (digit : Fin half) :
              oddDoubleCarryStep half 0 ↑((oddZeroCarryDigitSplitEquiv half).symm (Sum.inr digit)) = 1
              source
              theorem OddPrimeValuationDistribution.oddDoubleCarryStep_one_split_inl (half : ℕ) (digit : Fin half) :
              oddDoubleCarryStep half 1 ↑((oddOneCarryDigitSplitEquiv half).symm (Sum.inl digit)) = 0
              source
              theorem OddPrimeValuationDistribution.oddDoubleCarryStep_one_split_inr (half : ℕ) (digit : Fin (half + 1)) :
              oddDoubleCarryStep half 1 ↑((oddOneCarryDigitSplitEquiv half).symm (Sum.inr digit)) = 1
              source
              theorem OddPrimeValuationDistribution.oddCarryPolynomialFrom_zeroCarry_succ (half length : ℕ) :
              oddCarryPolynomialFrom half 0 (length + 1) = ↑(half + 1) * oddCarryPolynomialFrom half 0 length + ↑half * Polynomial.X * oddCarryPolynomialFrom half 1 length
              source
              theorem OddPrimeValuationDistribution.oddCarryPolynomialFrom_oneCarry_succ (half length : ℕ) :
              oddCarryPolynomialFrom half 1 (length + 1) = ↑half * oddCarryPolynomialFrom half 0 length + ↑(half + 1) * Polynomial.X * oddCarryPolynomialFrom half 1 length
              source
              @[simp]
              theorem OddPrimeValuationDistribution.oddCarryPolynomial_zero (half : ℕ) :
              oddCarryPolynomial half 0 = 1
              source
              @[simp]
              theorem OddPrimeValuationDistribution.oddCarryPolynomial_one (half : ℕ) :
              oddCarryPolynomial half 1 = ↑(half + 1) + ↑half * Polynomial.X
              source
              theorem OddPrimeValuationDistribution.oddCarryPolynomial_recurrence (half length : ℕ) :
              oddCarryPolynomial half (length + 2) + ↑(oddBase half) * Polynomial.X * oddCarryPolynomial half length = ↑(half + 1) * (1 + Polynomial.X) * oddCarryPolynomial half (length + 1)

              Headline recurrence for the full carry distribution in odd base 2 * half + 1.