[Merged by Bors] - chore(Analysis/Distribution): move the SchwartzSpace file to a new folder Distribution

[sgouezel]

---

[ADedecker]

maintainer merge
Are you doing this for a particular reason? I'm currently digging up my drafts on (usual) distributions to actually PR them to mathlib, so I hope there's no collision in sight 😅

[github-actions]

🚀 Pull request has been placed on the maintainer queue by ADedecker.

[sgouezel]

I need the fact that, if a locally integrable function has vanishing integral against all smooth compactly supported functions, then it is zero almost everywhere (towards Rademacher theorem on ae differentiability of Lipschitz functions). The natural place for the file would be in a distribution folder although this statement does not need the definition of distributions (and hopefully wouldn't overlap with what you are doing).

[ADedecker]

No overlap indeed, and I'll be glad if the result is already there when I need it, so that's perfect!

[ocfnash]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style