English
For AEMeasurable f on join m, the lintegral with respect to join m equals the double lintegral.
Русский
Для AEMeasurable f на join m интеграл линтеграла равен двойному линтеинтегралу.
LaTeX
$$$\\text{lintegral }_{{\\!join m}} f = \\text{lintegral }_{{m}} (\\lambda μ. \\text{lintegral }_{{μ}} f).$$$
Lean4
theorem lintegral_join {m : Measure (Measure α)} {f : α → ℝ≥0∞} (hf : AEMeasurable f (join m)) :
∫⁻ x, f x ∂join m = ∫⁻ μ, ∫⁻ x, f x ∂μ ∂m :=
by
wlog hfm : Measurable f generalizing f
· rcases hf with ⟨g, hgm, hfg⟩
rw [lintegral_congr_ae hfg, this hgm.aemeasurable hgm]
exact lintegral_congr_ae <| (ae_ae_of_ae_join hfg).mono fun μ hμ ↦ .symm <| lintegral_congr_ae hμ
simp_rw [lintegral_eq_iSup_eapprox_lintegral hfm, SimpleFunc.lintegral,
join_apply (SimpleFunc.measurableSet_preimage _ _)]
clear hf
suffices
∀ (s : ℕ → Finset ℝ≥0∞) (f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞),
(∀ n r, Measurable (f n r)) →
Monotone (fun n μ => ∑ r ∈ s n, r * f n r μ) →
⨆ n, ∑ r ∈ s n, r * ∫⁻ μ, f n r μ ∂m = ∫⁻ μ, ⨆ n, ∑ r ∈ s n, r * f n r μ ∂m
by
refine
this (fun n => SimpleFunc.range (SimpleFunc.eapprox f n)) (fun n r μ => μ (SimpleFunc.eapprox f n ⁻¹' { r })) ?_
?_
· exact fun n r => measurable_coe (SimpleFunc.measurableSet_preimage _ _)
· exact fun n m h μ => SimpleFunc.lintegral_mono (SimpleFunc.monotone_eapprox _ h) le_rfl
intro s f hf hm
rw [lintegral_iSup _ hm]
swap
· fun_prop
congr
funext n
rw [lintegral_finset_sum (s n)]
· simp_rw [lintegral_const_mul _ (hf _ _)]
· exact fun r _ => (hf _ _).const_mul _
