feat(Analysis/Distribution): compactly supported functions are dense in Schwartz space

[teorth]

This file adds SchwartzMap.dense_hasCompactSupport: the compactly supported
Schwartz functions are dense in 𝓢(E, F) (for E a finite-dimensional real
normed space).

The proof goes through smooth truncation, and some API for such truncations is provided.

---

This material will be used in a forthcoming PR on the prime number theorem.

AI was used to generate initial code, which was then heavily golfed and reviewed by the author.

[github-actions]

PR summary 3fc2a2622d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Analysis.Distribution.SchwartzSpace.CompactSupport (new file)	2875

---

Declarations diff (regex)

+ bumpR
+ bumpR_eq_one
+ bumpR_le_one
+ bumpR_nonneg
+ bumpχ
+ contDiff_bumpR
+ dense_hasCompactSupport
+ exists_bound_iteratedFDeriv_χ₀
+ hasCompactSupport_bumpR
+ hasCompactSupport_truncate
+ hasCompactSupport_χ₀
+ hasTemperateGrowth_bumpR
+ iteratedFDeriv_bumpR_eq_zero
+ norm_iteratedFDeriv_bumpR_le
+ support_bumpR
+ support_χ₀
+ tendsto_seminorm_truncate_sub
+ tendsto_truncate
+ truncate
+ truncate_apply
+ χ₀

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- unavailable)

⚠️ No declarations diff yet: there is no built master snapshot at this PR's merge-base (typically a bors-batch intermediate that CI never built). Merge master into this PR and push to refresh.

---

No changes to strong technical debt.

Increase in weak tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type (weak)
4949	1	exposed public sections

Current commit 3fc2a2622d
Reference commit d0809a79a4

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/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).