OAI/NumberTheory/Ostmann/Construction/FixedPivotPrior.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.scheduled_prior_fubini_real line 11
2. theorem OAI.Ostmann.constituent_fixedPivot_prior_fubini line 38

   Source documentation

   Every pivot constituent is integrated out, leaving one copy of each H/Y law.

   theorem constituent_fixedPivot_prior_fubini {I D : Type*} [Fintype I] [Fintype D]
       (role : I → CopyScheduleRole) (size : I → ℕ) (n M : ℕ) (p : I)
       (hp : role p = .pivot n) (hu : ∀ i, role i = .pivot n → i = p)
       (P : Finset ℕ) (μ : SurvivingConstituent role size n → P → ℝ)
       (hmass : ∀ i, ∑ a, μ i a = 1)
       (F : D → (CopyScheduleAtoms role n → ℕ) → ℝ) :
       (∑ d, ∑ q : SurvivingConstituent role size n → P,
         (∏ i, μ i (q i)) * F d (scheduledReplacePivot role n M
           (fun a => ((scheduleConstituentWord role size n a).map (fun v => (q v : ℕ))).prod))) =
       let e := pivotConstituentEquiv role size n p hp hu
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.SurvivingConstituent, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.scheduledReplacePivot, OAI.Ostmann.scheduleConstituentWord, OAI.Ostmann.pivotConstituentEquiv