-
Notifications
You must be signed in to change notification settings - Fork 1k
chore(Analysis/Distribution): split off derivatives from SchwartzSpace and create new folder
#34027
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
base: master
Are you sure you want to change the base?
Conversation
PR summary ca7d6f198f
|
| Files | Import difference |
|---|---|
Mathlib.Analysis.Distribution.FourierSchwartz |
-2653 |
Mathlib.Analysis.Distribution.SchwartzSpace |
-2558 |
24 filesMathlib.Analysis.Distribution.TemperedDistribution Mathlib.Analysis.Fourier.Convolution Mathlib.Analysis.Fourier.LpSpace 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.EisensteinSeries.E2.Defs Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable 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 |
1 |
Mathlib.Analysis.Distribution.SchwartzSpace.Basic |
2533 |
Mathlib.Analysis.Distribution.SchwartzSpace.Deriv (new file) |
2559 |
Mathlib.Analysis.Distribution.SchwartzSpace.Fourier |
2654 |
Declarations diff
No declarations were harmed in the making of this PR! 🐙
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.
Decrease in tech debt: (relative, absolute) = (1.00, 0.25)
| Current number | Change | Type |
|---|---|---|
| 4 | -1 | large files |
Current commit f75143afb9
Reference commit ca7d6f198f
You can run this locally as
./scripts/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).
note: file Mathlib/Analysis/Distribution/FourierSchwartz.lean` was renamed to `Mathlib/Analysis/Distribution/SchwartzSpace/Fourier.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!
note: file Mathlib/Analysis/Distribution/SchwartzSpace.lean` was renamed to `Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!
This reverts commit a719f64.
|
This pull request has conflicts, please merge |
Since
Analysis/Distribution/SchwartzSpace.leanis over 1500 lines, we have to move some of its contents into a new file.The derivatives are a natural choice, because it is quite a few lines of code, will see further expansion (with the Laplacian) and a number of imports are just needed for them.
We perform this split by moving the current file to
Analysis/Distribution/SchwartzSpace/Basic.leanand creating a new fileAnalysis/Distribution/SchwartzSpace.Deriv.lean. Moreover, we move the previousAnalysis/Distribution/FourierSchwartz.leantoAnalysis/Distribution/SchwartzSpace/Fourier.lean