OAI/NumberTheory/Ostmann/Arithmetic/MovingReducedModulus.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingReducedPairModulusBase line 11
2. def OAI.Ostmann.movingReducedPairModulus line 18
3. theorem OAI.Ostmann.movingReducedPairModulus_components line 24
4. theorem OAI.Ostmann.movingReducedPairModulus_pos line 37
5. theorem OAI.Ostmann.movingReducedPairModulus_tests line 51

   Source documentation

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

   theorem movingReducedPairModulus_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 := movingReducedPairModulus value hvalue outside childBound pivotBound T hf q S
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingReducedPairModulus

6. theorem OAI.Ostmann.movingReducedPairModulus_dvd_full line 82

   Source documentation

   The reduced modulus introduces no new size cost.

   theorem movingReducedPairModulus_dvd_full {σ 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) :
       movingReducedPairModulus value hvalue outside childBound pivotBound T hf q S ∣
         movingFullPairModulus value hvalue outside childBound pivotBound T hf q S := by
   …

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

7. theorem OAI.Ostmann.movingReducedPairModulus_coprime line 96

   Source documentation

   The auxiliary period and the node frequencies suffice to split off any regular block coprime to the fixed spectator primes.

   theorem movingReducedPairModulus_coprime {σ 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) (r : ℕ)
       (hfreq : ∀ b, (T b).Frequencies (fun s => r.Coprime s.natAbs))
       (haux : ∀ b, r.Coprime (movingAuxiliaryUnitPeriod value outside (T b)).natAbs)
       (hq : ∀ i ∈ S, r.Coprime (q i)) :
       r.Coprime (movingReducedPairModulus value hvalue outside childBound pivotBound T hf q S) := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingAuxiliaryUnitPeriod, OAI.Ostmann.movingReducedPairModulus