English
For a MeasurableEquiv f, the pushforward of gaussianReal μ v by f.symm has density |f'| times gaussianPDFReal μ v (f x).
Русский
Для измеримого эквивалента f.symm распределение гаусса имеет плотность, равную |f'|⋅gaussianPDFReal(μ,v)(f(x)).
LaTeX
$$$(\mathrm{gaussianReal}(\mu, v)).map f.symm(s) = \mathrm{ENNReal.ofReal}\left(\int_{x \in s} |f'(x)| \mathrm{gaussianPDFReal}(\mu, v, f(x)) \, dx\right)$$$
Lean4
theorem _root_.MeasurableEquiv.gaussianReal_map_symm_apply (hv : v ≠ 0) (f : ℝ ≃ᵐ ℝ) {f' : ℝ → ℝ}
(h_deriv : ∀ x, HasDerivAt f (f' x) x) {s : Set ℝ} (hs : MeasurableSet s) :
(gaussianReal μ v).map f.symm s = ENNReal.ofReal (∫ x in s, |f' x| * gaussianPDFReal μ v (f x)) :=
by
rw [gaussianReal_of_var_ne_zero _ hv, gaussianPDF_def]
exact
f.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul' hs h_deriv (ae_of_all _ (gaussianPDFReal_nonneg _ _))
(integrable_gaussianPDFReal _ _)
