LogProductBounds.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Finite logarithmic errors for prime-product normalizations

The quadratic logarithmic error is summable above the lower prime cutoff. The inverse factors in the exact Bernoulli product mass are controlled separately by a reciprocal sum over the selected primes.

theorem OAI.JointDickman.log_one_sub_add_error line 18
theorem OAI.JointDickman.finite_log_product_error line 29

theorem OAI.JointDickman.prime_log_product_error line 41

Source documentation

A selected-prime normalizer differs logarithmically from the linear reciprocal-prime sum by at most the reciprocal-square tail.

theorem prime_log_product_error (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
    {z : ℝ} (hz : 0 ≤ z) (hz1 : z ≤ 1) {N : ℕ} (hN : N ≠ 0)
    (hcut : ∀ p ∈ P, N < p) :
    |Real.log (∏ p ∈ P, (1 - z / (p : ℝ))) + z * ∑ p ∈ P, 1 / (p : ℝ)| ≤
      2 * z ^ 2 / (N : ℝ) := by
…

theorem OAI.JointDickman.inverse_product_le_exp line 70

Source documentation

The exact odds correction is bounded by an exponential of the selected reciprocal mass, uniformly in the number of allowed primes.

theorem inverse_product_le_exp {ι : Type*} (P : Finset ι) (x : ι → ℝ)
    (hx : ∀ i ∈ P, 0 ≤ x i ∧ x i ≤ 1 / 2) :
    (∏ i ∈ P, (1 - x i)⁻¹) ≤ Real.exp (2 * ∑ i ∈ P, x i) := by
…