[Merged by Bors] - chore(Analysis/Distribution): split off functions and measures of temperate growth by mcdoll · Pull Request #30553 · leanprover-community/mathlib4

mcdoll · 2025-10-14T18:15:01Z

The Schwartz function file reached 1500 lines of code, so it really needs splitting.

The only other change is that I added namespaces and moved one lemma into the MeasureTheory.Measure namespace to allow for dot-notation.

I've added Anatole to the list of authors for the BigO additions, I don't know whether there is someone else that should be mentioned. @mans0954 did you contribute to the temperate growth functions?

I did not write any new doc-strings, so that this PR does not get hung up on that, but this should be done in a subsequent PR.

github-actions · 2025-10-14T18:16:12Z

PR summary e29df49f46

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
20 files `Mathlib.Analysis.Distribution.FourierSchwartz` `Mathlib.Analysis.Distribution.SchwartzSpace` `Mathlib.Analysis.Fourier.PoissonSummation` `Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation` `Mathlib.NumberTheory.EulerProduct.DirichletLSeries` `Mathlib.NumberTheory.Harmonic.ZetaAsymp` `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.Nonvanishing` `Mathlib.NumberTheory.LSeries.PrimesInAP` `Mathlib.NumberTheory.LSeries.RiemannZeta` `Mathlib.NumberTheory.LSeries.ZMod` `Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds` `Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold` `Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable` `Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable`	1
`Mathlib.Analysis.Distribution.TemperateGrowth` (new file)	2432

Declarations diff

+ HasTemperateGrowth.const
+ HasTemperateGrowth.exists_eLpNorm_lt_top
+ HasTemperateGrowth.isBigO
+ HasTemperateGrowth.isBigO_uniform
+ HasTemperateGrowth.norm_iteratedFDeriv_le_uniform_aux
+ HasTemperateGrowth.of_fderiv
+ HasTemperateGrowth.zero
+ IsAddHaarMeasure.instHasTemperateGrowth
+ _root_.integrable_of_le_of_pow_mul_le
+ _root_.integral_pow_mul_le_of_le_of_pow_mul_le
+ _root_.pow_mul_le_of_le_of_pow_mul_le
+ hasTemperateGrowth_iff_isBigO
+ instance _root_.MeasureTheory.IsFiniteMeasure.instHasTemperateGrowth {μ : Measure D}
+ integrablePower
++ HasTemperateGrowth
- _root_.Function.HasTemperateGrowth
- _root_.Function.HasTemperateGrowth.const
- _root_.Function.HasTemperateGrowth.isBigO
- _root_.Function.HasTemperateGrowth.isBigO_uniform
- _root_.Function.HasTemperateGrowth.norm_iteratedFDeriv_le_uniform_aux
- _root_.Function.HasTemperateGrowth.of_fderiv
- _root_.Function.HasTemperateGrowth.zero
- _root_.Function.hasTemperateGrowth_iff_isBigO
- _root_.MeasureTheory.Measure.HasTemperateGrowth
- _root_.MeasureTheory.Measure.HasTemperateGrowth.exists_eLpNorm_lt_top
- _root_.MeasureTheory.Measure.integrablePower
- instance _root_.MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth {μ : Measure D}
- instance _root_.MeasureTheory.Measure.IsFiniteMeasure.instHasTemperateGrowth {μ : Measure D}
- integrable_of_le_of_pow_mul_le
- integral_pow_mul_le_of_le_of_pow_mul_le
- pow_mul_le_of_le_of_pow_mul_le

You can run this locally as follows

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

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/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).

Mathlib/Analysis/Distribution/TemperateGrowth.lean

ADedecker · 2025-10-19T13:20:50Z

Mathlib/Analysis/Distribution/TemperateGrowth.lean

+/-- A measure `μ` has temperate growth if there is an `n : ℕ` such that `(1 + ‖x‖) ^ (- n)` is
+`μ`-integrable. -/
+class HasTemperateGrowth (μ : Measure D) : Prop where
+  exists_integrable : ∃ (n : ℕ), Integrable (fun x ↦ (1 + ‖x‖) ^ (- (n : ℝ))) μ


This has nothing to do with the PR, but why are you using real exponents here? Doesn't it make things more complicated?

Honestly, I don't remember and I agree it looks a bit funny. You do need either real or integer powers, so it might have been easier just do change n to be real or integer.

Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>

ADedecker

Sorry for the delay.

Could you ask Christopher on Zulip about the authorship ? Other than that and these small comments I think this is ready to go.

Mathlib/Analysis/Distribution/TemperateGrowth.lean

Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>

mcdoll

Did a check with git blame and the parts that I was not remembering doing myself were by Sebastien for the Fourier transform.

Mathlib/Analysis/Distribution/TemperateGrowth.lean

ADedecker · 2025-10-28T12:19:32Z

Thanks!

bors d+

mathlib-bors · 2025-10-28T12:19:34Z

✌️ mcdoll can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

mcdoll · 2025-10-29T13:18:31Z

Thanks for the review! I will do the two issues that have come up tomorrow.
bors merge

…perate growth (#30553) The Schwartz function file reached 1500 lines of code, so it really needs splitting. The only other change is that I added namespaces and moved one lemma into the `MeasureTheory.Measure` namespace to allow for dot-notation.

mathlib-bors · 2025-10-29T13:34:29Z

Pull request successfully merged into master.

Build succeeded:

…perate growth (leanprover-community#30553) The Schwartz function file reached 1500 lines of code, so it really needs splitting. The only other change is that I added namespaces and moved one lemma into the `MeasureTheory.Measure` namespace to allow for dot-notation.

initial commit

c2aba67

github-actions bot added the t-analysis Analysis (normed *, calculus) label Oct 14, 2025

mcdoll added 2 commits October 14, 2025 11:19

shake

0c1f1cd

mk_all

55317ba

mcdoll mentioned this pull request Oct 14, 2025

[Merged by Bors] - feat(Analysis/Distribution): Multiplication of two functions of temperate growth is of temperate growth #30176

Closed

1 task

less variables and opens

5dc3ce5

mcdoll changed the title ~~chore(Analysis/Distribution): split of functions and measures of temperate growth~~ chore(Analysis/Distribution): split off functions and measures of temperate growth Oct 14, 2025

ADedecker reviewed Oct 19, 2025

View reviewed changes

Update Mathlib/Analysis/Distribution/TemperateGrowth.lean

cf4bb8f

Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>

leanprover-community-bot-assistant assigned j-loreaux Oct 23, 2025

ADedecker approved these changes Oct 28, 2025

View reviewed changes

ADedecker added the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 28, 2025

mcdoll and others added 4 commits October 28, 2025 22:03

Update Mathlib/Analysis/Distribution/TemperateGrowth.lean

6f1edb4

Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>

Update Mathlib/Analysis/Distribution/TemperateGrowth.lean

38dad23

Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>

Update Mathlib/Analysis/Distribution/TemperateGrowth.lean

7c8bf0d

Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>

Update Mathlib/Analysis/Distribution/TemperateGrowth.lean

bcc2bac

Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>

mcdoll commented Oct 28, 2025

View reviewed changes

Mathlib/Analysis/Distribution/TemperateGrowth.lean Outdated Show resolved Hide resolved

Update Mathlib/Analysis/Distribution/TemperateGrowth.lean

51cc5e8

mcdoll removed the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 28, 2025

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Oct 28, 2025

Merge branch 'master' into split_temperate

4b6272b

mathlib-bors bot changed the title ~~chore(Analysis/Distribution): split off functions and measures of temperate growth~~ [Merged by Bors] - chore(Analysis/Distribution): split off functions and measures of temperate growth Oct 29, 2025

mathlib-bors bot closed this Oct 29, 2025

Conversation

mcdoll commented Oct 14, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Oct 14, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary e29df49f46

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

ADedecker Oct 19, 2025

Choose a reason for hiding this comment

Uh oh!

mcdoll Oct 19, 2025

Choose a reason for hiding this comment

Uh oh!

ADedecker left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mcdoll left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

ADedecker commented Oct 28, 2025

Uh oh!

mathlib-bors bot commented Oct 28, 2025

Uh oh!

mcdoll commented Oct 29, 2025

Uh oh!

mathlib-bors bot commented Oct 29, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

mcdoll commented Oct 14, 2025 •

edited

Loading

github-actions bot commented Oct 14, 2025 •

edited

Loading