LogImbalanceVariance.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Logarithmic imbalance from the collision variance

theorem OAI.Ostmann.log_sq_le_four_variance_of_one_le line 13
theorem OAI.Ostmann.log_sq_le_four_variance line 39

theorem OAI.Ostmann.logarithmic_imbalance_budget line 51

Source documentation

A finite Cauchy--Schwarz form ready for the actual prime collision budget. A harmless absolute factor four avoids any additional analytic theorem.

theorem logarithmic_imbalance_budget (P : Finset ℕ) (κ : ℕ → ℝ)
    (hP : ∀ p ∈ P, 1 < p) (hκ : ∀ p ∈ P, 0 < κ p) :
    (∑ p ∈ P, |Real.log (κ p)| / p) ^ 2 ≤
      (4 * ∑ p ∈ P, (κ p + (κ p)⁻¹ - 2) * Real.log p / p) *
        ∑ p ∈ P, 1 / ((p : ℝ) * Real.log p) := by
…