Improper-integral asymptotics and logarithmic decay

This file extends Mathlib's improper-integral estimates with an asymptotic estimate for weighted integrals, integrability at infinity of (t (1 + log t) ^ 2)⁻¹, and the closed form ∫_A^∞ dy / y² = 1 / A as a Lebesgue integral.

Main declarations

• TauCeti.lintegral_Ioi_inv_sq: ∫⁻ y in Ioi A, (1 / ‖y‖₊) ^ 2 = ofReal A⁻¹ for 0 < A, the integrand being the density of the hyperbolic area measure.

• TauCeti.integrableAtFilter_inv_mul_one_add_log_sq: the function t ↦ (t (1 + log t) ^ 2)⁻¹ is integrable at infinity.

• TauCeti.isLittleO_integral_rpow_sub_one_mul: a remainder E t = o(t) has ∫ t in 1..x, t ^ (τ - 1) * E t = o(x ^ (τ + 1)).

theorem TauCeti.isLittleO_integral_rpow_sub_one_mul {E : ℝ → ℝ} {τ : ℝ} (hτ : -1 < τ) (hE_int : ∀ (x : ℝ), 1 ≤ x → IntervalIntegrable E MeasureTheory.volume 1 x) (hE : E =o[Filter.atTop] id) : (fun (x : ℝ) => ∫ (t : ℝ) in 1..x, t ^ (τ - 1) * E t) =o[Filter.atTop] fun (x : ℝ) => x ^ (τ + 1)

A remainder o(t) integrates to o(x ^ (τ + 1)) against t ^ (τ - 1). If E is interval integrable above 1 and E t = o(t), then for every exponent τ > -1 the weighted integral ∫ t in 1..x, t ^ (τ - 1) * E t is o(x ^ (τ + 1)).

theorem TauCeti.integrableAtFilter_inv_mul_one_add_log_sq : MeasureTheory.IntegrableAtFilter (fun (u : ℝ) => (u * (1 + Real.log u) ^ 2)⁻¹) Filter.atTop MeasureTheory.volume

The function (t (1 + log t) ^ 2)⁻¹ is integrable at infinity. On Ioi 1 it is dominated by Mathlib's log-Cauchy density (t (1 + (log t) ^ 2))⁻¹.

theorem TauCeti.lintegral_Ioi_inv_sq {A : ℝ} (hA : 0 < A) : ∫⁻ (y : ℝ) in Set.Ioi A, ↑((1 / ‖y‖₊) ^ 2) = ENNReal.ofReal A⁻¹

The improper integral of 1 / y²: ∫_A^∞ dy / y² = 1 / A for 0 < A, as a Lebesgue integral of the nonnegative function (1 / ‖y‖₊) ^ 2.