English
Under a differentiable change of variables f with derivative f', the pullback of gaussianReal μ v by f is ENNReal.ofReal of the integral of |f'| times gaussianPDFReal μ v (f x).
Русский
При замене переменной через отображение f с производной f', тянущее обратно гауссову меру, равно ENNReal.ofReal интегралу по s от |f'|⋅gaussianPDFReal μ v (f x).
LaTeX
$$$\mathrm{gaussianReal}(\mu, v)_{\comap f}(s) = \mathrm{ENNReal.ofReal}\left(\int_{x \in s} |f'(x)| \mathrm{gaussianPDFReal}(\mu, v, f(x)) \, dx\right)$$$
Lean4
theorem _root_.MeasurableEmbedding.gaussianReal_comap_apply (hv : v ≠ 0) {f : ℝ → ℝ} (hf : MeasurableEmbedding f)
{f' : ℝ → ℝ} (h_deriv : ∀ x, HasDerivAt f (f' x) x) {s : Set ℝ} (hs : MeasurableSet s) :
(gaussianReal μ v).comap f s = ENNReal.ofReal (∫ x in s, |f' x| * gaussianPDFReal μ v (f x)) :=
by
rw [gaussianReal_of_var_ne_zero _ hv, gaussianPDF_def]
exact
hf.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul' hs h_deriv (ae_of_all _ (gaussianPDFReal_nonneg _ _))
(integrable_gaussianPDFReal _ _)
