English
If f,g are a.e.-measurable, then the double lintegral of f x g y equals the product of their lintegrals: ∫⁻ x ∫⁻ y f x * g y = (∫⁻ x f x) * (∫⁻ y g y).
Русский
Если f и g измеримы по почти всем точкам, двойной линеграл от произведения равен произведению линегралов.
LaTeX
$$$\forall (β) [MeasurableSpace β], {ν : Measure β} {f : α \to \mathbb{R}_{\ge 0}^{\infty}} {g : β \to \mathbb{R}_{\ge 0}^{\infty}},\; (hf : AEMeasurable f μ) (hg : AEMeasurable g ν) \Rightarrow ∫^- x, ∫^- y, f x * g y ∂ν ∂μ = (∫^- x, f x ∂μ) * ∫^- y, g y ∂ν$$$
Lean4
theorem lintegral_trim {μ : Measure α} (hm : m ≤ m0) {f : α → ℝ≥0∞} (hf : Measurable[m] f) :
∫⁻ a, f a ∂μ.trim hm = ∫⁻ a, f a ∂μ :=
by
refine @Measurable.ennreal_induction α m (fun f => ∫⁻ a, f a ∂μ.trim hm = ∫⁻ a, f a ∂μ) ?_ ?_ ?_ f hf
· intro c s hs
rw [lintegral_indicator hs, lintegral_indicator (hm s hs), setLIntegral_const, setLIntegral_const]
suffices h_trim_s : μ.trim hm s = μ s by rw [h_trim_s]
exact trim_measurableSet_eq hm hs
· intro f g _ hf _ hf_prop hg_prop
have h_m := lintegral_add_left (μ := Measure.trim μ hm) hf g
have h_m0 := lintegral_add_left (μ := μ) (Measurable.mono hf hm le_rfl) g
rwa [hf_prop, hg_prop, ← h_m0] at h_m
· intro f hf hf_mono hf_prop
rw [lintegral_iSup hf hf_mono]
rw [lintegral_iSup (fun n => Measurable.mono (hf n) hm le_rfl) hf_mono]
congr with n
exact hf_prop n
