OAI/NumberTheory/Ostmann/Construction/FullCopiedWeight.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.scheduleAtomLeft_copied line 12
2. theorem OAI.Ostmann.scheduleAtomRight_copied line 17
3. theorem OAI.Ostmann.fullAtomTransferWeight_copied line 24

   Source documentation

   The parent coefficient is exactly the product of the two inherited coefficients at the forced pivot, with only the new root tests added.

   theorem fullAtomTransferWeight_copied {I : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (childBound pivotBound : ℕ → ℕ)
       (ranges : (j : ℕ) → List (ScheduleAtomRange role j))
       (leaf : ScheduleAtomState role → ℤ → ℂ) (n : ℕ)
       (u : CopyScheduleY role n → ℕ) (l r : CopyScheduleH role n → ℕ)
       (s : ℤ) (t t' : FrequencyTree ℤ n) (P : ℕ)
       (hP : ValidTransferNode (scheduleAtomSystem role childBound pivotBound)
         ⟨n + 1, scheduledCopiedAssignment role n u l r⟩
         s (frequencyRoot n t) (frequencyRoot n t') P) :
       fullAtomTransferWeight role childBound pivotBound ranges leaf (n + 1)
           (scheduledCopiedAssignment role n u l r) (s, t, t') =
         if fullAtomRootGuard role ranges n (scheduledCopiedAssignment role n u l r) P s then
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.ScheduleAtomRange, OAI.Ostmann.ScheduleAtomState, OAI.Ostmann.CopyScheduleY, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.FrequencyTree, OAI.Ostmann.ValidTransferNode, OAI.Ostmann.scheduleAtomSystem, OAI.Ostmann.scheduledCopiedAssignment, OAI.Ostmann.frequencyRoot, OAI.Ostmann.fullAtomTransferWeight, OAI.Ostmann.fullAtomRootGuard