From 85d9916e7fac1e98b0be1dee6abe5b0607eba65b Mon Sep 17 00:00:00 2001 From: Taksh Date: Sat, 15 Aug 2026 09:30:03 +0530 Subject: [PATCH] fix: disambiguate duplicate Verso labels in MeasureTheory 1.2.2-1.4.3 Twenty-three docstrings across nine groups shared a label: Exercise 1.2.21, Definition 1.3.5, Exercises 1.3.1(i) and 1.3.1(vi), Definition 1.3.6, Exercises 1.3.2(i) and 1.3.2(iii), Example 1.4.3 and Example 1.4.21. Each label now names the declaration it sits on - almost always / almost everywhere equal / support, real vs complex, Lebesgue vs Jordan vs null vs elementary - keeping the statement number. --- Analysis/MeasureTheory/Section_1_2_2.lean | 4 ++-- Analysis/MeasureTheory/Section_1_3_1.lean | 28 +++++++++++------------ Analysis/MeasureTheory/Section_1_4_1.lean | 4 ++-- Analysis/MeasureTheory/Section_1_4_3.lean | 10 ++++---- 4 files changed, 23 insertions(+), 23 deletions(-) diff --git a/Analysis/MeasureTheory/Section_1_2_2.lean b/Analysis/MeasureTheory/Section_1_2_2.lean index 8a8ca3dab..72d2b56e1 100644 --- a/Analysis/MeasureTheory/Section_1_2_2.lean +++ b/Analysis/MeasureTheory/Section_1_2_2.lean @@ -1744,12 +1744,12 @@ theorem Lebesgue_measure.translate {d:ℕ} {E: Set (EuclideanSpace' d)} (x: Eucl (hE: LebesgueMeasurable E): Lebesgue_measure (E + {x}) = Lebesgue_measure E := by sorry -/-- Exercise 1.2.21 (Change of variables) -/ +/-- Exercise 1.2.21 (Change of variables, measurability) -/ lemma LebesgueMeasurable.linear {d:ℕ} (T: EuclideanSpace' d ≃ₗ[ℝ] EuclideanSpace' d) {E: Set (EuclideanSpace' d)} (hE: LebesgueMeasurable E): LebesgueMeasurable (T '' E) := by sorry -/-- Exercise 1.2.21 (Change of variables) -/ +/-- Exercise 1.2.21 (Change of variables, the measure scales by the determinant) -/ lemma Lebesgue_measure.linear {d:ℕ} (A: Matrix (Fin d) (Fin d) ℝ) [Invertible A] {E: Set (EuclideanSpace' d)} (hE: LebesgueMeasurable E): Lebesgue_measure (A.linear_equiv '' E) = |A.det| * Lebesgue_measure E := by sorry diff --git a/Analysis/MeasureTheory/Section_1_3_1.lean b/Analysis/MeasureTheory/Section_1_3_1.lean index 38cc4ca68..081c25343 100644 --- a/Analysis/MeasureTheory/Section_1_3_1.lean +++ b/Analysis/MeasureTheory/Section_1_3_1.lean @@ -819,15 +819,15 @@ lemma UnsignedSimpleFunction.integral_eq {d:ℕ} {f: EuclideanSpace' d → EReal simp only [UnsignedSimpleFunction.IntegralWellDef.weightedMeasureSum] at h exact h.symm -/-- Definition 1.3.5 -/ +/-- Definition 1.3.5 (almost always) -/ def AlmostAlways {d:ℕ} (P: EuclideanSpace' d → Prop) : Prop := IsNull { x | ¬ P x } -/-- Definition 1.3.5 -/ +/-- Definition 1.3.5 (almost everywhere equal) -/ def AlmostEverywhereEqual {d:ℕ} {X: Type*} (f g: EuclideanSpace' d → X) : Prop := AlmostAlways (fun x ↦ f x = g x) -/-- Definition 1.3.5 -/ +/-- Definition 1.3.5 (support) -/ def Support {X Y: Type*} [Zero Y] (f: X → Y) : Set X := { x | f x ≠ 0 } lemma UnsignedSimpleFunction.support_measurable {d:ℕ} {f: EuclideanSpace' d → EReal} (hf: UnsignedSimpleFunction f) : LebesgueMeasurable (Support f) := by @@ -1027,12 +1027,12 @@ theorem AlmostEverywhereEqual.equivalence {d:ℕ} {X: Type*} : Equivalence (@AlmostEverywhereEqual d X) := ⟨refl, symm, trans⟩ -/-- Exercise 1.3.1 (i) (Unsigned linearity) -/ +/-- Exercise 1.3.1 (i) (Unsigned linearity, sum) -/ lemma UnsignedSimpleFunction.integral_add {d:ℕ} {f g: EuclideanSpace' d → EReal} (hf: UnsignedSimpleFunction f) (hg: UnsignedSimpleFunction g) : (hf.add hg).integ = hf.integ + hg.integ := by sorry -/-- Exercise 1.3.1 (i) (Unsigned linearity) -/ +/-- Exercise 1.3.1 (i) (Unsigned linearity, scalar multiple) -/ lemma UnsignedSimpleFunction.integral_smul {d:ℕ} {f: EuclideanSpace' d → EReal} (hf: UnsignedSimpleFunction f) {c:EReal} (hc: c ≥ 0) : (hf.smul hc).integ = c * hf.integ := by sorry @@ -1059,12 +1059,12 @@ lemma UnsignedSimpleFunction.integral_le_integral_of_aeLe {d:ℕ} {f g: Euclidea hf.integ ≤ hg.integ := by sorry -/-- Exercise 1.3.1(vi) (Compatibility with Lebesgue measure) -/ +/-- 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 -/-- Exercise 1.3.1(vi) (Compatibility with Lebesgue measure) -/ +/-- 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 @@ -1075,11 +1075,11 @@ lemma RealSimpleFunction.abs {d:ℕ} {f: EuclideanSpace' d → ℝ} (hf: RealSim lemma ComplexSimpleFunction.abs {d:ℕ} {f: EuclideanSpace' d → ℂ} (hf: ComplexSimpleFunction f) : UnsignedSimpleFunction (EReal.abs_fun f) := by sorry -/-- Definition 1.3.6 (Absolutely convergent simple integral) -/ +/-- Definition 1.3.6 (Absolutely convergent simple integral, real) -/ def RealSimpleFunction.AbsolutelyIntegrable {d:ℕ} {f: EuclideanSpace' d → ℝ} (hf: RealSimpleFunction f) : Prop := (hf.abs).integ < ⊤ -/-- Definition 1.3.6 (Absolutely convergent simple integral) -/ +/-- Definition 1.3.6 (Absolutely convergent simple integral, complex) -/ def ComplexSimpleFunction.AbsolutelyIntegrable {d:ℕ} {f: EuclideanSpace' d → ℂ} (hf: ComplexSimpleFunction f) : Prop := (hf.abs).integ < ⊤ @@ -1272,20 +1272,20 @@ lemma ComplexSimpleFunction.AbsolutelyIntegrable.smul {d:ℕ} {f: EuclideanSpace lemma ComplexSimpleFunction.AbsolutelyIntegrable.conj {d:ℕ} {f: EuclideanSpace' d → ℂ} {hf: ComplexSimpleFunction f} (hf_integ: hf.AbsolutelyIntegrable) : (hf.conj).AbsolutelyIntegrable := by sorry -/-- Exercise 1.3.2 (i) ({lit}`*`-linearity) -/ +/-- Exercise 1.3.2 (i) ({lit}`*`-linearity, sum) -/ lemma RealSimpleFunction.integ_add {d:ℕ} {f g: EuclideanSpace' d → ℝ} {hf: RealSimpleFunction f} {hg: RealSimpleFunction g} (hf_integ: hf.AbsolutelyIntegrable) (hg_integ: hg.AbsolutelyIntegrable) : (hf.add hg).integ = hf.integ + hg.integ := by sorry lemma ComplexSimpleFunction.integ_add {d:ℕ} {f g: EuclideanSpace' d → ℂ} {hf: ComplexSimpleFunction f} {hg: ComplexSimpleFunction g} (hf_integ: hf.AbsolutelyIntegrable) (hg_integ: hg.AbsolutelyIntegrable) : (hf.add hg).integ = hf.integ + hg.integ := by sorry -/-- Exercise 1.3.2 (i) ({lit}`*`-linearity) -/ +/-- Exercise 1.3.2 (i) ({lit}`*`-linearity, scalar multiple) -/ lemma RealSimpleFunction.integ_smul {d:ℕ} {f: EuclideanSpace' d → ℝ} {hf: RealSimpleFunction f} (hf_integ: hf.AbsolutelyIntegrable) (a: ℝ) : (hf.smul a).integ = a * hf.integ := by sorry lemma ComplexSimpleFunction.integ_smul {d:ℕ} {f: EuclideanSpace' d → ℂ} {hf: ComplexSimpleFunction f} (hf_integ: hf.AbsolutelyIntegrable) (a: ℂ) : (hf.smul a).integ = a * hf.integ := by sorry -/-- Exercise 1.3.2 (i) ({lit}`*`-linearity) -/ +/-- Exercise 1.3.2 (i) ({lit}`*`-linearity, conjugation) -/ lemma ComplexSimpleFunction.integral_conj {d:ℕ} {f: EuclideanSpace' d → ℂ} {hf: ComplexSimpleFunction f} (hf_integ: hf.AbsolutelyIntegrable) : (hf.conj).integ = (starRingEnd ℂ) hf.integ := by sorry @@ -1296,7 +1296,7 @@ lemma RealSimpleFunction.integral_eq_integral_of_aeEqual {d:ℕ} {f g: Euclidean lemma ComplexSimpleFunction.integral_eq_integral_of_aeEqual {d:ℕ} {f g: EuclideanSpace' d → ℂ} {hf: ComplexSimpleFunction f} {hg: ComplexSimpleFunction g} (hf_integ: hf.AbsolutelyIntegrable) (hg_integ: hg.AbsolutelyIntegrable) (h_ae: AlmostEverywhereEqual f g) : hf.integ = hg.integ := by sorry -/-- Exercise 1.3.2(iii) (Compatibility with Lebesgue measure) -/ +/-- 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 @@ -1305,7 +1305,7 @@ lemma ComplexSimpleFunction.indicator {d:ℕ} {E: Set (EuclideanSpace' d)} (hE: ComplexSimpleFunction (Complex.indicator E) := by sorry -/-- Exercise 1.3.2(iii) (Compatibility with Lebesgue measure) -/ +/-- 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 sorry diff --git a/Analysis/MeasureTheory/Section_1_4_1.lean b/Analysis/MeasureTheory/Section_1_4_1.lean index cf4d5e96f..59bee3421 100644 --- a/Analysis/MeasureTheory/Section_1_4_1.lean +++ b/Analysis/MeasureTheory/Section_1_4_1.lean @@ -29,7 +29,7 @@ instance ConcreteBooleanAlgebra.instPartialOrder (X:Type*) : PartialOrder (Concr def ConcreteBooleanAlgebra.measurableSets {X:Type*} (B: ConcreteBooleanAlgebra X) : Set (Set X) := { E | B.measurable E } -/-- Example 1.4.3 -/ +/-- Example 1.4.3 (the largest algebra) -/ instance ConcreteBooleanAlgebra.instOrderTop {X:Type*} : OrderTop (ConcreteBooleanAlgebra X) := { top := { @@ -41,7 +41,7 @@ instance ConcreteBooleanAlgebra.instOrderTop {X:Type*} : OrderTop (ConcreteBoole le_top := sorry } -/-- Example 1.4.3 -/ +/-- Example 1.4.3 (the smallest algebra) -/ instance ConcreteBooleanAlgebra.instOrderBot {X:Type*} : OrderBot (ConcreteBooleanAlgebra X) := { bot := { diff --git a/Analysis/MeasureTheory/Section_1_4_3.lean b/Analysis/MeasureTheory/Section_1_4_3.lean index 0f797fa71..60d13f856 100644 --- a/Analysis/MeasureTheory/Section_1_4_3.lean +++ b/Analysis/MeasureTheory/Section_1_4_3.lean @@ -17,7 +17,7 @@ class FinitelyAdditiveMeasure {X:Type*} (B: ConcreteBooleanAlgebra X) where measure_finite_additive : ∀ E F : Set X, B.measurable E → B.measurable F → Disjoint E F → measure (E ∪ F) = measure E + measure F -/-- Example 1.4.21 -/ +/-- Example 1.4.21 (Lebesgue measure) -/ noncomputable def FinitelyAdditiveMeasure.lebesgue (d:ℕ) : FinitelyAdditiveMeasure (LebesgueMeasurable.boolean_algebra d) := { measure A := Lebesgue_measure A @@ -26,7 +26,7 @@ noncomputable def FinitelyAdditiveMeasure.lebesgue (d:ℕ) : FinitelyAdditiveMea measure_finite_additive := by sorry } -/-- Example 1.4.21 -/ +/-- Example 1.4.21 (restriction to a subalgebra) -/ def FinitelyAdditiveMeasure.restrict_alg {X:Type*} {B: ConcreteBooleanAlgebra X} (μ: FinitelyAdditiveMeasure B) {B':ConcreteBooleanAlgebra X} (hBB': B' ≤ B) : FinitelyAdditiveMeasure B' := { measure := μ.measure @@ -35,15 +35,15 @@ def FinitelyAdditiveMeasure.restrict_alg {X:Type*} {B: ConcreteBooleanAlgebra X} measure_finite_additive := by sorry } -/-- Example 1.4.21 -/ +/-- Example 1.4.21 (Jordan measure) -/ noncomputable def FinitelyAdditiveMeasure.jordan (d:ℕ) : FinitelyAdditiveMeasure (JordanMeasurable.boolean_algebra d) := (FinitelyAdditiveMeasure.lebesgue d).restrict_alg (LebesgueMeasurable.gt_jordan_boolean_algebra d) -/-- Example 1.4.21 -/ +/-- Example 1.4.21 (null sets) -/ noncomputable def FinitelyAdditiveMeasure.null (d:ℕ) : FinitelyAdditiveMeasure (IsNull.boolean_algebra d) := (FinitelyAdditiveMeasure.lebesgue d).restrict_alg (IsNull.lt_lebesgue_boolean_algebra d) -/-- Example 1.4.21 -/ +/-- Example 1.4.21 (elementary sets) -/ noncomputable def FinitelyAdditiveMeasure.elem (d:ℕ) : FinitelyAdditiveMeasure (EuclideanSpace'.elementary_boolean_algebra d) := (FinitelyAdditiveMeasure.lebesgue d).restrict_alg (by sorry)