From f3b69433675bedd46ca44ebaf9a15dab08ebfbe4 Mon Sep 17 00:00:00 2001 From: Terence Tao Date: Mon, 3 Aug 2026 07:59:15 -0700 Subject: [PATCH] Measure theory 1.2.2: restore Exercise 1.2.13 to the text's statement MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Exercise 1.2.13 in the text defines pointwise convergence of sets via pointwise convergence of the indicator functions, and then asks: (i) if the E_n are measurable and converge pointwise to E, show E is measurable; (ii) if additionally the E_n lie in a measurable F of finite measure, show m(E_n) -> m(E); (iii) give a counterexample when the E_n are not contained in a set of finite measure. Throughout, E is given and the convergence is pointwise everywhere, not almost everywhere. #582 replaced this with an a.e. formulation and, in doing so, moved E from a hypothesis into the goal, making (i) and (ii) false: for E_n alternating between the empty set and the whole space (resp. F), the indicators oscillate at every point, so no measurable E₀ has 1_{E_n} -> 1_{E₀} off a null set. This restores the previous statements, which match the text. Co-Authored-By: Claude Opus 5 (1M context) --- Analysis/MeasureTheory/Section_1_2_2.lean | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) diff --git a/Analysis/MeasureTheory/Section_1_2_2.lean b/Analysis/MeasureTheory/Section_1_2_2.lean index ebca1f47..9f66bc42 100644 --- a/Analysis/MeasureTheory/Section_1_2_2.lean +++ b/Analysis/MeasureTheory/Section_1_2_2.lean @@ -1657,23 +1657,18 @@ example {d:ℕ} (m: Set (EuclideanSpace' d) → EReal) (h_empty: m ∅ = 0) (h_p sorry /-- Exercise 1.2.13(i) -/ -example {d:ℕ} {E: ℕ → Set (EuclideanSpace' d)} (hE: ∀ n, LebesgueMeasurable (E n)) : - ∃ E₀, LebesgueMeasurable E₀ ∧ - IsNull {x | ¬ Filter.atTop.Tendsto (fun n ↦ (E n).indicator' x) (nhds (E₀.indicator' x))} := by sorry +example {d:ℕ} {E: ℕ → Set (EuclideanSpace' d)} {E₀: Set (EuclideanSpace' d)} (hE: ∀ n, LebesgueMeasurable (E n)) (hpoint: ∀ x, Filter.atTop.Tendsto (fun n ↦ (E n).indicator' x) (nhds (E₀.indicator' x))) : LebesgueMeasurable E₀ := by sorry /-- Exercise 1.2.13(ii) -/ -example {d:ℕ} {E: ℕ → Set (EuclideanSpace' d)} {F: Set (EuclideanSpace' d)} +example {d:ℕ} {E: ℕ → Set (EuclideanSpace' d)} {E₀ F: Set (EuclideanSpace' d)} (hE: ∀ n, LebesgueMeasurable (E n)) - (hsub: ∀ n, E n ⊆ F) (hFmes: LebesgueMeasurable F) (hfin: Lebesgue_measure F < ⊤) : - ∃ E₀, LebesgueMeasurable E₀ ∧ - IsNull {x | ¬ Filter.atTop.Tendsto (fun n ↦ (E n).indicator' x) (nhds (E₀.indicator' x))} ∧ - Filter.atTop.Tendsto (fun n ↦ Lebesgue_measure (E n)) (nhds (Lebesgue_measure E₀)) := by sorry + (hpoint: ∀ x, Filter.atTop.Tendsto (fun n ↦ (E n).indicator' x) (nhds (E₀.indicator' x))) + (hsub: ∀ n, E n ⊆ F) (hFmes: LebesgueMeasurable F) (hfin: Lebesgue_measure F < ⊤) : Filter.atTop.Tendsto (fun n ↦ Lebesgue_measure (E n)) (nhds (Lebesgue_measure E₀)) := by sorry /-- Exercise 1.2.13(iii) -/ example : ∃ (d:ℕ) (E: ℕ → Set (EuclideanSpace' d)) (E₀ F: Set (EuclideanSpace' d)) (hE: ∀ n, LebesgueMeasurable (E n)) - (hE₀: LebesgueMeasurable E₀) - (hpoint : IsNull {x | ¬ Filter.atTop.Tendsto (fun n ↦ (E n).indicator' x) (nhds (E₀.indicator' x))}) + (hpoint: ∀ x, Filter.atTop.Tendsto (fun n ↦ (E n).indicator' x) (nhds (E₀.indicator' x))) (hsub: ∀ n, E n ⊆ F) (hFmes: LebesgueMeasurable F), ¬ Filter.atTop.Tendsto (fun n ↦ Lebesgue_measure (E n)) (nhds (Lebesgue_measure E₀)) := by sorry /-- Exercise 1.2.14 -/