feat(Analysis.SpecialFunctions.Gaussian): add integrable_fun_mul_exp_neg_mul_sq

[slerpyyy]

If f : ℝ → ℝ is bounded by a polynomial, fun x : ℝ => f x * exp (-b * x ^ 2) is integrable.

---

[slerpyyy]

Currently, the condition that f is bounded by a polynomial is expressed as follows.

(hfs : f =O[atTop] fun x : ℝ => x ^ s) (hfs' : (fun x => f (-x)) =O[atTop] fun x : ℝ => x ^ s)

Is there a better way to state this?

[urkud]

You can generalize this from $e^{-ax^2/2}$ to any function satisfying Asymptotics.SuperpolynomialDecay. In fact, your statement is a combination of three facts:

• if f has at most polynomial growth and g has a superpolynomial decay, then f * g has a superpolynomial decay;
• a strongly measurable function with superpolynomial decay is integrable;
• $e^{-ax^2/2}$ has superpolynomial decay.

As for ±∞, you can use either of

• a condition with atTop and a condition with atBot;
• a condition with cobounded of cocompact; this is especially useful if you're going to generalize your theorem to a finite dimensional vector space with a Haar measure;
• in the future, someone may need a stronger version with (one of the filters above) ⊓ volume.ae; this is useful if f is a coercion of an element of Lp or AEEqFun.

One more comment: a version with f : Real -> E and scalar multiplication is useful too.

[ocfnash]

@slerpyyy I'm relabeling this as "awaiting-author" as I presume you are working on Yury's suggestions. If not, please relabel back and feel free to ping for review in "PR reviews" on Zulip.