OAI/NumberTheory/Ostmann/Arithmetic/MovingRegularCoprime.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.product_coprime_frequency line 10
2. theorem OAI.Ostmann.MovingSlotData.smallProduct_frequency_coprime line 18
3. theorem OAI.Ostmann.movingOriginalRegular_coprime_reduced line 30

   Source documentation

   For the two original histories, the computed reduced modulus is coprime to their common regular-prime product. No extra coprimality of moduli is assumed.

   theorem movingOriginalRegular_coprime_reduced {σ I : Type*} (tier : σ → ℕ) (value : σ → ℕ)
       (hprime : ∀ i, (value i).Prime) (hdisjoint : ∀ i j, tier i ≠ tier j → value i ≠ value j)
       (outside : List ℕ) (childBound pivotBound : ℕ → ℕ) {n : ℕ}
       (T : Bool → MovingSlotData σ n) (hf : ∀ b, (T b).Frequencies (· ≠ 0))
       (hlevels : ∀ b, (T b).Levels tier)
       (hsmall : ∀ b i, (T b).Frequencies (fun s => IsCoprime s (value i : ℤ)))
       (hout : ∀ b, movingRegularOutsidePairwise value outside (T b))
       (R : ℕ) (hregular : ∀ b, MovingSlotReversal.naturalProduct value (T b).regularSlots = R)
       (q : I → ℕ) (S : Finset I) (hq : ∀ i ∈ S, R.Coprime (q i)) :
       R.Coprime (movingReducedPairModulus value (fun i => (hprime i).ne_zero) outside
         childBound pivotBound T hf q S) := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingRegularOutsidePairwise, OAI.Ostmann.MovingSlotReversal.naturalProduct, OAI.Ostmann.movingReducedPairModulus