OAI/NumberTheory/Ostmann/Construction/ScheduledPriorFubini.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.scheduledPartitionAssignment line 12
2. theorem OAI.Ostmann.scheduledPartitionAssignment_apply line 18
3. def OAI.Ostmann.scheduledPartitionAssignmentEquiv line 26
4. theorem OAI.Ostmann.scheduledPartitionAssignment_prior line 52

   Source documentation

   The retained outside prior occurs once, while the pivot and H priors stay in their own independent blocks.

   theorem scheduledPartitionAssignment_prior {I A : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (n r : ℕ) (e : Fin r ≃ CurrentPivotConstituent role n)
       (μ : {i : CopyScheduleVertex I n // CopyScheduleSurvives role n i} → A → ℝ)
       (u : CopyScheduleY role n → A) (x : Fin r → A) (l : CopyScheduleH role n → A) :
       (∏ i, μ i (scheduledPartitionAssignment role n r e u x l i)) =
         (∏ y, μ (enumeratedPartitionEquiv role n r e (.inr (.inr y))) (u y)) *
         (∏ i, μ (enumeratedPartitionEquiv role n r e (.inl i)) (x i)) *
         (∏ h, μ (enumeratedPartitionEquiv role n r e (.inr (.inl h))) (l h)) := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CurrentPivotConstituent, OAI.Ostmann.CopyScheduleVertex, OAI.Ostmann.CopyScheduleSurvives, OAI.Ostmann.CopyScheduleY, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.scheduledPartitionAssignment, OAI.Ostmann.enumeratedPartitionEquiv

5. theorem OAI.Ostmann.scheduled_prior_fubini line 67

   Source documentation

   This is the precise finite Fubini identity used by the current amplitude; it changes no marginal, including the common outside sample.

   theorem scheduled_prior_fubini {I A : Type*} [Fintype I] [Fintype A]
       (role : I → CopyScheduleRole) (n r : ℕ) (e : Fin r ≃ CurrentPivotConstituent role n)
       (μ : {i : CopyScheduleVertex I n // CopyScheduleSurvives role n i} → A → ℝ)
       (F : ({i : CopyScheduleVertex I n // CopyScheduleSurvives role n i} → A) → ℂ) :
       (∑ a, ((∏ i, μ i (a i) : ℝ) : ℂ) * F a) =
         ∑ u : CopyScheduleY role n → A,
           ((∏ y, μ (enumeratedPartitionEquiv role n r e (.inr (.inr y))) (u y) : ℝ) : ℂ) *
           ∑ x : Fin r → A,
             ((∏ i, μ (enumeratedPartitionEquiv role n r e (.inl i)) (x i) : ℝ) : ℂ) *
             ∑ l : CopyScheduleH role n → A,
               ((∏ h, μ (enumeratedPartitionEquiv role n r e (.inr (.inl h))) (l h) : ℝ) : ℂ) *
                 F (scheduledPartitionAssignment role n r e u x l) := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CurrentPivotConstituent, OAI.Ostmann.CopyScheduleVertex, OAI.Ostmann.CopyScheduleSurvives, OAI.Ostmann.CopyScheduleY, OAI.Ostmann.enumeratedPartitionEquiv, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.scheduledPartitionAssignment