OAI/NumberTheory/Ostmann/Construction/InitialLogSumRate.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.logSumCenter_count_bound line 10
2. theorem OAI.Ostmann.halfPower_div_logSumCenters line 27
3. theorem OAI.Ostmann.exists_balanced_prime_log_sum_center line 52

   Source documentation

   A literal logarithmic-sum weight with mass at least exp(-C m). The constant is independent of the later gap parameters and transfer depth.

   theorem exists_balanced_prime_log_sum_center (P : Finset ℕ)
       (hP : ∀ p ∈ P, p.Prime) (n m : ℕ) (T : ℝ)
       (μ : Fin n → P → ℝ) (good : Fin n → P → Prop)
       (hm : 1 ≤ m) (hn : n ≤ m) (hT : T ≤ m)
       (hlog : ∀ p : P, Real.log (p : ℝ) ≤ Real.exp T)
       (hmass : ∀ i, (1 / 2 : ℝ) ≤ ∑ p, if good i p then μ i p else 0) :
       ∃ c ∈ Finset.Icc (0 : ℤ) ⌈(n : ℝ) * Real.exp T⌉₊,
         Real.exp (-(Real.log 2 + 2) * m) ≤
           ∑ x ∈ balancedTupleSet n good, productPrior μ x *
             logCellProfile ((∑ i, Real.log (x i : ℝ)) - c) := by
   …

   Mentions: OAI.Ostmann.balancedTupleSet, OAI.Ostmann.productPrior, OAI.Ostmann.logCellProfile