OAI/NumberTheory/Ostmann/Construction/ConstituentCopiedWeight.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.copiedConstituentAtomValues line 12
2. theorem OAI.Ostmann.constituentTransferWeight_product line 24

   Source documentation

   The two old coefficients multiply to the next full coefficient with exactly two original H priors; no outside prior is squared here.

   theorem constituentTransferWeight_product {I : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (size : I → ℕ) (n : ℕ)
       (P : Finset ℕ) (Q : (Σ i, Fin (size i)) → Finset ℕ)
       (childBound pivotBound : ℕ → ℕ) (ranges : (j : ℕ) → List (ScheduleAtomRange role j))
       (leaf : ScheduleAtomState role → ℤ → ℂ)
       (u : CopyScheduleY (fun i : Σ a, Fin (size a) => role i.1) n → P)
       (l r : CopyScheduleH (fun i : Σ a, Fin (size a) => role i.1) n → P)
       (s : ℤ) (t t' : FrequencyTree ℤ n) (M : ℕ)
       (hP : ValidTransferNode (scheduleAtomSystem role childBound pivotBound)
         ⟨n + 1, copiedConstituentAtomValues role size n P u l r⟩
         s (frequencyRoot n t) (frequencyRoot n t') M)
       (hroot : fullAtomRootGuard role ranges n (copiedConstituentAtomValues role size n P u l r) M s)
   …

   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.copiedConstituentAtomValues, OAI.Ostmann.frequencyRoot, OAI.Ostmann.fullAtomRootGuard