OAI/NumberTheory/Ostmann/Construction/ConstituentAtomSupport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.scheduleConstituentWord_coprime_left line 12
2. theorem OAI.Ostmann.scheduleConstituentWord_coprime_right line 20
3. theorem OAI.Ostmann.constituent_fullAtomRootGuard line 29

   Source documentation

   Every coprimality and frequency-unit component of the next grouped guard is supplied by the constituent-level arithmetic transfer.

   theorem constituent_fullAtomRootGuard {I : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (size : I → ℕ)
       (ranges : (j : ℕ) → List (ScheduleAtomRange role j)) (n : ℕ)
       (q : SurvivingConstituent role size (n + 1) → ℕ) (M : ℕ) (s : ℤ)
       (hq : Pairwise (fun i j => (q i).Coprime (q j)))
       (hM : ∀ i, M.Coprime (q i)) (hs : ∀ i, (q i).Coprime s.natAbs)
       (hrange : ∀ r ∈ ranges (n + 1), r.Holds
         (fun v => ((scheduleConstituentWord role size (n + 1) v).map q).prod)) :
       fullAtomRootGuard role ranges n
         (fun v => ((scheduleConstituentWord role size (n + 1) v).map q).prod) M s := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.ScheduleAtomRange, OAI.Ostmann.SurvivingConstituent, OAI.Ostmann.scheduleConstituentWord, OAI.Ostmann.fullAtomRootGuard