OAI/NumberTheory/Ostmann/Arithmetic/AtomIntervalRanges.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.atomInterval line 12
2. def OAI.Ostmann.atomIntervalRanges line 18
3. theorem OAI.Ostmann.atomInterval_holds_iff line 22
4. theorem OAI.Ostmann.atomIntervalRanges_holds_iff line 29
5. theorem OAI.Ostmann.atomIntervalRanges_copied line 43

   Source documentation

   Copying preserves the original atom origin and hence its exact interval.

   theorem atomIntervalRanges_copied {I : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (lo hi : I → ℕ) (n M : ℕ)
       (u : CopyScheduleY role n → ℕ) (l r : CopyScheduleH role n → ℕ)
       (hL : ∀ a ∈ atomIntervalRanges role lo hi n,
         a.Holds (scheduledInsertedAtoms role n M l u))
       (hR : ∀ a ∈ atomIntervalRanges role lo hi n,
         a.Holds (scheduledInsertedAtoms role n M r u)) :
       ∀ a ∈ atomIntervalRanges role lo hi (n + 1),
         a.Holds (scheduledCopiedAssignment role n u l r) := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleY, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.atomIntervalRanges, OAI.Ostmann.scheduledInsertedAtoms, OAI.Ostmann.scheduledCopiedAssignment

6. theorem OAI.Ostmann.fullAtomTransferWeight_copied_intervals line 71

   Source documentation

   Both old full coefficients enforce every new interval. This discharges the interval clause in the actual guarded arithmetic step.

   theorem fullAtomTransferWeight_copied_intervals {I : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (lo hi : I → ℕ)
       (childBound pivotBound : ℕ → ℕ) (leaf : ScheduleAtomState role → ℤ → ℂ)
       (n M : ℕ) (u : CopyScheduleY role n → ℕ) (l r : CopyScheduleH role n → ℕ)
       (t t' : FrequencyTree ℤ n)
       (hL : fullAtomTransferWeight role childBound pivotBound (atomIntervalRanges role lo hi) leaf n
         (scheduledInsertedAtoms role n M l u) t ≠ 0)
       (hR : fullAtomTransferWeight role childBound pivotBound (atomIntervalRanges role lo hi) leaf n
         (scheduledInsertedAtoms role n M r u) t' ≠ 0) :
       ∀ a ∈ atomIntervalRanges role lo hi (n + 1), a.Holds (scheduledCopiedAssignment role n u l r) := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.ScheduleAtomState, OAI.Ostmann.CopyScheduleY, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.FrequencyTree, OAI.Ostmann.fullAtomTransferWeight, OAI.Ostmann.atomIntervalRanges, OAI.Ostmann.scheduledInsertedAtoms, OAI.Ostmann.scheduledCopiedAssignment