feat(Analysis/SpecialFunctions/ImproperIntegrals): Frullani integral#34815
Open
Deep0Thinking wants to merge 17 commits intoleanprover-community:masterfrom
Open
feat(Analysis/SpecialFunctions/ImproperIntegrals): Frullani integral#34815Deep0Thinking wants to merge 17 commits intoleanprover-community:masterfrom
Deep0Thinking wants to merge 17 commits intoleanprover-community:masterfrom
Conversation
…_div` and `Cont...right_div`
…ral as `Frullani.integral_Ioi`
github-actions
bot
added
the
new-contributor
github-actions
bot
added
the
large-import
PR summary 35186be320Import changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue | 2316 | 2477 | +161 (+6.95%) |
| Mathlib.Analysis.SpecialFunctions.ImproperIntegrals | 2498 | 2500 | +2 (+0.08%) |
Import changes for all files
| Files | Import difference |
|---|---|
95 filesMathlib.Analysis.Distribution.FourierMultiplier Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.Analysis.Distribution.SchwartzSpace.Fourier 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.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.MeasureTheory.Integral.Gamma Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.Cyclotomic.Rat Mathlib.NumberTheory.Cyclotomic.Three Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.NumberTheory.FLT.Three 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.ModularForms.DedekindEta Mathlib.NumberTheory.ModularForms.Delta Mathlib.NumberTheory.ModularForms.Derivative 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.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.Ideal.Asymptotics Mathlib.NumberTheory.NumberField.Ideal.Basic Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.NumberTheory.NumberField.Units.Regulator 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 |
2 |
Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue |
161 |
Declarations diff
+ ContinuousOn.comp_mul_left
+ ContinuousOn.comp_mul_left_div
+ ContinuousOn.comp_mul_right
+ ContinuousOn.comp_mul_right_div
+ comp_mul_left_div
+ integral_Ioi_eq
+ integral_comp_mul_div
+ intervalIntegrable_comp_mul_div
+ le_max_mul_of_mem_uIcc_mul
+ min_mul_le_of_mem_uIcc_mul
+ pos_of_mem_uIcc_mul
+ tendsto_intervalIntegral
++ exists_integral_div_eq_mul_log
You can run this locally as follows
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/reporting/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
Contributor
Author
|
t-analysis |
Deep0Thinking
changed the title
sgouezel
reviewed
Feb 4, 2026
CoolRmal
reviewed
Feb 5, 2026
sgouezel
added
the
awaiting-author
mathlib-dependent-issues
bot
added
the
blocked-by-other-PR
mathlib-dependent-issues
bot
removed
the
blocked-by-other-PR
|
This PR/issue depends on: |
mathlib-merge-conflicts
bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
Deep0Thinking
force-pushed
the
Frullani_integral
branch
3 times, most recently
from
95ec31c to
9d3d5b1
Compare
github-actions
bot
removed
the
merge-conflict
…imit form (`sorry`); improve docstring and variable naming; format
…leOn.tendsto_integral_Ioi`
…ze Frullani's integral to limit form
Contributor
Author
|
-awaiting-author |
github-actions
bot
removed
the
awaiting-author
Contributor
Author
|
@sgouezel Thank you for the comments! I've proved the limit form of Frullani's integral ( |
sgouezel
reviewed
Apr 6, 2026
Contributor
sgouezel
left a comment
sgouezel
left a comment
There was a problem hiding this comment.
You're wirting this for functions taking values in R. But isn't this true for any function taking values in a (complete) real normed space? The strategy would have to be slightly different as lemmas such as exists_integral_div_eq_mul_log would not apply any more (this is specifically a one-dimensional phenomenon) but I guess the result will still be true.
sgouezel
added
the
awaiting-author
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
continuousWithinAt_Ici/Iic_primitive_Ioi/IioandcontinuousOn_Ici/Iic_primitive_Ioi/Iio/Ici/Iic#34966Add a proof of Frullani integral.
Main theorems:
Frullani.integral_IoiIntegrableOn.tendsto_integral_Ioiexists_integral_div_eq_mul_logSupporting lemmas:
Frullani.comp_mul_left_divFrullani.intervalIntegrable_divFrullani.exists_integral_div_eq_mul_logIoi_diff_IocContinuousOn.comp_mul_left_div,ContinuousOn.comp_mul_right_divContinuousOn.comp_mul_left,ContinuousOn.comp_mul_right