From 8c72237b5e863a5b3a323af6611d731785ae5591 Mon Sep 17 00:00:00 2001 From: Taksh Date: Tue, 4 Aug 2026 19:14:50 +0530 Subject: [PATCH 1/3] fix: drop stray space in Exercise 1.3.23 Lusin docstring --- Analysis/MeasureTheory/Section_1_3_5.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Analysis/MeasureTheory/Section_1_3_5.lean b/Analysis/MeasureTheory/Section_1_3_5.lean index afee6b45..9562a4ea 100644 --- a/Analysis/MeasureTheory/Section_1_3_5.lean +++ b/Analysis/MeasureTheory/Section_1_3_5.lean @@ -1568,7 +1568,7 @@ example : ∃ (d:ℕ) (f : EuclideanSpace' d → ℝ), def LocallyComplexAbsolutelyIntegrable {d:ℕ} (f: EuclideanSpace' d → ℂ) : Prop := ∀ (S: Set (EuclideanSpace' d)), LebesgueMeasurable S ∧ Bornology.IsBounded S → ComplexAbsolutelyIntegrableOn f S -/-- Exercise 1.3.23 (Lusin's theorem only requires local absolute integrability ). -/ +/-- Exercise 1.3.23 (Lusin's theorem only requires local absolute integrability). -/ theorem LocallyComplexAbsolutelyIntegrable.approx_by_continuous_outside_small {d:ℕ} {f : EuclideanSpace' d → ℂ} (hf: LocallyComplexAbsolutelyIntegrable f) (ε : ℝ) (hε : 0 < ε) : From 35c740989bdbfece1c1fe682680bad7aea6fb830 Mon Sep 17 00:00:00 2001 From: Taksh Date: Tue, 4 Aug 2026 19:14:50 +0530 Subject: [PATCH 2/3] =?UTF-8?q?fix:=20part-label=20Example=2011.5.5=20Vers?= =?UTF-8?q?o=20docs=20(a)=E2=80=93(e)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Analysis/Section_11_5.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Analysis/Section_11_5.lean b/Analysis/Section_11_5.lean index d23b322e..3512a8b0 100644 --- a/Analysis/Section_11_5.lean +++ b/Analysis/Section_11_5.lean @@ -203,14 +203,19 @@ noncomputable abbrev f_11_5_5 : ℝ → ℝ := fun x ↦ else if x = 2 then 7 else x^3 +/-- Example 11.5.5 (a) -/ example : ¬ ContinuousOn f_11_5_5 (Icc 1 3) := by sorry +/-- Example 11.5.5 (b) -/ example : ContinuousOn f_11_5_5 (Ico 1 2) := by sorry +/-- Example 11.5.5 (c) -/ example : ContinuousOn f_11_5_5 (Icc 2 2) := by sorry +/-- Example 11.5.5 (d) -/ example : ContinuousOn f_11_5_5 (Ioc 2 3) := by sorry +/-- Example 11.5.5 (e) -/ example : PiecewiseContinuousOn f_11_5_5 (Icc 1 3) := by sorry /-- Proposition 11.5.6 / Exercise 11.5.1 -/ From c2f07fe9adfdd16678c7b1fb6cca8a28d4a546d3 Mon Sep 17 00:00:00 2001 From: Taksh Date: Tue, 4 Aug 2026 19:14:50 +0530 Subject: [PATCH 3/3] fix: label 1/x examples as Cor. 11.5.2 sharpness They formalize the remark after the corollary, not Exercise 11.5.1. --- Analysis/Section_11_5.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Analysis/Section_11_5.lean b/Analysis/Section_11_5.lean index 3512a8b0..0126e396 100644 --- a/Analysis/Section_11_5.lean +++ b/Analysis/Section_11_5.lean @@ -83,8 +83,10 @@ theorem integ_of_uniform_cts {I: BoundedInterval} {f:ℝ → ℝ} (hf: UniformCo theorem integ_of_cts {a b:ℝ} {f:ℝ → ℝ} (hf: ContinuousOn f (Icc a b)) : IntegrableOn f (Icc a b) := integ_of_uniform_cts (UniformContinuousOn.of_continuousOn hf) +/-- Corollary 11.5.2 (sharpness) (a) -/ example : ¬ ContinuousOn (fun x:ℝ ↦ 1/x) (Icc 0 1) := by sorry +/-- Corollary 11.5.2 (sharpness) (b) -/ example : ¬ IntegrableOn (fun x:ℝ ↦ 1/x) (Icc 0 1) := by sorry open PiecewiseConstantOn ConstantOn in