English
Tonelli's theorem for product, for nonnegative functions: the integral over μ×ν equals the iterated integral over μ then ν.
Русский
Т Tonelli для произведения мер: интеграл по μ×ν равен повторному интегралу по μ затем ν.
LaTeX
$$$\int f \, d(\mu \times \nu) = \int \left( \int f \ d\nu \right) d\mu$$$
Lean4
/-- **Tonelli's Theorem**: For `ℝ≥0∞`-valued almost everywhere measurable functions on `α × β`,
the integral of `f` is equal to the iterated integral. -/
theorem lintegral_prod (f : α × β → ℝ≥0∞) (hf : AEMeasurable f (μ.prod ν)) :
∫⁻ z, f z ∂μ.prod ν = ∫⁻ x, ∫⁻ y, f (x, y) ∂ν ∂μ :=
by
rw [Measure.prod] at *
rw [lintegral_bind Measurable.map_prodMk_left.aemeasurable hf]
apply lintegral_congr_ae
filter_upwards [Measurable.map_prodMk_left.aemeasurable.ae_of_bind hf] with a ha
exact lintegral_map' ha (by fun_prop)
