Commit 2025-12-19 11:20 e9f2f256

feat: gaussianReal_const_sub (#31551)

• Add lemmas stating that if X is a real Gaussian random variable with mean μ and variance v, then -X, X - y and y - X are Gaussian with variance v and respective means -μ, μ - y and y - μ.
• Generalize this section of the file from MeasureSpace to MeasurableSpace+Measure