ReciprocalTail.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Quantitative reciprocal-square tails

The error in the independent-product replacement is controlled by the tail of all integers; no prime number theorem is needed here.

theorem OAI.JointDickman.sum_reciprocal_square_tail line 17

theorem OAI.JointDickman.twoSplitPrimeProducts_cell_tail_bound line 33

Source documentation

The cell probability comparison has error at most 9/(8N) when all allowed primes exceed N.

theorem twoSplitPrimeProducts_cell_tail_bound (Q : Finset ℕ)
    (hQ : ∀ p ∈ Q, p.Prime) {N : ℕ} (hN : N ≠ 0)
    (hcut : ∀ p ∈ Q, N < p) (A B : Set ℕ) :
    |(∑ x, if (actualSplitProducts Q x).1 ∈ A ∧ (actualSplitProducts Q x).2 ∈ B then
        sameSiteTwoSplitProductMass (fun p : Q => 1 / (p.val : ℝ)) x else 0) -
      (∑ y, if (independentSplitProducts Q y).1 ∈ A ∧ (independentSplitProducts Q y).2 ∈ B then
        bernoulliProductMass univ
          (fun (p : Q) (_ : Fin 3) => 1 / (4 * (p.val : ℝ))) y else 0)| ≤
      9 / (8 * N : ℝ) := by
…

Mentions: OAI.JointDickman.actualSplitProducts, OAI.JointDickman.sameSiteTwoSplitProductMass, OAI.JointDickman.independentSplitProducts, OAI.JointDickman.bernoulliProductMass