From 756cdbd7ff9762334178162f7ac8f852c6d6064f Mon Sep 17 00:00:00 2001 From: Taksh Date: Sat, 25 Jul 2026 09:05:53 +0300 Subject: [PATCH 1/3] fix(MeasureTheory): require nonempty for continuous Riemann lemmas RiemannIntegrableOn needs I.toSet.Nonempty; continuous/piecewise_continuous omitted it, so empty Icc a b with a > b made the conclusions false. Co-authored-by: Cursor --- Analysis/MeasureTheory/Section_1_1_3.lean | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/Analysis/MeasureTheory/Section_1_1_3.lean b/Analysis/MeasureTheory/Section_1_1_3.lean index 1e8e5b3c..597246f8 100644 --- a/Analysis/MeasureTheory/Section_1_1_3.lean +++ b/Analysis/MeasureTheory/Section_1_1_3.lean @@ -1040,13 +1040,16 @@ lemma RiemannIntegrableOn.iff_darbouxIntegrable {f:ℝ → ℝ} {I: BoundedInter lemma riemann_integral_eq_darboux_integral {f:ℝ → ℝ} {I: BoundedInterval} (hf: RiemannIntegrableOn f I) : riemannIntegral f I = darbouxIntegral f I := by sorry /-- Exercise 1.1.23 -/ --- Any function continuous on a closed interval is Riemann integrable. -lemma RiemannIntegrableOn.continuous {f:ℝ → ℝ} {I: BoundedInterval} (hI: I = Icc I.a I.b) (hcont: ContinuousOn f I.toSet) : RiemannIntegrableOn f I := by sorry +-- Any function continuous on a nonempty closed interval is Riemann integrable. +lemma RiemannIntegrableOn.continuous {f:ℝ → ℝ} {I: BoundedInterval} (hI: I = Icc I.a I.b) + (hnonempty : I.toSet.Nonempty) (hcont: ContinuousOn f I.toSet) : RiemannIntegrableOn f I := by sorry -- A function that is continuous on each piece of a partition is Riemann integrable on the whole interval. lemma RiemannIntegrableOn.piecewise_continuous {f:ℝ → ℝ} {I: BoundedInterval} (hI: I = Icc I.a I.b) - (T: Finset BoundedInterval) (hdisjoint: (T : Set BoundedInterval).PairwiseDisjoint BoundedInterval.toSet) - (hcover : I.toSet = ⋃ J ∈ T, J.toSet) (hcont: ∀ J ∈ T, ContinuousOn f J.toSet) : RiemannIntegrableOn f I := by sorry + (hnonempty : I.toSet.Nonempty) + (T: Finset BoundedInterval) (hdisjoint: (T : Set BoundedInterval).PairwiseDisjoint BoundedInterval.toSet) + (hcover : I.toSet = ⋃ J ∈ T, J.toSet) (hcont: ∀ J ∈ T, ContinuousOn f J.toSet) : + RiemannIntegrableOn f I := by sorry /-- Exercise 1.1.24 (a) (scalar multiple, integrability). -/ -- A scalar multiple of a Riemann integrable function is Riemann integrable. From acda7ac7ab404066eec0fc2fcbdcbc7a3dee331e Mon Sep 17 00:00:00 2001 From: Taksh Date: Sat, 25 Jul 2026 09:06:03 +0300 Subject: [PATCH 2/3] fix(MeasureTheory): align DarbouxIntegrableOn with Riemann nonempty Empty reversed intervals made DarbouxIntegrableOn hold vacuously while RiemannIntegrableOn failed, so iff_darbouxIntegrable was false. Co-authored-by: Cursor --- Analysis/MeasureTheory/Section_1_1_3.lean | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/Analysis/MeasureTheory/Section_1_1_3.lean b/Analysis/MeasureTheory/Section_1_1_3.lean index 1e8e5b3c..e9fa3615 100644 --- a/Analysis/MeasureTheory/Section_1_1_3.lean +++ b/Analysis/MeasureTheory/Section_1_1_3.lean @@ -943,8 +943,11 @@ lemma lower_darboux_le_upper_darboux {f:ℝ → ℝ} {I: BoundedInterval} (hboun exact PiecewiseConstantFunction.integral_mono' g h h_pointwise /-- Definition 1.1.6 (Darboux integral) -/ --- A function is Darboux integrable if it is bounded and its lower and upper Darboux integrals coincide. -noncomputable def DarbouxIntegrableOn (f:ℝ → ℝ) (I: BoundedInterval) : Prop := (I = Icc I.a I.b) ∧ ∃ M, ∀ x ∈ I, |f x| ≤ M ∧ LowerDarbouxIntegral f I = UpperDarbouxIntegral f I +-- A function is Darboux integrable if it is bounded on a nonempty closed interval and its +-- lower and upper Darboux integrals coincide. Nonemptiness matches {name}`RiemannIntegrableOn`. +noncomputable def DarbouxIntegrableOn (f:ℝ → ℝ) (I: BoundedInterval) : Prop := + (I = Icc I.a I.b) ∧ I.toSet.Nonempty ∧ + (∃ M, ∀ x ∈ I, |f x| ≤ M) ∧ LowerDarbouxIntegral f I = UpperDarbouxIntegral f I /-- We give the Darboux integral the "junk" value of the lower Darboux integral when the function is not integrable. -/ -- The Darboux integral: equals the common value if integrable, otherwise the lower Darboux integral. From 336367ec91f185c5e0cc3e2c5ab88d490cc9e622 Mon Sep 17 00:00:00 2001 From: Taksh Date: Sat, 25 Jul 2026 09:06:19 +0300 Subject: [PATCH 3/3] fix(MeasureTheory): require closed nonempty I for indicator Riemann indicator_of_elem claimed RiemannIntegrableOn on any BoundedInterval; open intervals make the conclusion false, and riemann_integral_of_elem then returned the junk value 0 instead of the Jordan measure. Co-authored-by: Cursor --- Analysis/MeasureTheory/Section_1_1_3.lean | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/Analysis/MeasureTheory/Section_1_1_3.lean b/Analysis/MeasureTheory/Section_1_1_3.lean index 1e8e5b3c..a04be721 100644 --- a/Analysis/MeasureTheory/Section_1_1_3.lean +++ b/Analysis/MeasureTheory/Section_1_1_3.lean @@ -1069,12 +1069,18 @@ theorem riemann_integral_add {I: BoundedInterval} {f g: ℝ → ℝ} (hf: Rieman theorem riemann_integral_mono {I: BoundedInterval} {f g: ℝ → ℝ} (hf: RiemannIntegrableOn f I) (hg: RiemannIntegrableOn g I) (hmono: ∀ x ∈ I.toSet, f x ≤ g x): riemannIntegral f I ≤ riemannIntegral g I := by sorry /-- Exercise 1.1.24 (c) (Indicator functions) -/ --- The indicator function of a Jordan measurable set is Riemann integrable. -theorem RiemannIntegrableOn.indicator_of_elem (I: BoundedInterval) {E:Set ℝ} (hE: JordanMeasurable (Real.equiv_EuclideanSpace' '' E) ) : RiemannIntegrableOn E.indicator' I := by sorry +-- The indicator function of a Jordan measurable set is Riemann integrable on a nonempty closed interval. +theorem RiemannIntegrableOn.indicator_of_elem {I: BoundedInterval} (hI: I = Icc I.a I.b) + (hnonempty : I.toSet.Nonempty) {E:Set ℝ} + (hE: JordanMeasurable (Real.equiv_EuclideanSpace' '' E)) : + RiemannIntegrableOn E.indicator' I := by sorry /-- Exercise 1.1.24 (c) (Piecewise constant integral of indicator functions) -/ -- The integral of an indicator function equals the measure of the set it indicates. -theorem riemann_integral_of_elem {I: BoundedInterval} {E:Set ℝ} (hE: JordanMeasurable (Real.equiv_EuclideanSpace' '' E) ) (hsub: E ⊆ I.toSet) : riemannIntegral E.indicator' I = hE.measure := by sorry +theorem riemann_integral_of_elem {I: BoundedInterval} (hI: I = Icc I.a I.b) + (hnonempty : I.toSet.Nonempty) {E:Set ℝ} + (hE: JordanMeasurable (Real.equiv_EuclideanSpace' '' E)) (hsub: E ⊆ I.toSet) : + riemannIntegral E.indicator' I = hE.measure := by sorry /-- Exercise 1.1.24 (Uniqueness) -/ -- The Riemann integral is the unique integral satisfying linearity, monotonicity, and normalization on indicator functions.