MovingAuxiliaryCoprime.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The recursive auxiliary period is coprime to the original regular block

theorem OAI.Ostmann.product_coprime_right line 11
theorem OAI.Ostmann.MovingSlotData.regular_level_bound line 20
theorem OAI.Ostmann.movingAuxiliaryUnitPeriod_coprime line 27

theorem OAI.Ostmann.movingRegularProduct_coprime_auxiliary line 52

Source documentation

This is the actual CRT separation: an original regular prime has higher level than every compensation prime in the subtree, and is coprime to every frequency and to the fixed outside list.

theorem movingRegularProduct_coprime_auxiliary {σ : Type*} (tier : σ → ℕ) (value : σ → ℕ)
    (hprime : ∀ i, (value i).Prime) (hdisjoint : ∀ i j, tier i ≠ tier j → value i ≠ value j)
    (outside : List ℕ) {n : ℕ} (T : MovingSlotData σ n) (hT : T.Levels tier)
    (hf : ∀ i, T.Frequencies (fun s => IsCoprime s (value i : ℤ)))
    (houtside : movingRegularOutsidePairwise value outside T) :
    IsCoprime (MovingSlotReversal.naturalProduct value T.regularSlots : ℤ)
      (movingAuxiliaryUnitPeriod value outside T) := by
…

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