theorem helperForTheorem_8_6_integrable_of_absIntegrable (f : ℝ × ℝ → ℝ) (hf_meas : AEMeasurable f MeasureTheory.volume) (hfin : MeasureTheory.Integrable (fun (z : ℝ × ℝ) => |f z|) MeasureTheory.volume) : MeasureTheory.Integrable f MeasureTheory.volume

Helper for Theorem 8.6: absolute integrability of a real-valued function on ℝ² implies its integrability.

theorem helperForTheorem_8_6_sections_and_outer_integrable (f : ℝ × ℝ → ℝ) (hf_int : MeasureTheory.Integrable f MeasureTheory.volume) : (∀ᵐ (x : ℝ), MeasureTheory.Integrable (fun (y : ℝ) => f (x, y)) MeasureTheory.volume) ∧ (∀ᵐ (y : ℝ), MeasureTheory.Integrable (fun (x : ℝ) => f (x, y)) MeasureTheory.volume) ∧ MeasureTheory.Integrable (fun (x : ℝ) => ∫ (y : ℝ), f (x, y)) MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (y : ℝ) => ∫ (x : ℝ), f (x, y)) MeasureTheory.volume

Helper for Theorem 8.6: integrability on ℝ² gives a.e. integrable sections and integrability of the iterated-integral functions.

theorem helperForTheorem_8_6_fubini_equalities_for_f (f : ℝ × ℝ → ℝ) (hf_int : MeasureTheory.Integrable f MeasureTheory.volume) : ∫ (z : ℝ × ℝ), f z = ∫ (x : ℝ) (y : ℝ), f (x, y) ∧ ∫ (x : ℝ) (y : ℝ), f (x, y) = ∫ (y : ℝ) (x : ℝ), f (x, y)

Helper for Theorem 8.6: Fubini equalities for an integrable real-valued function on ℝ².

theorem helperForTheorem_8_6_tonelli_equalities_for_abs (f : ℝ × ℝ → ℝ) (hfin : MeasureTheory.Integrable (fun (z : ℝ × ℝ) => |f z|) MeasureTheory.volume) : ∫ (x : ℝ) (y : ℝ), |f (x, y)| = ∫ (z : ℝ × ℝ), |f z| ∧ ∫ (z : ℝ × ℝ), |f z| = ∫ (y : ℝ) (x : ℝ), |f (x, y)|

Helper for Theorem 8.6: Tonelli equalities for the absolute value |f| on ℝ².

theorem fubini_tonelli_absolutely_integrable_R2 (f : ℝ × ℝ → ℝ) (hf_meas : AEMeasurable f MeasureTheory.volume) (hfin : MeasureTheory.Integrable (fun (z : ℝ × ℝ) => |f z|) MeasureTheory.volume) : (∀ᵐ (x : ℝ), MeasureTheory.Integrable (fun (y : ℝ) => f (x, y)) MeasureTheory.volume) ∧ (∀ᵐ (y : ℝ), MeasureTheory.Integrable (fun (x : ℝ) => f (x, y)) MeasureTheory.volume) ∧ MeasureTheory.Integrable (fun (x : ℝ) => ∫ (y : ℝ), f (x, y)) MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (y : ℝ) => ∫ (x : ℝ), f (x, y)) MeasureTheory.volume ∧ ∫ (z : ℝ × ℝ), f z = ∫ (x : ℝ) (y : ℝ), f (x, y) ∧ ∫ (x : ℝ) (y : ℝ), f (x, y) = ∫ (y : ℝ) (x : ℝ), f (x, y) ∧ ∫ (x : ℝ) (y : ℝ), |f (x, y)| = ∫ (z : ℝ × ℝ), |f z| ∧ ∫ (z : ℝ × ℝ), |f z| = ∫ (y : ℝ) (x : ℝ), |f (x, y)|

Theorem 8.6 (Fubini--Tonelli for absolutely integrable functions on ℝ²): if f : ℝ × ℝ → ℝ is Lebesgue measurable and ∫ |f| < ∞ on ℝ², then for almost every x the section y ↦ f (x, y) is integrable, for almost every y the section x ↦ f (x, y) is integrable, the iterated-integral functions are integrable, and both the Fubini equalities for f and for |f| hold.

theorem fubini_theorem_R2 (f : ℝ × ℝ → ℝ) (hf_meas : AEMeasurable f MeasureTheory.volume) (hfin : MeasureTheory.Integrable (fun (z : ℝ × ℝ) => |f z|) MeasureTheory.volume) : (∀ᵐ (x : ℝ), MeasureTheory.Integrable (fun (y : ℝ) => f (x, y)) MeasureTheory.volume) ∧ MeasureTheory.Integrable (fun (x : ℝ) => ∫ (y : ℝ), f (x, y)) MeasureTheory.volume ∧ (∀ᵐ (y : ℝ), MeasureTheory.Integrable (fun (x : ℝ) => f (x, y)) MeasureTheory.volume) ∧ MeasureTheory.Integrable (fun (y : ℝ) => ∫ (x : ℝ), f (x, y)) MeasureTheory.volume ∧ ∫ (x : ℝ) (y : ℝ), f (x, y) = ∫ (z : ℝ × ℝ), f z ∧ ∫ (z : ℝ × ℝ), f z = ∫ (y : ℝ) (x : ℝ), f (x, y)

Theorem 8.7 (Fubini's theorem): if f : ℝ × ℝ → ℝ is Lebesgue measurable and ∫ |f| < ∞ on ℝ², then (1) for almost every x, the section y ↦ f (x, y) is absolutely integrable and F x := ∫ y, f (x, y) defines an L¹ function of x; (2) for almost every y, the section x ↦ f (x, y) is absolutely integrable and G y := ∫ x, f (x, y) defines an L¹ function of y; and (3) the two iterated integrals agree with the integral over ℝ².