English
If g is a measurable embedding and f: β → ℝ≥0∞ is arbitrary, then ∫ f d(map g μ) = ∫ (f ∘ g) dμ; i.e., the lintegral respects a measurable embedding and pullback of the measure.
Русский
Если g — измеримое вложение и f: β → ℝ≥0∞ произвольна, то ∫ f d(map g μ) = ∫ f(g(a)) dμ; то есть линегральный интеграл сохраняется при отображении и вытаскивании меры.
LaTeX
$$$$ \\int f(a) \\, d(\\mathrm{map}\, g\, \\mu) = \\int f(g(a)) \\, d\\mu. $$$$
Lean4
/-- If `g : α → β` is a measurable embedding and `f : β → ℝ≥0∞` is any function (not necessarily
measurable), then `∫⁻ a, f a ∂(map g μ) = ∫⁻ a, f (g a) ∂μ`. Compare with `lintegral_map` which
applies to any measurable `g : α → β` but requires that `f` is measurable as well. -/
theorem _root_.MeasurableEmbedding.lintegral_map {g : α → β} (hg : MeasurableEmbedding g) (f : β → ℝ≥0∞) :
∫⁻ a, f a ∂map g μ = ∫⁻ a, f (g a) ∂μ := by
rw [lintegral, lintegral]
refine le_antisymm (iSup₂_le fun f₀ hf₀ => ?_) (iSup₂_le fun f₀ hf₀ => ?_)
· rw [SimpleFunc.lintegral_map _ hg.measurable]
have : (f₀.comp g hg.measurable : α → ℝ≥0∞) ≤ f ∘ g := fun x => hf₀ (g x)
exact le_iSup_of_le (comp f₀ g hg.measurable) (by exact le_iSup (α := ℝ≥0∞) _ this)
· rw [← f₀.extend_comp_eq hg (const _ 0), ← SimpleFunc.lintegral_map, ← SimpleFunc.lintegral_eq_lintegral, ←
lintegral]
refine lintegral_mono_ae (hg.ae_map_iff.2 <| Eventually.of_forall fun x => ?_)
exact (extend_apply _ _ _ _).trans_le (hf₀ _)
