Auxiliary tail lemmas for primitive sets above x

This file contains the standalone calculus lemmas reused in the proof of tailEstimate. Its main output is a small API for the model kernels 1 / (t log(ct)^2) and 2 / (t log(ct)^3): each kernel is integrable on an admissible tail, and its tail integral can be computed exactly.

Main statements

• integrableOn_Ioi_inv_log_sq
• integral_Ioi_inv_log_sq
• integrableOn_Ioi_two_inv_log_cube
• integral_Ioi_two_inv_log_cube

theorem PrimitiveSetsAboveX.hasDerivAt_inv_log_mul {c t : ℝ} (hc : 0 < c) (hct : 1 < c * t) : HasDerivAt (fun (u : ℝ) => (Real.log (c * u))⁻¹) (-(1 / (t * Real.log (c * t) ^ 2))) t

The logarithmic antiderivative underlying tailEstimate has derivative -1 / (t log(ct)^2).

theorem PrimitiveSetsAboveX.hasDerivAt_inv_log_sq_mul {c t : ℝ} (hc : 0 < c) (hct : 1 < c * t) : HasDerivAt (fun (u : ℝ) => (Real.log (c * u))⁻¹ ^ 2) (-(2 / (t * Real.log (c * t) ^ 3))) t

Squaring the inverse logarithm gives the exact derivative -2 / (t log(ct)^3).

theorem PrimitiveSetsAboveX.integrableOn_Ioi_inv_log_sq {c y : ℝ} (hc : 0 < c) (hy : 1 < c * y) : MeasureTheory.IntegrableOn (fun (t : ℝ) => 1 / (t * Real.log (c * t) ^ 2)) (Set.Ioi y) MeasureTheory.volume

The logarithmic kernel 1 / (t log(ct)^2) is integrable on every admissible tail.

theorem PrimitiveSetsAboveX.integral_Ioi_inv_log_sq {c y : ℝ} (hc : 0 < c) (hy : 1 < c * y) : ∫ (t : ℝ) in Set.Ioi y, 1 / (t * Real.log (c * t) ^ 2) = (Real.log (c * y))⁻¹

The integral of 1 / (t log(ct)^2) over a tail is exactly 1 / log(cy).

theorem PrimitiveSetsAboveX.integrableOn_Ioi_two_inv_log_cube {c y : ℝ} (hc : 0 < c) (hy : 1 < c * y) : MeasureTheory.IntegrableOn (fun (t : ℝ) => 2 / (t * Real.log (c * t) ^ 3)) (Set.Ioi y) MeasureTheory.volume

The cubic logarithmic kernel 2 / (t log(ct)^3) is integrable on every admissible tail.

theorem PrimitiveSetsAboveX.integral_Ioi_two_inv_log_cube {c y : ℝ} (hc : 0 < c) (hy : 1 < c * y) : ∫ (t : ℝ) in Set.Ioi y, 2 / (t * Real.log (c * t) ^ 3) = (Real.log (c * y))⁻¹ ^ 2

The integral of 2 / (t log(ct)^3) over a tail equals the square of the inverse logarithm.