Analysis II (Tao, 2022) -- Chapter 08 -- Section 05

open MeasureTheorysection Chap08section Section05

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

lemma helperForTheorem_8_6_integrable_of_absIntegrable (f : ℝ × ℝ → ℝ) (hf_meas : AEMeasurable f (volume : Measure (ℝ × ℝ))) (hfin : Integrable (fun z : ℝ × ℝ => |f z|)) : Integrable f := by have hnorm : Integrable (fun z : ℝ × ℝ => ‖f z‖) := by simpa [Real.norm_eq_abs] using hfin exact (integrable_norm_iff hf_meas.aestronglyMeasurable).1 hnorm

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

lemma helperForTheorem_8_6_sections_and_outer_integrable (f : ℝ × ℝ → ℝ) (hf_int : Integrable f) : (∀ᵐ x : ℝ ∂(volume : Measure ℝ), Integrable (fun y : ℝ => f (x, y))) ∧ (∀ᵐ y : ℝ ∂(volume : Measure ℝ), Integrable (fun x : ℝ => f (x, y))) ∧ Integrable (fun x : ℝ => ∫ y : ℝ, f (x, y) ∂(volume : Measure ℝ)) ∧ Integrable (fun y : ℝ => ∫ x : ℝ, f (x, y) ∂(volume : Measure ℝ)) := by have hf_prod : Integrable f ((volume : Measure ℝ).prod (volume : Measure ℝ)) := by simpa [Measure.volume_eq_prod] using hf_int refine ⟨?_, ?_, ?_, ?_⟩ · simpa using hf_prod.prod_right_ae · simpa using hf_prod.prod_left_ae · simpa using hf_prod.integral_prod_left · simpa using hf_prod.integral_prod_right

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

lemma helperForTheorem_8_6_fubini_equalities_for_f (f : ℝ × ℝ → ℝ) (hf_int : Integrable f) : (∫ z : ℝ × ℝ, f z ∂(volume : Measure (ℝ × ℝ))) = (∫ x : ℝ, (∫ y : ℝ, f (x, y) ∂(volume : Measure ℝ)) ∂(volume : Measure ℝ)) ∧ (∫ x : ℝ, (∫ y : ℝ, f (x, y) ∂(volume : Measure ℝ)) ∂(volume : Measure ℝ)) = (∫ y : ℝ, (∫ x : ℝ, f (x, y) ∂(volume : Measure ℝ)) ∂(volume : Measure ℝ)) := by have hf_prod : Integrable f ((volume : Measure ℝ).prod (volume : Measure ℝ)) := by simpa [Measure.volume_eq_prod] using hf_int have h_prod_eq_xy : (∫ z : ℝ × ℝ, f z ∂(volume : Measure (ℝ × ℝ))) = (∫ x : ℝ, (∫ y : ℝ, f (x, y) ∂(volume : Measure ℝ)) ∂(volume : Measure ℝ)) := by simpa [Measure.volume_eq_prod] using integral_prod f hf_prod have h_prod_eq_yx : (∫ z : ℝ × ℝ, f z ∂(volume : Measure (ℝ × ℝ))) = (∫ y : ℝ, (∫ x : ℝ, f (x, y) ∂(volume : Measure ℝ)) ∂(volume : Measure ℝ)) := by simpa [Measure.volume_eq_prod] using integral_prod_symm f hf_prod have h_xy_eq_yx : (∫ x : ℝ, (∫ y : ℝ, f (x, y) ∂(volume : Measure ℝ)) ∂(volume : Measure ℝ)) = (∫ y : ℝ, (∫ x : ℝ, f (x, y) ∂(volume : Measure ℝ)) ∂(volume : Measure ℝ)) := h_prod_eq_xy.symm.trans h_prod_eq_yx exact ⟨h_prod_eq_xy, h_xy_eq_yx⟩

Helper for Theorem 8.6: Tonelli equalities for the absolute value |sorry| : ?m.1|Unknown identifier `f`f| on .

lemma helperForTheorem_8_6_tonelli_equalities_for_abs (f : ℝ × ℝ → ℝ) (hfin : Integrable (fun z : ℝ × ℝ => |f z|)) : (∫ x : ℝ, (∫ y : ℝ, |f (x, y)| ∂(volume : Measure ℝ)) ∂(volume : Measure ℝ)) = (∫ z : ℝ × ℝ, |f z| ∂(volume : Measure (ℝ × ℝ))) ∧ (∫ z : ℝ × ℝ, |f z| ∂(volume : Measure (ℝ × ℝ))) = (∫ y : ℝ, (∫ x : ℝ, |f (x, y)| ∂(volume : Measure ℝ)) ∂(volume : Measure ℝ)) := by have habs_prod : Integrable (fun z : ℝ × ℝ => |f z|) ((volume : Measure ℝ).prod (volume : Measure ℝ)) := by simpa [Measure.volume_eq_prod] using hfin have h_prod_eq_xy_abs : (∫ z : ℝ × ℝ, |f z| ∂(volume : Measure (ℝ × ℝ))) = (∫ x : ℝ, (∫ y : ℝ, |f (x, y)| ∂(volume : Measure ℝ)) ∂(volume : Measure ℝ)) := by simpa [Measure.volume_eq_prod] using integral_prod (fun z : ℝ × ℝ => |f z|) habs_prod have h_prod_eq_yx_abs : (∫ z : ℝ × ℝ, |f z| ∂(volume : Measure (ℝ × ℝ))) = (∫ y : ℝ, (∫ x : ℝ, |f (x, y)| ∂(volume : Measure ℝ)) ∂(volume : Measure ℝ)) := by simpa [Measure.volume_eq_prod] using integral_prod_symm (fun z : ℝ × ℝ => |f z|) habs_prod exact ⟨h_prod_eq_xy_abs.symm, h_prod_eq_yx_abs⟩

Theorem 8.6 (Fubini--Tonelli for absolutely integrable functions on ): if is Lebesgue measurable and on , then for almost every Unknown identifier `x`x the section is integrable, for almost every Unknown identifier `y`y the section is integrable, the iterated-integral functions are integrable, and both the Fubini equalities for Unknown identifier `f`f and for |sorry| : ?m.1|Unknown identifier `f`f| hold.

theorem fubini_tonelli_absolutely_integrable_R2 (f : ℝ × ℝ → ℝ) (hf_meas : AEMeasurable f (volume : Measure (ℝ × ℝ))) (hfin : Integrable (fun z : ℝ × ℝ => |f z|)) : (∀ᵐ x : ℝ ∂(volume : Measure ℝ), Integrable (fun y : ℝ => f (x, y))) ∧ (∀ᵐ y : ℝ ∂(volume : Measure ℝ), Integrable (fun x : ℝ => f (x, y))) ∧ Integrable (fun x : ℝ => ∫ y : ℝ, f (x, y) ∂(volume : Measure ℝ)) ∧ Integrable (fun y : ℝ => ∫ x : ℝ, f (x, y) ∂(volume : Measure ℝ)) ∧ (∫ z : ℝ × ℝ, f z ∂(volume : Measure (ℝ × ℝ))) = (∫ x : ℝ, (∫ y : ℝ, f (x, y) ∂(volume : Measure ℝ)) ∂(volume : Measure ℝ)) ∧ (∫ x : ℝ, (∫ y : ℝ, f (x, y) ∂(volume : Measure ℝ)) ∂(volume : Measure ℝ)) = (∫ y : ℝ, (∫ x : ℝ, f (x, y) ∂(volume : Measure ℝ)) ∂(volume : Measure ℝ)) ∧ (∫ x : ℝ, (∫ y : ℝ, |f (x, y)| ∂(volume : Measure ℝ)) ∂(volume : Measure ℝ)) = (∫ z : ℝ × ℝ, |f z| ∂(volume : Measure (ℝ × ℝ))) ∧ (∫ z : ℝ × ℝ, |f z| ∂(volume : Measure (ℝ × ℝ))) = (∫ y : ℝ, (∫ x : ℝ, |f (x, y)| ∂(volume : Measure ℝ)) ∂(volume : Measure ℝ)) := by have hf_int : Integrable f := helperForTheorem_8_6_integrable_of_absIntegrable f hf_meas hfin have h_sections : (∀ᵐ x : ℝ ∂(volume : Measure ℝ), Integrable (fun y : ℝ => f (x, y))) ∧ (∀ᵐ y : ℝ ∂(volume : Measure ℝ), Integrable (fun x : ℝ => f (x, y))) ∧ Integrable (fun x : ℝ => ∫ y : ℝ, f (x, y) ∂(volume : Measure ℝ)) ∧ Integrable (fun y : ℝ => ∫ x : ℝ, f (x, y) ∂(volume : Measure ℝ)) := helperForTheorem_8_6_sections_and_outer_integrable f hf_int have h_fubini : (∫ z : ℝ × ℝ, f z ∂(volume : Measure (ℝ × ℝ))) = (∫ x : ℝ, (∫ y : ℝ, f (x, y) ∂(volume : Measure ℝ)) ∂(volume : Measure ℝ)) ∧ (∫ x : ℝ, (∫ y : ℝ, f (x, y) ∂(volume : Measure ℝ)) ∂(volume : Measure ℝ)) = (∫ y : ℝ, (∫ x : ℝ, f (x, y) ∂(volume : Measure ℝ)) ∂(volume : Measure ℝ)) := helperForTheorem_8_6_fubini_equalities_for_f f hf_int have h_tonelli_abs : (∫ x : ℝ, (∫ y : ℝ, |f (x, y)| ∂(volume : Measure ℝ)) ∂(volume : Measure ℝ)) = (∫ z : ℝ × ℝ, |f z| ∂(volume : Measure (ℝ × ℝ))) ∧ (∫ z : ℝ × ℝ, |f z| ∂(volume : Measure (ℝ × ℝ))) = (∫ y : ℝ, (∫ x : ℝ, |f (x, y)| ∂(volume : Measure ℝ)) ∂(volume : Measure ℝ)) := helperForTheorem_8_6_tonelli_equalities_for_abs f hfin rcases h_sections with ⟨h_sec_x, h_sec_y, h_int_x, h_int_y⟩ rcases h_fubini with ⟨h_prod_eq_xy, h_xy_eq_yx⟩ rcases h_tonelli_abs with ⟨h_abs_xy_eq_prod, h_abs_prod_eq_yx⟩ exact ⟨h_sec_x, h_sec_y, h_int_x, h_int_y, h_prod_eq_xy, h_xy_eq_yx, h_abs_xy_eq_prod, h_abs_prod_eq_yx⟩

Theorem 8.7 (Fubini's theorem): if is Lebesgue measurable and on , then (1) for almost every Unknown identifier `x`x, the section is absolutely integrable and defines an function of Unknown identifier `x`x; (2) for almost every Unknown identifier `y`y, the section is absolutely integrable and defines an function of Unknown identifier `y`y; and (3) the two iterated integrals agree with the integral over .

theorem fubini_theorem_R2 (f : ℝ × ℝ → ℝ) (hf_meas : AEMeasurable f (volume : Measure (ℝ × ℝ))) (hfin : Integrable (fun z : ℝ × ℝ => |f z|)) : (∀ᵐ x : ℝ ∂(volume : Measure ℝ), Integrable (fun y : ℝ => f (x, y))) ∧ Integrable (fun x : ℝ => ∫ y : ℝ, f (x, y) ∂(volume : Measure ℝ)) ∧ (∀ᵐ y : ℝ ∂(volume : Measure ℝ), Integrable (fun x : ℝ => f (x, y))) ∧ Integrable (fun y : ℝ => ∫ x : ℝ, f (x, y) ∂(volume : Measure ℝ)) ∧ (∫ x : ℝ, (∫ y : ℝ, f (x, y) ∂(volume : Measure ℝ)) ∂(volume : Measure ℝ)) = (∫ z : ℝ × ℝ, f z ∂(volume : Measure (ℝ × ℝ))) ∧ (∫ z : ℝ × ℝ, f z ∂(volume : Measure (ℝ × ℝ))) = (∫ y : ℝ, (∫ x : ℝ, f (x, y) ∂(volume : Measure ℝ)) ∂(volume : Measure ℝ)) := by rcases fubini_tonelli_absolutely_integrable_R2 f hf_meas hfin with ⟨h_sec_x, h_sec_y, h_int_x, h_int_y, h_prod_eq_xy, h_xy_eq_yx, _, _⟩ have h_xy_eq_prod : (∫ x : ℝ, (∫ y : ℝ, f (x, y) ∂(volume : Measure ℝ)) ∂(volume : Measure ℝ)) = (∫ z : ℝ × ℝ, f z ∂(volume : Measure (ℝ × ℝ))) := h_prod_eq_xy.symm have h_prod_eq_yx : (∫ z : ℝ × ℝ, f z ∂(volume : Measure (ℝ × ℝ))) = (∫ y : ℝ, (∫ x : ℝ, f (x, y) ∂(volume : Measure ℝ)) ∂(volume : Measure ℝ)) := h_prod_eq_xy.trans h_xy_eq_yx exact ⟨h_sec_x, h_int_x, h_sec_y, h_int_y, h_xy_eq_prod, h_prod_eq_yx⟩
end Section05end Chap08