OAI/NumberTheory/Ostmann/Arithmetic/MovingFullModulus.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A concrete common modulus for every full-support residue test

  1. theorem OAI.Ostmann.MovingSlotData.compensation_dvd_spectatorDenominator line 11
  2. def OAI.Ostmann.movingFullPairModulusBase line 31
  3. def OAI.Ostmann.movingFullPairModulus line 38
  4. theorem OAI.Ostmann.movingFullPairModulus_components line 44
  5. theorem OAI.Ostmann.movingFullPairModulus_pos line 57
  6. theorem OAI.Ostmann.movingFullPairModulus_tests line 71

    Source documentation

    The one common modulus supplies all four divisibility conditions used in exact two-history factorization, including every compensation-prime square.

    theorem movingFullPairModulus_tests {σ I : Type*} (value : σ → ℕ)
    (hvalue : ∀ i, value i ≠ 0) (outside : List ℕ) (childBound pivotBound : ℕ → ℕ)
    {n : ℕ} (T : Bool → MovingSlotData σ n) (hf : ∀ b, (T b).Frequencies (· ≠ 0))
    (q : I → ℕ) (S : Finset I) :
    let M := movingFullPairModulus value hvalue outside childBound pivotBound T hf q S
…

    Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingFullPairModulus