OAI/NumberTheory/Ostmann/Construction/RepeatedPrior.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.repeated_prior_weight_le line 16

   Source documentation

   Keep one occurrence's prior and charge the other occurrences their pointwise bounds.

   theorem repeated_prior_weight_le {I : Type*} [DecidableEq I]
       (S : Finset I) (i : I) (hi : i ∈ S) (μ : I → ℝ) (b E : ℝ)
       (hb : 2 ≤ b) (hμ : ∀ j ∈ S, 0 ≤ μ j)
       (hbound : ∀ j ∈ S.erase i, b * μ j ≤ E) :
       (∏ j ∈ S, b * μ j) / (b - 1) ≤ 2 * μ i * E ^ (S.card - 1) := by
   …

2. theorem OAI.Ostmann.repeated_prior_sum_le line 41

   Source documentation

   Summing a repeated sample loses no factor from the number of possible prime values.

   theorem repeated_prior_sum_le {I B : Type*} [DecidableEq I]
       (S : Finset I) (i : I) (hi : i ∈ S) (P : Finset B)
       (μ : I → B → ℝ) (value : B → ℝ) (E : ℝ) (hE : 0 ≤ E)
       (hb : ∀ b ∈ P, 2 ≤ value b) (hμ : ∀ j ∈ S, ∀ b ∈ P, 0 ≤ μ j b)
       (hbound : ∀ j ∈ S.erase i, ∀ b ∈ P, value b * μ j b ≤ E)
       (hmass : (∑ b ∈ P, μ i b) ≤ 1) :
       (∑ b ∈ P, (∏ j ∈ S, value b * μ j b) / (value b - 1)) ≤
         2 * E ^ (S.card - 1) := by
   …