From d83d11959f8dbac798390cc8ce745b630c5ca015 Mon Sep 17 00:00:00 2001 From: Taksh Date: Wed, 12 Aug 2026 21:56:23 +0530 Subject: [PATCH] fix: Exercise 1.1.7(i) needs the box to be closed A Box is a product of BoundedIntervals, which need not be closed, and ContinuousOn f B.toSet on a non-closed box does not force f to be bounded. Taking d = 1, B = Ioo 0 1 and f x = 1 / x (continuous on B.toSet) makes the graph, and the region under it, unbounded, so neither is Jordan measurable -- JordanMeasurable carries a boundedness field. Requiring IsClosed B.toSet makes B.toSet compact, so f is bounded and uniformly continuous there, which is the hypothesis the textbook exercise uses. IsClosed B.toSet is the same way closed boxes are spelled elsewhere (Section_1_2_1). Signed-off-by: Taksh --- Analysis/MeasureTheory/Section_1_1_2.lean | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/Analysis/MeasureTheory/Section_1_1_2.lean b/Analysis/MeasureTheory/Section_1_1_2.lean index d13a3dba7..ff41aa168 100644 --- a/Analysis/MeasureTheory/Section_1_1_2.lean +++ b/Analysis/MeasureTheory/Section_1_1_2.lean @@ -660,15 +660,22 @@ lemma JordanMeasurable.measure_of_translate {d:ℕ} {E: Set (EuclideanSpace' d)} · exact eq_outer hE; /-- Exercise 1.1.7 (i) (Regions under graphs are Jordan measurable) -/ -lemma JordanMeasurable.graph {d:ℕ} {B:Box d} {f: EuclideanSpace' d → ℝ} (hf: ContinuousOn f B.toSet) : JordanMeasurable { p | ∃ x ∈ B.toSet, EuclideanSpace'.prod_equiv d 1 p = ⟨ x, f x ⟩ } := by +lemma JordanMeasurable.graph {d:ℕ} {B:Box d} (hB: IsClosed B.toSet) {f: EuclideanSpace' d → ℝ} + (hf: ContinuousOn f B.toSet) : + JordanMeasurable { p | ∃ x ∈ B.toSet, EuclideanSpace'.prod_equiv d 1 p = ⟨ x, f x ⟩ } := by sorry /-- Exercise 1.1.7 (i) (Regions under graphs are Jordan measurable) -/ -lemma JordanMeasurable.measure_of_graph {d:ℕ} {B:Box d} {f: EuclideanSpace' d → ℝ} (hf: ContinuousOn f B.toSet) : (JordanMeasurable.graph hf).measure = 0 := by +lemma JordanMeasurable.measure_of_graph {d:ℕ} {B:Box d} (hB: IsClosed B.toSet) + {f: EuclideanSpace' d → ℝ} (hf: ContinuousOn f B.toSet) : + (JordanMeasurable.graph hB hf).measure = 0 := by sorry /-- Exercise 1.1.7 (i) (Regions under graphs are Jordan measurable) -/ -lemma JordanMeasurable.undergraph {d:ℕ} {B:Box d} {f: EuclideanSpace' d → ℝ} (hf: ContinuousOn f B.toSet) : JordanMeasurable { p | ∃ x ∈ B.toSet, ∃ t:ℝ, EuclideanSpace'.prod_equiv d 1 p = ⟨ x, t ⟩ ∧ 0 ≤ t ∧ t ≤ f x } := by +lemma JordanMeasurable.undergraph {d:ℕ} {B:Box d} (hB: IsClosed B.toSet) + {f: EuclideanSpace' d → ℝ} (hf: ContinuousOn f B.toSet) : + JordanMeasurable + { p | ∃ x ∈ B.toSet, ∃ t:ℝ, EuclideanSpace'.prod_equiv d 1 p = ⟨ x, t ⟩ ∧ 0 ≤ t ∧ t ≤ f x } := by sorry /-- Exercise 1.1.8(i) (A triangle is Jordan measurable) -/