OAI/NumberTheory/Ostmann/Construction/ConstituentPriorAssembly.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.scheduledPartitionAssignment_map line 12
2. theorem OAI.Ostmann.constituent_weighted_prior_fubini line 25

   Source documentation

   The pivot tuple and both remaining coordinate blocks keep their original marginals. The full coefficient depends on the pivot tuple only through its product, as required by the arithmetic Cauchy step.

   theorem constituent_weighted_prior_fubini {I D : Type*} [Fintype I] [Fintype D]
       (role : I → CopyScheduleRole) (size : I → ℕ) (n : ℕ) (p : I)
       (hp : role p = .pivot n) (hu : ∀ i, role i = .pivot n → i = p)
       (P : Finset ℕ) (μ : SurvivingConstituent role size n → P → ℝ)
       (childBound pivotBound : ℕ → ℕ) (ranges : (j : ℕ) → List (ScheduleAtomRange role j))
       (leaf : ScheduleAtomState role → ℤ → ℂ) (hist : D → FrequencyTree ℤ n)
       (phase : (SurvivingConstituent role size n → P) → D → ℂ) :
       (∑ q : SurvivingConstituent role size n → P, ((∏ i, μ i (q i) : ℝ) : ℂ) *
         ∑ d, fullAtomTransferWeight role childBound pivotBound ranges leaf n
           (fun v => ((scheduleConstituentWord role size n v).map (fun i => (q i : ℕ))).prod)
           (hist d) * phase q d) =
       let e := pivotConstituentEquiv role size n p hp hu
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.SurvivingConstituent, OAI.Ostmann.ScheduleAtomRange, OAI.Ostmann.ScheduleAtomState, OAI.Ostmann.FrequencyTree, OAI.Ostmann.fullAtomTransferWeight, OAI.Ostmann.scheduleConstituentWord, OAI.Ostmann.pivotConstituentEquiv