English
If f is AEMeasurable with respect to map g μ and g is AEMeasurable with respect to μ, then ∫ f d(map g μ) = ∫ f(g) dμ, i.e., the equality holds after replacing f by an a.e. version and using composition.
Русский
Если f является AEMeasurable относительно map g μ и g является AEMeasurable относительно μ, то ∫ f d(map g μ) = ∫ f(g) dμ, т.е. тождество сохраняется после замены f на эквивалентную по АЕ версию и использования композиции.
LaTeX
$$$$ \int f\, d(map\ g\ μ) = \int f(g)\, dμ, \quad \text{при } \ hf :\text{AEMeasurable } f\ (map\ g\ μ), \ hg : \text{AEMeasurable } g\ μ.$$$$
Lean4
theorem lintegral_map' {f : β → ℝ≥0∞} {g : α → β} (hf : AEMeasurable f (Measure.map g μ)) (hg : AEMeasurable g μ) :
∫⁻ a, f a ∂Measure.map g μ = ∫⁻ a, f (g a) ∂μ :=
calc
∫⁻ a, f a ∂Measure.map g μ = ∫⁻ a, hf.mk f a ∂Measure.map g μ := lintegral_congr_ae hf.ae_eq_mk
_ = ∫⁻ a, hf.mk f a ∂Measure.map (hg.mk g) μ := by
congr 1
exact Measure.map_congr hg.ae_eq_mk
_ = ∫⁻ a, hf.mk f (hg.mk g a) ∂μ := (lintegral_map hf.measurable_mk hg.measurable_mk)
_ = ∫⁻ a, hf.mk f (g a) ∂μ := (lintegral_congr_ae <| hg.ae_eq_mk.symm.fun_comp _)
_ = ∫⁻ a, f (g a) ∂μ := lintegral_congr_ae (ae_eq_comp hg hf.ae_eq_mk.symm)
