feat(Analysis/SpecialFunctions/Log/InvLog): add more API for inv_log and log_log

[teorth]

Add a simp lemma form Real.deriv_inv_log' of Real.deriv_inv_log, in analogy with Real.deriv_inv and Real.deriv_inv', or Real.deriv_log' and Real.deriv_log. There were two downstream applications of Real.deriv_inv_log that received minor golfs as a consequence. Also added some helper lemmas for the associated DifferentiableAt and HasDeriv versions, as well as variants for the double logarithm. As applications, definite integrals of t⁻¹ / log t and t⁻¹ / (log t)^2 were added to Analysis.SpecialFunctions.Integrals.Basic, and improper integrals of t⁻¹ / (log t)^2 were added to Analysis.SpecialFunctions.ImproperIntegrals.

Also added two asymptotic lemmas, asserting that (fun x ↦ 1 / log x) =o[atTop] (fun _ ↦ (1:ℝ)) and (fun _ ↦ (1:ℝ)) =o[atTop] (fun x ↦ log (log x)), which will be needed to establish Mertens' second theorem.

---

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary f296b3fdd4

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.SpecialFunctions.Integrals.Basic	2514	2515	+1 (+0.04%)
Mathlib.Analysis.SpecialFunctions.ImproperIntegrals	2536	2537	+1 (+0.04%)

Import changes for all files

Files

Import difference

146 files Mathlib.Analysis.Complex.JensenFormula Mathlib.Analysis.Complex.ValueDistribution.Cartan Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation Mathlib.Analysis.Distribution.FourierMultiplier Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.Analysis.Distribution.SchwartzSpace.Fourier Mathlib.Analysis.Distribution.Sobolev Mathlib.Analysis.Distribution.Support Mathlib.Analysis.Distribution.TemperedDistribution Mathlib.Analysis.Fourier.Convolution Mathlib.Analysis.Fourier.Inversion Mathlib.Analysis.Fourier.LpSpace Mathlib.Analysis.Fourier.PoissonSummation Mathlib.Analysis.MellinInversion Mathlib.Analysis.MellinTransform Mathlib.Analysis.Meromorphic.Complex Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn Mathlib.Analysis.Normed.Ring.InfiniteProd Mathlib.Analysis.ODE.ExistUnique Mathlib.Analysis.ODE.PicardLindelof Mathlib.Analysis.Polynomial.MahlerMeasure Mathlib.Analysis.Real.Pi.Irrational Mathlib.Analysis.Real.Pi.Leibniz Mathlib.Analysis.Real.Pi.Wallis Mathlib.Analysis.SpecialFunctions.Complex.Arctan Mathlib.Analysis.SpecialFunctions.Complex.LogBounds Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order Mathlib.Analysis.SpecialFunctions.Gamma.Basic Mathlib.Analysis.SpecialFunctions.Gamma.Beta Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup Mathlib.Analysis.SpecialFunctions.Gamma.Deligne Mathlib.Analysis.SpecialFunctions.Gamma.Deriv Mathlib.Analysis.SpecialFunctions.Gamma.Digamma Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation Mathlib.Analysis.SpecialFunctions.ImproperIntegrals Mathlib.Analysis.SpecialFunctions.Integrals.Basic Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage Mathlib.Analysis.SpecialFunctions.Log.Summable Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Analysis.SpecialFunctions.Stirling Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd Mathlib.Analysis.SumIntegralExpDecay Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique Mathlib.Geometry.Manifold.IntegralCurve.UniformTime Mathlib.MeasureTheory.Constructions.HaarToSphere Mathlib.MeasureTheory.Integral.Gamma Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion Mathlib.MeasureTheory.Measure.CharacteristicFunction Mathlib.MeasureTheory.Measure.FiniteMeasureExt Mathlib.MeasureTheory.Measure.IntegralCharFun Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls Mathlib.MeasureTheory.Measure.LevyConvergence Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.Harmonic.Bounds Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.NumberTheory.LSeries.AbstractFuncEq Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.NumberTheory.LSeries.HurwitzZetaEven Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.NumberTheory.LSeries.HurwitzZeta Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.NumberTheory.LSeries.Nonvanishing Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.NumberTheory.LSeries.SumCoeff Mathlib.NumberTheory.LSeries.ZMod Mathlib.NumberTheory.LSeries.ZetaZeros Mathlib.NumberTheory.MahlerMeasure Mathlib.NumberTheory.ModularForms.CuspFormSubmodule Mathlib.NumberTheory.ModularForms.DedekindEta Mathlib.NumberTheory.ModularForms.Delta Mathlib.NumberTheory.ModularForms.Derivative Mathlib.NumberTheory.ModularForms.DimensionFormulas.LevelOne Mathlib.NumberTheory.ModularForms.Discriminant Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing Mathlib.NumberTheory.NumberField.CMField Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.NumberTheory.NumberField.Cyclotomic.Basic Mathlib.NumberTheory.NumberField.Cyclotomic.Galois Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal Mathlib.NumberTheory.NumberField.Cyclotomic.PID Mathlib.NumberTheory.NumberField.Cyclotomic.Three Mathlib.NumberTheory.NumberField.DedekindZeta Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.NumberField.Discriminant.Different Mathlib.NumberTheory.NumberField.ExistsRamified Mathlib.NumberTheory.NumberField.Ideal.Asymptotics Mathlib.NumberTheory.NumberField.Ideal.Basic Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.Probability.BrownianMotion.Basic Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily Mathlib.Probability.CentralLimitTheorem Mathlib.Probability.Distributions.Beta Mathlib.Probability.Distributions.Cauchy Mathlib.Probability.Distributions.Exponential Mathlib.Probability.Distributions.Gamma Mathlib.Probability.Distributions.Gaussian.Basic Mathlib.Probability.Distributions.Gaussian.CharFun Mathlib.Probability.Distributions.Gaussian.Fernique Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Def Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Def Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence Mathlib.Probability.Distributions.Gaussian.Multivariate Mathlib.Probability.Distributions.Gaussian.Real Mathlib.Probability.Distributions.Pareto Mathlib.Probability.Distributions.Poisson.Basic Mathlib.Probability.Distributions.Poisson.PoissonLimitThm Mathlib.Probability.Independence.CharacteristicFunction Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess Mathlib.Probability.Moments.ComplexMGF Mathlib.Probability.Moments.MGFAnalytic Mathlib.Probability.Moments.SubGaussian Mathlib.Probability.Moments.Tilted

1

---

Declarations diff (regex)

+ deriv_inv_log'
+ deriv_log_log
+ differentiableAt_inv_log
+ differentiableAt_log_log
+ differentiableOn_inv_log
+ differentiableOn_log_log
+ hasDerivAt_inv_log
+ hasDerivAt_log_log
+ integrableOn_Ioi_inv_div_log_sq
+ integral_Ioi_inv_divlog_sq
+ integral_inv_div_log
+ integral_inv_div_log_sq
+ inv_log_eq_o_one
+ one_eq_o_log_log

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit f296b3f).

• +14 new declarations
• −0 removed declarations

+Real.deriv_inv_log'
+Real.deriv_log_log
+Real.differentiableAt_inv_log
+Real.differentiableAt_log_log
+Real.differentiableOn_inv_log
+Real.differentiableOn_log_log
+Real.hasDerivAt_inv_log
+Real.hasDerivAt_log_log
+Real.inv_log_eq_o_one
+Real.one_eq_o_log_log
+integrableOn_Ioi_inv_div_log_sq
+integral_Ioi_inv_divlog_sq
+integral_inv_div_log
+integral_inv_div_log_sq

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit f296b3fdd4
Reference commit bdf26e4015

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).