Gaussian Integration by Parts (Stein's Lemma) - 1D + Hilbert

Stream: maths

[Matteo Cipollina]

Hi all, I've put together a formalization of Gaussian Integration by Parts (Stein's Lemma), and I'd be happy to start PR'ing it if people think it would be a useful addition in this form.

https://github.com/or4nge19/mathlib4/blob/GIBP/Mathlib/Probability/Distributions/GaussianIntegrationByParts.lean

https://github.com/or4nge19/mathlib4/blob/GIBP/Mathlib/Probability/Distributions/GIBP_HilbertFin.lean

The formalization covers so far:

1. The 1D case: For a centered Gaussian X ~ N(0, v), it proves 𝔼[X * F(X)] = v * 𝔼[F'(X)] via exponential tilt and differentiation under the integral sign, for which I've tried to setup some sharp, uniform bounds for the difference quotient, considering that the immediate need for this is the attempt to formalize prerequisites to formalise results in Talagrand "Mean Field models for Spin Glasses" for which these bounds I believe should be enough .
2. A finite-dimensional Hilbert space version: For a centered Gaussian g on H with covariance operator Σ, it proves the covariant form 𝔼[⟪g, h⟫ F(g)] = 𝔼[(fderiv ℝ F g) (Σ h)] by decomposing along an orthonormal basis and applying the 1D result conditionally using Fubini's theorem.

To make the main lemmas cleaner, and following/adapting from Talagrand, I've introduced a HasModerateGrowth predicate to bundle the polynomial growth conditions on the test function F and its derivative.

Any feedback on the plan, the code, design choice or abstractions introduced would be very welcome :)