Commit 2026-07-08 03:27 6420e6d6

feat(Analysis/SpecialFunctions/Log/InvLog): add more API for inv_log and log_log (#40847) 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.