English
If there is a measurable map m' : α → β that aligns f and g via f(a) = g(m'(a)) for all a, and pushing forward μ' through m' matches μ on preimages, then f.lintegral μ = g.lintegral μ'.
Русский
Если существует измеримое отображение m' : α → β, такое что f(a) = g(m'(a)) для всех a, и μ'^{-1} мe(D) согласуется через m' с μ на предобразах, то f.lintegral μ = g.lintegral μ'.
LaTeX
$$$(\\forall a, f(a) = g(m'(a))) \\land (\\forall s, MeasurableSet s → μ'(s) = μ(m'^{-1}(s))) → f.lintegral μ = g.lintegral μ'$$$
Lean4
theorem lintegral_map' {β} [MeasurableSpace β] {μ' : Measure β} (f : α →ₛ ℝ≥0∞) (g : β →ₛ ℝ≥0∞) (m' : α → β)
(eq : ∀ a, f a = g (m' a)) (h : ∀ s, MeasurableSet s → μ' s = μ (m' ⁻¹' s)) : f.lintegral μ = g.lintegral μ' :=
lintegral_eq_of_measure_preimage fun y => by
simp only [preimage, eq]
exact (h (g ⁻¹' { y }) (g.measurableSet_preimage _)).symm
