OAI/NumberTheory/Ostmann/Construction/InitialWordAtomIntervals.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.initialWordAtomLower line 10
2. def OAI.Ostmann.initialWordAtomUpper line 14
3. theorem OAI.Ostmann.initialWordBinRange_values line 18
4. theorem OAI.Ostmann.initialWordBinRanges_values line 27
5. theorem OAI.Ostmann.initialWordAtomIntervals_equiv line 45

   Source documentation

   All nonword intervals already hold on the original prior. Thus adding these guards leaves precisely the two original word-bin events.

   theorem initialWordAtomIntervals_equiv {C : Type*} [Fintype C]
       (role : Bool × Option C → CopyScheduleRole) (j : ℕ) (lo hi : C → ℕ)
       (x : CopyScheduleAtoms role 0 → ℕ)
       (hcell : ∀ (b : Bool) (c : C), lo c ≤ x ⟨(b, some c), trivial⟩ ∧
         x ⟨(b, some c), trivial⟩ ≤ hi c) :
       (∀ r ∈ atomIntervalRanges role (initialWordAtomLower j lo)
         (initialWordAtomUpper j hi) 0, r.Holds x) ↔
       ∀ r ∈ initialWordBinRanges role j, r.Holds x := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.atomIntervalRanges, OAI.Ostmann.initialWordAtomLower, OAI.Ostmann.initialWordAtomUpper, OAI.Ostmann.initialWordBinRanges