FloorErrors.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Replacing divisibility counts by reciprocal products

Replacing floor(N/d)/N by 1/d over admissible prime tuples has an explicit finite error. This error tends to zero when the number of tuples is o(N).

theorem OAI.JointDickman.normalized_division_error line 19
theorem OAI.JointDickman.finite_divisibility_error line 35

theorem OAI.JointDickman.divisibility_error_tendsto_zero line 49

Source documentation

A sublinear number of terms makes the complete floor replacement error vanish. The tuple family is allowed to vary with the counting scale.

theorem divisibility_error_tendsto_zero {ι : Type*}
    (s : ℕ → Finset ι) (d : ℕ → ι → ℕ)
    (hd : ∀ N i, i ∈ s N → 0 < d N i)
    (hsmall : Tendsto (fun N => ((s N).card : ℝ) / N) atTop (𝓝 0)) :
    Tendsto (fun N =>
      (∑ i ∈ s N, ((N / d N i : ℕ) : ℝ)) / N -
        ∑ i ∈ s N, 1 / (d N i : ℝ)) atTop (𝓝 0) := by
…