From 22bdec32ff6d17c76d7171837bed295dce6bdaed Mon Sep 17 00:00:00 2001 From: Terence Tao Date: Sun, 2 Aug 2026 09:12:45 -0700 Subject: [PATCH] Section 11.5: correct Exercise 11.5.1 continuity statement MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `fun x ↦ 1/x` is not continuous on `Icc 0 1`: with Lean's `1/0 = 0`, the function fails to be continuous at `0` within the interval, so the stated `ContinuousOn` goal was false and the `sorry` unprovable. Negate it, matching the exercise's intent that Corollary 11.5.2 does not apply here. Also label both parts as Exercise 11.5.1, which they previously lacked. Co-Authored-By: Claude Opus 5 (1M context) --- Analysis/Section_11_5.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Analysis/Section_11_5.lean b/Analysis/Section_11_5.lean index 188d9b53..7564432e 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) -example : ContinuousOn (fun x:ℝ ↦ 1/x) (Icc 0 1) := by sorry +/-- Exercise 11.5.1 -/ +example : ¬ ContinuousOn (fun x:ℝ ↦ 1/x) (Icc 0 1) := by sorry +/-- Exercise 11.5.1 -/ example : ¬ IntegrableOn (fun x:ℝ ↦ 1/x) (Icc 0 1) := by sorry open PiecewiseConstantOn ConstantOn in