feat(Analysis/Distribution): tempered distributions #29819

mcdoll · 2025-09-19T18:09:00Z

This is mainly a tracking PR: Most features will be PR'd separately.

With the exception of the file FourierMultiplier now everything is in a PR.

depends on: [Merged by Bors] - chore(Analysis/Distribution/SchwartzMap): correct a definition and add two lemmas #29818
depends on: [Merged by Bors] - chore(Data/Nat/Choose): add le-version of a bound and fix name of the lt-version #29821
depends on: [Merged by Bors] - feat(SchwartzSpace): integration by parts in 1d #29846
depends on: [Merged by Bors] - feat(Analysis/Fourier): Plancherel's theorem #29860
depends on: [Merged by Bors] - feat: the Hölder conjugate of an ENNReal #30174
depends on: [Merged by Bors] - feat(Analysis/Distribution): a smooth function with compact support is a Schwartz function #30175
depends on: [Merged by Bors] - feat(Analysis/Distribution): Multiplication of two functions of temperate growth is of temperate growth #30176
depends on: [Merged by Bors] - feat(Analysis/Calculus): add a version of bounding iterated derivatives of compositions with fewer assumptions on differentiability #30180
depends on: feat(Topology): scalar multiplication as a CLM #30195
depends on: [Merged by Bors] - chore(Analysis/Distribution/TemperateGrowth): avoid redefining variables #31075
depends on: [Merged by Bors] - feat(Analysis/Normed): extend densely defined LinearMaps to CLM #31074
depends on: [Merged by Bors] - chore(Analysis/Normed/Operator): move extension to a new file #29888
depends on: [Merged by Bors] - chore(Analysis/Distribution): fix name of a theorem #31073
depends on: [Merged by Bors] - feat(Analysis/Fourier): the Fourier transform on L^2 #29948
depends on: [Merged by Bors] - feat(Analysis/Normed): extension to linear isometry equivalence #31076
depends on: [Merged by Bors] - feat(Analysis/ContDiff): smooth compactly supported functions are dense in Lp #31079
depends on: [Merged by Bors] - feat(Analysis/Distribution): basic algebraic properties of functions of temperate growth #31112
depends on: [Merged by Bors] - feat(Analysis/Fourier): introduce notation type class for the Fourier transform #31115
depends on: [Merged by Bors] - feat(Analysis): use new notation for Fourier transform on Schwartz functions and simplify presentation #31114
depends on: [Merged by Bors] - feat(Topology/Algebra): topology of pointwise convergence for continuous linear maps #11496
depends on: [Merged by Bors] - feat(Analysis/InnerProductSpace): fderiv of norm squared #31085
depends on: [Merged by Bors] - feat(Analysis): the topology of pointwise convergence is locally convex #31577
depends on: [Merged by Bors] - feat(Topology/Algebra): the equivalence of continuous linear maps and UniformConvergenceCLM #31756
depends on: [Merged by Bors] - feat(Analysis/Distribution): definition of tempered distributions #31757
depends on: [Merged by Bors] - feat(Topology/Algebra): generalize precomp and postcomp to UniformConvergenceCLM #31760
depends on: [Merged by Bors] - feat(Analysis/Distribution): composition of temperate growth functions #32297
depends on: [Merged by Bors] - feat(Analysis/Distribution): notation for lineDeriv #32084
depends on: [Merged by Bors] - feat(Analysis/Distribution): integration by parts for Schwartz functions #31876
depends on: [Merged by Bors] - feat(Analysis/Distribution): the bilinear pairing of Schwartz functions #32411
depends on: [Merged by Bors] - feat(Analysis/Distribution): (1 + |x| ^ 2) ^ r has temperate growth #32307
depends on: [Merged by Bors] - feat(Analysis/TemperedDistribution): embedding of temperate growth functions #32766
depends on: [Merged by Bors] - feat(Analysis/TemperedDistribution): embedding of Lp-functions #32767
depends on: [Merged by Bors] - feat(Analysis/TemperedDistribution): embedding of Schwartz functions #32768
depends on: [Merged by Bors] - feat(Analysis/TemperedDistribution): multiplication with temperate growth functions #32769
depends on: [Merged by Bors] - feat(Analysis/TemperedDistribution): derivatives #32770
depends on: [Merged by Bors] - feat(Analysis/Fourier): Fourier transform of the convolution #32992
depends on: [Merged by Bors] - feat(Analysis/TemperedDistribution): the embedding of Lp and SchwartzMap give the same tempered distribution #33229
depends on: [Merged by Bors] - feat(Analysis/TemperedDistribution): Fourier transform of the dirac delta #33230
depends on: [Merged by Bors] - feat(Analysis/TemperedDistribution): the Fourier transform on tempered distributions extends the FT on Schwartz space #33232
depends on: [Merged by Bors] - feat(Analysis/Fourier): L2 and TemperedDistribution Fourier transforms coincide #33242

github-actions · 2025-09-19T18:10:13Z

PR summary e02195e618

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Analysis.Distribution.TemperedDistribution` (new file)	2548

Declarations diff

+ MeasureTheory.Measure.toTemperedDistribution
+ MeasureTheory.Measure.toTemperedDistribution_apply
+ TemperedDistribution
+ TemperedDistribution.pderivCLM
+ _root_.ContinuousLinearMap.smul
+ _root_.ContinuousLinearMap.smulCLM_apply
+ _root_.Function.HasTemperateGrowth.mul
+ bilinLeftCLM
+ bilinLeftCLM_apply_apply
+ delta'
+ delta'_apply
+ derivCLM
+ derivCLM_apply_apply
+ derivCLM_toTemperedDistributionCLM_eq
+ foo
+ fourierTransform
+ fourierTransformCLM
+ fourierTransformCLM_apply_apply
+ fourierTransformCLM_toTemperedDistributionCLM_eq
+ fourierTransformInv
+ fourierTransformInv_apply
+ fourierTransform_apply
+ hasDerivAt
+ hasTemperateGrowth
+ integral_bilin_fourierIntegral_eq_flip
+ integral_bilinear_deriv_right_eq_neg_left
+ integral_clm_comp_deriv_right_eq_neg_left
+ memLp_of_bilin
+ mkCompCLM
+ mkCompCLM_apply_apply
+ mkCompCLM_comp
+ mkCompCLM_id
+ mulLeftCLM
+ neg_apply
+ pairingCLM
+ pairingLM
+ pairingLM_apply
+ pairingLM_apply_apply
+ pderivCLM_apply
+ smulLeftCLM_const
+ smulLeftCLM_mul
+ smulLeftCLM_toTemperedDistributionCLM_eq
+ toTemperedDistributionCLM_apply
+ toTemperedDistributionCLM_apply_apply
+ toTemperedDistribution_aux
++ smulLeftCLM
++ smulLeftCLM_apply_apply
++ toTemperedDistribution
++ toTemperedDistributionCLM
++ toTemperedDistribution_apply
+-+ mkCLM

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 · 2026-01-06T22:24:32Z

This PR/issue depends on:

~~[Merged by Bors] - chore(Analysis/Distribution/SchwartzMap): correct a definition and add two lemmas #29818~~
~~[Merged by Bors] - chore(Data/Nat/Choose): add le-version of a bound and fix name of the lt-version #29821~~
~~[Merged by Bors] - feat(SchwartzSpace): integration by parts in 1d #29846~~
~~[Merged by Bors] - feat(Analysis/Fourier): Plancherel's theorem #29860~~
~~[Merged by Bors] - feat: the Hölder conjugate of an ENNReal #30174~~
~~[Merged by Bors] - feat(Analysis/Distribution): a smooth function with compact support is a Schwartz function #30175~~
~~[Merged by Bors] - feat(Analysis/Distribution): Multiplication of two functions of temperate growth is of temperate growth #30176~~
~~[Merged by Bors] - feat(Analysis/Calculus): add a version of bounding iterated derivatives of compositions with fewer assumptions on differentiability #30180~~
~~feat(Topology): scalar multiplication as a CLM #30195~~
~~[Merged by Bors] - chore(Analysis/Distribution/TemperateGrowth): avoid redefining variables #31075~~
~~[Merged by Bors] - feat(Analysis/Normed): extend densely defined LinearMaps to CLM #31074~~
~~[Merged by Bors] - chore(Analysis/Normed/Operator): move extension to a new file #29888~~
~~[Merged by Bors] - chore(Analysis/Distribution): fix name of a theorem #31073~~
~~[Merged by Bors] - feat(Analysis/Fourier): the Fourier transform on L^2 #29948~~
~~[Merged by Bors] - feat(Analysis/Normed): extension to linear isometry equivalence #31076~~
~~[Merged by Bors] - feat(Analysis/ContDiff): smooth compactly supported functions are dense in Lp #31079~~
~~[Merged by Bors] - feat(Analysis/Distribution): basic algebraic properties of functions of temperate growth #31112~~
~~[Merged by Bors] - feat(Analysis/Fourier): introduce notation type class for the Fourier transform #31115~~
~~[Merged by Bors] - feat(Analysis): use new notation for Fourier transform on Schwartz functions and simplify presentation #31114~~
~~[Merged by Bors] - feat(Topology/Algebra): topology of pointwise convergence for continuous linear maps #11496~~
~~[Merged by Bors] - feat(Analysis/InnerProductSpace): fderiv of norm squared #31085~~
~~[Merged by Bors] - feat(Analysis): the topology of pointwise convergence is locally convex #31577~~
~~[Merged by Bors] - feat(Topology/Algebra): the equivalence of continuous linear maps and UniformConvergenceCLM #31756~~
~~[Merged by Bors] - feat(Analysis/Distribution): definition of tempered distributions #31757~~
~~[Merged by Bors] - feat(Topology/Algebra): generalize precomp and postcomp to UniformConvergenceCLM #31760~~
~~[Merged by Bors] - feat(Analysis/Distribution): composition of temperate growth functions #32297~~
~~[Merged by Bors] - feat(Analysis/Distribution): notation for lineDeriv #32084~~
~~[Merged by Bors] - feat(Analysis/Distribution): integration by parts for Schwartz functions #31876~~
~~[Merged by Bors] - feat(Analysis/Distribution): the bilinear pairing of Schwartz functions #32411~~
~~[Merged by Bors] - feat(Analysis/Distribution): (1 + |x| ^ 2) ^ r has temperate growth #32307~~
~~[Merged by Bors] - feat(Analysis/TemperedDistribution): embedding of temperate growth functions #32766~~
~~[Merged by Bors] - feat(Analysis/TemperedDistribution): embedding of Lp-functions #32767~~
~~[Merged by Bors] - feat(Analysis/TemperedDistribution): embedding of Schwartz functions #32768~~
~~[Merged by Bors] - feat(Analysis/TemperedDistribution): multiplication with temperate growth functions #32769~~
~~[Merged by Bors] - feat(Analysis/TemperedDistribution): derivatives #32770~~
~~[Merged by Bors] - feat(Analysis/Fourier): Fourier transform of the convolution #32992~~
~~[Merged by Bors] - feat(Analysis/TemperedDistribution): the embedding of Lp and SchwartzMap give the same tempered distribution #33229~~
~~[Merged by Bors] - feat(Analysis/TemperedDistribution): Fourier transform of the dirac delta #33230~~
~~[Merged by Bors] - feat(Analysis/TemperedDistribution): the Fourier transform on tempered distributions extends the FT on Schwartz space #33232~~
~~[Merged by Bors] - feat(Analysis/Fourier): L2 and TemperedDistribution Fourier transforms coincide #33242~~
By Dependent Issues (🤖). Happy coding!

mcdoll · 2026-01-07T20:06:22Z

Closing since all of the remaining parts are in the PR #33329

mcdoll added 2 commits September 19, 2025 20:02

corrections

93509b8

tempered distros

e223eee

mcdoll added the WIP Work in progress label Sep 19, 2025

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

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Sep 19, 2025

mcdoll added 24 commits September 20, 2025 13:57

fourier trafo

fbe6025

basic lemma

98adc32

stuff

81d6075

semilinearize

c79551b

revert accidental deletion

accbdba

part 2

11044f2

Merge branch 'semilinearize_int' into semilinearize_int2

24f0880

more

f57d16a

merged

6324c8e

Parseval for VectorFourier

1cf7f89

finished proof

c03d17a

added Parseval for inner f.toLp f.top

f415bde

initial commit

46a13b7

merged

ad41c7b

doc strings

65b6c40

mk_all

804b48d

update doc

9372cc3

renaming and generalization

7300090

relax assumptions f and g

03d9d49

Merge branch 'master' into parseval

9d2468e

fix

2349092

deduplication

ba371c9

renaming

aabfd52

renaming 2

d37c8cf

mcdoll added 21 commits October 3, 2025 10:04

prettier

106ca65

merged

3411bb4

fixes

3fb3e7c

merged

ca15435

things

7063b94

definition of Sobolev functions

4d4d248

density in Lp

ab8752f

add, norm_sq for temperate growth

b3baf8e

use junk values

758e6cb

add notation for FT and Laplacian

2b1d32d

almost there

ed34634

done

cf81e72

fixed names

331b0f8

really done

b8e7a38

fix build

c2eafa1

notation file

5970df0

wrong file

a364736

coercions

1c433db

copyright

c4cae4c

style

483bff3

golf proof

cfde5cf

grunweg changed the title ~~feat(Analysis/Distribution): Tempered distributions~~ feat(Analysis/Distribution): tempered distributions Oct 31, 2025

mcdoll added 4 commits November 10, 2025 11:59

added strong operator topology

61f9d19

fixes

82afbaf

new files

f50ad06

minor fixes

0cfa8e0

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 6, 2026

mcdoll closed this Jan 7, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

feat(Analysis/Distribution): tempered distributions #29819

feat(Analysis/Distribution): tempered distributions #29819

Uh oh!

mcdoll commented Sep 19, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Sep 19, 2025 •

edited

Loading

Declarations diff

Uh oh!

mathlib4-dependent-issues-bot commented Jan 6, 2026

Uh oh!

mcdoll commented Jan 7, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

feat(Analysis/Distribution): tempered distributions #29819

feat(Analysis/Distribution): tempered distributions #29819

Uh oh!

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

PR summary e02195e618

Import changes for modified files

Declarations diff

Uh oh!

mathlib4-dependent-issues-bot commented Jan 6, 2026

Uh oh!

mcdoll commented Jan 7, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

mcdoll commented Sep 19, 2025 •

edited

Loading

github-actions bot commented Sep 19, 2025 •

edited

Loading