OAI/NumberTheory/Ostmann/Construction/ScheduledRolePrior.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.scheduledRolePrior line 12
2. theorem OAI.Ostmann.scheduledRolePrior_nonneg line 17
3. theorem OAI.Ostmann.scheduledRolePrior_mass line 22
4. theorem OAI.Ostmann.scheduledRolePrior_copied line 29
5. theorem OAI.Ostmann.scheduledRolePrior_copied_product line 40

   Source documentation

   The inherited original marginals give exactly two independent H priors, while every outside marginal is still present exactly once.

   theorem scheduledRolePrior_copied_product {I A : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (μ : I → A → ℝ) (n : ℕ)
       (u : CopyScheduleY role n → A) (l r : CopyScheduleH role n → A) :
       (∏ i, scheduledRolePrior role μ (n + 1) i (scheduledCopiedAssignment role n u l r i)) =
         (∏ y, μ (copyScheduleOrigin n y.val) (u y)) *
         (∏ h, μ (copyScheduleOrigin n h.val) (l h)) *
         (∏ h, μ (copyScheduleOrigin n h.val) (r h)) := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleY, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.scheduledRolePrior, OAI.Ostmann.scheduledCopiedAssignment, OAI.Ostmann.copyScheduleOrigin

6. theorem OAI.Ostmann.scheduledHarmonicPrior_mass line 52

   Source documentation

   Harmonic marginal normalization holds on the actual surviving schedule, including unequal original prime cells.

   theorem scheduledHarmonicPrior_mass {I : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (P : Finset ℕ) (Q : I → Finset ℕ)
       (hQP : ∀ i, Q i ⊆ P) (hQ : ∀ i, (∑ p ∈ Q i, (p : ℝ)⁻¹) ≠ 0) (n : ℕ) :
       (∑ x : ({i : CopyScheduleVertex I n // CopyScheduleSurvives role n i} → P),
         ∏ i, scheduledRolePrior role (fun j => primeSubsetPrior P (Q j)) n i (x i)) = 1 :=
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleVertex, OAI.Ostmann.CopyScheduleSurvives, OAI.Ostmann.scheduledRolePrior, OAI.Ostmann.primeSubsetPrior