feat(Analysis/Distribution): compactly supported functions have temperate growth (leanprover-community#34606)

---

Note this follows also from the fact that Schwartz functions have temperate growth, but I think a direct proof is nicer.


<!-- Your PR title will become the first line of the commit message.

In this box, the text above the `---` (if not empty) will be appended
to the commit message, and can be used to give additional context or
details. Please leave a blank newline before the `---`, otherwise GitHub
will format the text above it as a title.

For details on the "pull request lifecycle" in mathlib, please see:
https://leanprover-community.github.io/contribute/index.html

In particular, note that most reviewers will only notice your PR
if it passes the continuous integration checks.
Please ask for help on https://leanprover.zulipchat.com if needed.

When merging, all the commits will be squashed into a single commit
listing all co-authors.

Co-authors in the squash commit are gathered from two sources:

First, all authors of commits to this PR branch are included. Thus,
one way to add co-authors is to include at least one commit authored by
each co-author among the commits in the pull request. If necessary, you
may create empty commits to indicate co-authorship, using commands like so:

git commit --author="Author Name <author@email.com>" --allow-empty -m "add Author Name as coauthor"

Second, co-authors can also be listed in lines at the very bottom of
the commit message (that is, directly before the `---`) using the following format:


If you are moving or deleting declarations, please include these lines
at the bottom of the commit message (before the `---`, and also before
any "Co-authored-by" lines) using the following format:

Moves:
- Vector.* -> List.Vector.*
- ...

Deletions:
- Nat.bit1_add_bit1
- ...

Any other comments you want to keep out of the PR commit should go
below the `---`, and placed outside this HTML comment, or else they
will be invisible to reviewers.

If this PR depends on other PRs, please list them below this comment,
using the following format:
- [ ] depends on: #abc [optional extra text]
- [ ] depends on: #xyz [optional extra text]

-->

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

Co-authored-by: Author Name <author@email.com>

Author: mcdoll

Mathlib/Analysis/Distribution/TemperateGrowth.lean

@@ -115,6 +115,16 @@ lemma HasTemperateGrowth.const (c : F) :
     Function.HasTemperateGrowth (fun _ : E ↦ c) :=
   .of_fderiv (by simpa using .zero) (differentiable_const c) (k := 0) (C := ‖c‖) (fun x ↦ by simp)
 
+@[fun_prop]
+lemma _root_.HasCompactSupport.hasTemperateGrowth {f : E → F} (h₁ : HasCompactSupport f)
+    (h₂ : ContDiff ℝ ∞ f) : f.HasTemperateGrowth := by
+  refine ⟨h₂, fun n ↦ ?_⟩
+  set g := fun x ↦ ‖iteratedFDeriv ℝ n f x‖
+  have hg : Continuous g := (h₂.continuous_iteratedFDeriv <| mod_cast le_top).norm
+  obtain ⟨x₀, hx₀⟩ := hg.exists_forall_ge_of_hasCompactSupport ((h₁.iteratedFDeriv _).norm)
+  refine ⟨0, g x₀, fun x ↦ ?_⟩
+  simpa using hx₀ x
+
 /-- Composition of two temperate growth functions is of temperate growth.
 
 Version where the outer function `g` is only of temperate growth on the image of inner function