OAI/NumberTheory/Ostmann/Construction/CopiedPriorFubini.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.scheduledCopiedAssignment line 11
2. theorem OAI.Ostmann.scheduledCopiedAssignment_left line 20
3. theorem OAI.Ostmann.scheduledCopiedAssignment_right line 25
4. theorem OAI.Ostmann.scheduledCopiedAssignment_outside line 30
5. def OAI.Ostmann.scheduledCopiedAssignmentEquiv line 35
6. theorem OAI.Ostmann.scheduledCopiedAssignment_prior line 62
7. theorem OAI.Ostmann.copied_prior_fubini line 77

   Source documentation

   The off-diagonal sum samples two independent H copies and retains one Y. No second outside prior is inserted when passing to the next level.

   theorem copied_prior_fubini {I A : Type*} [Fintype I] [Fintype A]
       (role : I → CopyScheduleRole) (n : ℕ)
       (μ : {i : CopyScheduleVertex I (n + 1) // CopyScheduleSurvives role (n + 1) i} → A → ℝ)
       (F : ({i : CopyScheduleVertex I (n + 1) // CopyScheduleSurvives role (n + 1) i} → A) → ℂ) :
       (∑ a, ((∏ i, μ i (a i) : ℝ) : ℂ) * F a) =
         ∑ u : CopyScheduleY role n → A,
           ((∏ y, μ (scheduledOutputVertex role n (.inr y)) (u y) : ℝ) : ℂ) *
           ∑ l : CopyScheduleH role n → A,
             ((∏ h, μ (scheduledOutputVertex role n (.inl (true, h))) (l h) : ℝ) : ℂ) *
             ∑ r : CopyScheduleH role n → A,
               ((∏ h, μ (scheduledOutputVertex role n (.inl (false, h))) (r h) : ℝ) : ℂ) *
                 F (scheduledCopiedAssignment role n u l r) := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleVertex, OAI.Ostmann.CopyScheduleSurvives, OAI.Ostmann.CopyScheduleY, OAI.Ostmann.scheduledOutputVertex, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.scheduledCopiedAssignment