From ddec488423e616ea61593d8c899f1bc4e1d72f59 Mon Sep 17 00:00:00 2001 From: Taksh Date: Tue, 8 Sep 2026 16:09:30 +0530 Subject: [PATCH 1/4] Record that the EReal indicator is toEReal after the real indicator. This is the representation used by the unsigned simple-function calculus. --- Analysis/MeasureTheory/Section_1_3_1.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Analysis/MeasureTheory/Section_1_3_1.lean b/Analysis/MeasureTheory/Section_1_3_1.lean index 081c25343..117150c2e 100644 --- a/Analysis/MeasureTheory/Section_1_3_1.lean +++ b/Analysis/MeasureTheory/Section_1_3_1.lean @@ -24,8 +24,7 @@ noncomputable def EReal.indicator {X:Type*} (A: Set X) : X → EReal := Real.ERe theorem EReal.indicator_of_mem {X:Type*} {A: Set X} {x:X} (h: x ∈ A) : EReal.indicator A x = 1 := by simp [EReal.indicator, Real.EReal_fun, Set.indicator'_of_mem h] -theorem EReal.indicator_of_notMem {X:Type*} {A: Set X} {x:X} (h: x ∉ A) : EReal.indicator A x = 0 := by - simp [EReal.indicator, Real.EReal_fun, Set.indicator'_of_notMem h] +theorem EReal.indicator_eq_comp {X:Type*} (A: Set X) : EReal.indicator A = Real.toEReal ∘ A.indicator' := rfl noncomputable def Complex.indicator {X:Type*} (A: Set X) : X → ℂ := Real.complex_fun A.indicator' From a8fdc7f4256b24232c600493ec3154b156729e10 Mon Sep 17 00:00:00 2001 From: Taksh Date: Tue, 8 Sep 2026 16:09:58 +0530 Subject: [PATCH 2/4] Keep the off-set evaluation of the EReal indicator. The on-set and off-set lemmas are used throughout the simple-function identities. --- Analysis/MeasureTheory/Section_1_3_1.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Analysis/MeasureTheory/Section_1_3_1.lean b/Analysis/MeasureTheory/Section_1_3_1.lean index 117150c2e..0edc33041 100644 --- a/Analysis/MeasureTheory/Section_1_3_1.lean +++ b/Analysis/MeasureTheory/Section_1_3_1.lean @@ -24,6 +24,9 @@ noncomputable def EReal.indicator {X:Type*} (A: Set X) : X → EReal := Real.ERe theorem EReal.indicator_of_mem {X:Type*} {A: Set X} {x:X} (h: x ∈ A) : EReal.indicator A x = 1 := by simp [EReal.indicator, Real.EReal_fun, Set.indicator'_of_mem h] +theorem EReal.indicator_of_notMem {X:Type*} {A: Set X} {x:X} (h: x ∉ A) : EReal.indicator A x = 0 := by + simp [EReal.indicator, Real.EReal_fun, Set.indicator'_of_notMem h] + theorem EReal.indicator_eq_comp {X:Type*} (A: Set X) : EReal.indicator A = Real.toEReal ∘ A.indicator' := rfl noncomputable def Complex.indicator {X:Type*} (A: Set X) : X → ℂ := Real.complex_fun A.indicator' From 15f4027e72d7cdd376375a8a10b76a4efcdd2661 Mon Sep 17 00:00:00 2001 From: Taksh Date: Tue, 8 Sep 2026 16:10:23 +0530 Subject: [PATCH 3/4] Fill that measurable indicators are unsigned simple functions. A one-term representation with coefficient one is the definition. --- Analysis/MeasureTheory/Section_1_3_1.lean | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/Analysis/MeasureTheory/Section_1_3_1.lean b/Analysis/MeasureTheory/Section_1_3_1.lean index 0edc33041..a52f396c6 100644 --- a/Analysis/MeasureTheory/Section_1_3_1.lean +++ b/Analysis/MeasureTheory/Section_1_3_1.lean @@ -1064,7 +1064,14 @@ lemma UnsignedSimpleFunction.integral_le_integral_of_aeLe {d:ℕ} {f g: Euclidea /-- Exercise 1.3.1(vi) (Compatibility with Lebesgue measure, indicator) -/ lemma UnsignedSimpleFunction.indicator {d:ℕ} {E: Set (EuclideanSpace' d)} (hE: LebesgueMeasurable E) : UnsignedSimpleFunction (Real.toEReal ∘ E.indicator') := by - sorry + use 1, fun _ => (1 : EReal), fun _ => E + constructor + · intro + exact ⟨hE, zero_le_one⟩ + · ext x + simp only [Function.comp_apply, Finset.sum_apply, Pi.smul_apply, smul_eq_mul] + rw [Fin.sum_univ_one] + simp [EReal.indicator, Real.EReal_fun] /-- Exercise 1.3.1(vi) (Compatibility with Lebesgue measure, integral of an indicator) -/ lemma UnsignedSimpleFunction.integral_indicator {d:ℕ} {E: Set (EuclideanSpace' d)} (hE: LebesgueMeasurable E) : From 9ddebf600a19f5297d071af194aeb2c01e0a04d1 Mon Sep 17 00:00:00 2001 From: Taksh Date: Tue, 8 Sep 2026 16:11:15 +0530 Subject: [PATCH 4/4] Fill that the unsigned simple integral of an indicator is Lebesgue measure. Well-definedness of the simple integral reduces this to a one-term sum. --- Analysis/MeasureTheory/Section_1_3_1.lean | 27 ++++++++++++++++++++--- 1 file changed, 24 insertions(+), 3 deletions(-) diff --git a/Analysis/MeasureTheory/Section_1_3_1.lean b/Analysis/MeasureTheory/Section_1_3_1.lean index a52f396c6..434df43f0 100644 --- a/Analysis/MeasureTheory/Section_1_3_1.lean +++ b/Analysis/MeasureTheory/Section_1_3_1.lean @@ -1076,7 +1076,14 @@ lemma UnsignedSimpleFunction.indicator {d:ℕ} {E: Set (EuclideanSpace' d)} (hE: /-- Exercise 1.3.1(vi) (Compatibility with Lebesgue measure, integral of an indicator) -/ lemma UnsignedSimpleFunction.integral_indicator {d:ℕ} {E: Set (EuclideanSpace' d)} (hE: LebesgueMeasurable E) : (UnsignedSimpleFunction.indicator hE).integ = Lebesgue_measure E := by - sorry + have hrep : Real.toEReal ∘ E.indicator' = + ∑ i : Fin 1, (1 : EReal) • EReal.indicator ((fun _ : Fin 1 => E) i) := by + ext x + simp only [Function.comp_apply, Finset.sum_apply, Pi.smul_apply, smul_eq_mul] + rw [Fin.sum_univ_one] + simp [EReal.indicator, Real.EReal_fun] + have h := integral_eq (indicator hE) (fun _ => hE) (fun _ => zero_le_one) hrep + simpa [Fin.sum_univ_one] using h lemma RealSimpleFunction.abs {d:ℕ} {f: EuclideanSpace' d → ℝ} (hf: RealSimpleFunction f) : UnsignedSimpleFunction (EReal.abs_fun f) := by sorry @@ -1308,11 +1315,25 @@ lemma ComplexSimpleFunction.integral_eq_integral_of_aeEqual {d:ℕ} {f g: Euclid /-- Exercise 1.3.2(iii) (Compatibility with Lebesgue measure, indicator) -/ lemma RealSimpleFunction.indicator {d:ℕ} {E: Set (EuclideanSpace' d)} (hE: LebesgueMeasurable E) : RealSimpleFunction (E.indicator') := by - sorry + use 1, fun _ => (1 : ℝ), fun _ => E + constructor + · intro + exact hE + · ext x + simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul] + rw [Fin.sum_univ_one] + simp lemma ComplexSimpleFunction.indicator {d:ℕ} {E: Set (EuclideanSpace' d)} (hE: LebesgueMeasurable E) : ComplexSimpleFunction (Complex.indicator E) := by - sorry + use 1, fun _ => (1 : ℂ), fun _ => E + constructor + · intro + exact hE + · ext x + simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul] + rw [Fin.sum_univ_one] + simp [Complex.indicator, Real.complex_fun] /-- Exercise 1.3.2(iii) (Compatibility with Lebesgue measure, integral of an indicator) -/ lemma RealSimpleFunction.integral_indicator {d:ℕ} {E: Set (EuclideanSpace' d)} (hE: LebesgueMeasurable E) (hfin: Lebesgue_measure E < ⊤): (RealSimpleFunction.indicator hE).integ = (Lebesgue_measure E).toReal := by