Local integrability of log ‖x‖ and of log (log t)

On a finite-dimensional real normed space with an additive Haar measure, the function x ↦ log ‖x‖ is locally integrable. Its only singularity is at the origin, where it is dominated by ‖x‖ ^ (-1 / 2), which is locally integrable in every positive dimension. In the plane this is the local integrability of the logarithmic fundamental solution of the Laplacian.

On the half-line [1, ∞) the iterated logarithm t ↦ log (log t) is locally integrable as well: its singularity at t = 1 is integrable, by Mathlib's Real.integrableOn_log_log_mul_rpow. This is the integrability that Abelian arguments against log log t need, as in Mertens' theorems.

Main declarations

• TauCeti.locallyIntegrable_log_norm: x ↦ log ‖x‖ is locally integrable.
• TauCeti.locallyIntegrableOn_log_log: t ↦ log (log t) is locally integrable on [1, ∞).

theorem TauCeti.locallyIntegrable_log_norm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] : MeasureTheory.LocallyIntegrable (fun (x : E) => Real.log ‖x‖) μ

On a finite-dimensional real normed space with an additive Haar measure, x ↦ log ‖x‖ is locally integrable.

theorem TauCeti.locallyIntegrableOn_log_log : MeasureTheory.LocallyIntegrableOn (fun (t : ℝ) => Real.log (Real.log t)) (Set.Ici 1) MeasureTheory.volume

t ↦ log (log t) is locally integrable on [1, ∞): its logarithmic singularity at t = 1 is integrable. This lets Abelian integrals ∫_1^∞ t ^ (-s) f(t) dt treat log (log t) like any other locally integrable weight up to the endpoint t = 1.