[Merged by Bors] - feat(Analysis/Distribution): (1 + |x| ^ 2) ^ r has temperate growth

[mcdoll]

The function (1 + |x| ^ 2) ^ r, also known as the Bessel potential, has temperate growth. This is a crucial ingredient to define Sobolev spaces via the Fourier transform, since only multiplication with temperate growth function maps Schwartz functions to Schwartz functions (hence tempered distributions to itself).

We also add to_fun attributes to various declarations because fun_prop did not solve 1 + |x|^2 without fun_add.

---

• depends on: [Merged by Bors] - feat(Analysis/Distribution): composition of temperate growth functions #32297

[github-actions]

PR summary 89111f4099

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.Distribution.TemperateGrowth	2267	2269	+2 (+0.09%)

Import changes for all files

Files

Import difference

22 files Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.Analysis.Distribution.SchwartzSpace Mathlib.Analysis.Distribution.TemperateGrowth 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.QExpansion Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

2

---

Declarations diff

+ hasTemperateGrowth_one_add_norm_sq_rpow

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

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(Analysis/Distribution): composition of temperate growth functions #32297
  By Dependent Issues (🤖). Happy coding!

[j-loreaux]

This proof is pretty long, so it's hard to follow from the source code alone. Can you please add some comments sketching the idea for the reader?

[mcdoll]

Thanks that is a very good point. I've added some comments.
Also if we add a predicate HasTemperateGrowthOn then a big part of the proof should be factored out.

[j-loreaux]

Thanks! That's significantly more readable.

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Post-Build Step
• Build