HarmonicSummation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Partial summation for the local prime-product law

Harmonic weighting of a counting estimate costs only the logarithmic length of the interval. The finite counting function is kept explicit.

def OAI.JointDickman.finiteCountingFunction line 19
theorem OAI.JointDickman.sum_div_eq_boundary_add_integral line 22
theorem OAI.JointDickman.finiteCountingFunction_div_sq_integrable line 47

theorem OAI.JointDickman.integral_counting_error_le line 59

Source documentation

The integrated counting error is controlled by the logarithmic length.

theorem integral_counting_error_le (w : ℕ → ℝ) (F : ℝ → ℝ) {a b ε : ℝ}
    (ha : 0 < a) (hab : a ≤ b)
    (herr : ∀ t ∈ Set.Icc a b, |finiteCountingFunction w t - F t| ≤ ε * t) :
    |∫ t in a..b, (finiteCountingFunction w t - F t) / t ^ 2| ≤ ε * Real.log (b / a) := by
…

Mentions: OAI.JointDickman.finiteCountingFunction

theorem OAI.JointDickman.harmonic_counting_error_le line 81

Source documentation

Harmonic weighting loses at most two endpoint errors and one logarithm.

theorem harmonic_counting_error_le (w : ℕ → ℝ) (F : ℝ → ℝ) {a b ε : ℝ}
    (ha : 0 < a) (hab : a ≤ b) (hF : ContinuousOn F (Set.Icc a b))
    (herr : ∀ t ∈ Set.Icc a b, |finiteCountingFunction w t - F t| ≤ ε * t) :
    |(∑ n ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, w n / (n : ℝ)) -
      (F b / b - F a / a + ∫ t in a..b, F t / t ^ 2)| ≤
        ε * (2 + Real.log (b / a)) := by
…

Mentions: OAI.JointDickman.finiteCountingFunction

theorem OAI.JointDickman.harmonic_model_integral line 123

Source documentation

Integration of the model's derivative gives the same harmonic model.

theorem harmonic_model_integral (F M : ℝ → ℝ) {a b : ℝ}
    (ha : 0 < a) (hab : a ≤ b)
    (hF : ∀ t ∈ Set.Icc a b, HasDerivAt F (M t) t)
    (hM : ContinuousOn M (Set.Icc a b)) :
    (∫ t in a..b, M t / t) = F b / b - F a / a + ∫ t in a..b, F t / t ^ 2 := by
…