OAI/NumberTheory/Ostmann/Construction/ScheduledWordLeafPrior.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.scheduled_wordLeaf_sum line 10
2. theorem OAI.Ostmann.scheduled_wordLeaf_sum_le line 33

   Source documentation

   A bound for each fixed assignment of the remaining primes averages without any loss. The selected 2^n prime marginals remain the original ones.

   theorem scheduled_wordLeaf_sum_le {I A D : Type*}
       [Fintype I] [Fintype A] [Fintype D]
       (role : I → CopyScheduleRole) (i : I) (hi : role i = .word) (n : ℕ)
       (μ : I → A → ℝ) (hμ : ∀ j a, 0 ≤ μ j a) (hmass : ∀ j, ∑ a, μ j a = 1)
       (F : D → (CopyScheduleAtoms role n → A) → ℝ) (B : ℝ)
       (hsection : ∀ y : WordLeafOutside role i hi n → A,
         (∑ d, ∑ x : TreeLeafIndex n → A, (∏ t, μ i (x t)) *
           F d (wordLeafAssignment role i hi n y x)) ≤ B) :
       (∑ d, ∑ q, scheduledPrimePrior role n μ q * F d q) ≤ B := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.WordLeafOutside, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.wordLeafAssignment, OAI.Ostmann.scheduledPrimePrior