OAI/NumberTheory/Ostmann/Construction/ScheduledNodeUnits.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.ScheduleNodeUnits line 11
2. theorem OAI.Ostmann.scheduleAtomUnitsValid_nodeList line 15
3. theorem OAI.Ostmann.scheduledNodeValues_units line 31
4. theorem OAI.Ostmann.fullAtomTransferWeight_valid_units line 59

   Source documentation

   Nonzero full weights already contain all validity and frequency-unit conditions used by the sampled-history estimate.

   theorem fullAtomTransferWeight_valid_units {I : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (childBound pivotBound : ℕ → ℕ)
       (ranges : (j : ℕ) → List (ScheduleAtomRange role j))
       (leaf : ScheduleAtomState role → ℤ → ℂ) (n : ℕ)
       (C : CopyScheduleAtoms role n → ℕ) (t : FrequencyTree ℤ n)
       (hw : fullAtomTransferWeight role childBound pivotBound ranges leaf n C t ≠ 0) :
       ValidTransferHistory (scheduleAtomSystem role childBound pivotBound) n ⟨n, C⟩ t ∧
         scheduleAtomUnitsValid role childBound pivotBound (totalAtomUnitRanges role) n C t := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.ScheduleAtomRange, OAI.Ostmann.ScheduleAtomState, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.FrequencyTree, OAI.Ostmann.fullAtomTransferWeight, OAI.Ostmann.ValidTransferHistory, OAI.Ostmann.scheduleAtomSystem, OAI.Ostmann.scheduleAtomUnitsValid, OAI.Ostmann.totalAtomUnitRanges