From d774f908210e913098de220c43d3132d47fb67a7 Mon Sep 17 00:00:00 2001 From: Taksh Date: Fri, 7 Aug 2026 20:45:25 +0530 Subject: [PATCH] fix: restore determinant scaling factor to measure_linear Exercise 1.1.11(2) states the linear image measure scales by D (the witness the statement itself introduces), matching measure_linear_of_elem and measure_linear_det right below it, plus the doc comment. As written the RHS dropped D entirely, i.e. claimed linear maps preserve Jordan measure exactly, which is false (e.g. x -> 2x doubles the measure of [0,1]). --- Analysis/MeasureTheory/Section_1_1_2.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Analysis/MeasureTheory/Section_1_1_2.lean b/Analysis/MeasureTheory/Section_1_1_2.lean index 0b5ae5ef..d13a3dba 100644 --- a/Analysis/MeasureTheory/Section_1_1_2.lean +++ b/Analysis/MeasureTheory/Section_1_1_2.lean @@ -735,7 +735,7 @@ lemma JordanMeasurable.linear {d:ℕ} (T: EuclideanSpace' d ≃ₗ[ℝ] Euclidea /-- Exercise 1.1.11 (2) -/ -- The measure of a linear image of a Jordan measurable set equals the original measure (up to determinant scaling). lemma JordanMeasurable.measure_linear {d:ℕ} (T: EuclideanSpace' d ≃ₗ[ℝ] EuclideanSpace' d) : -∃ D > 0, ∀ (E: Set (EuclideanSpace' d)) (hE: JordanMeasurable E), (linear T hE).measure = hE.measure := by sorry +∃ D > 0, ∀ (E: Set (EuclideanSpace' d)) (hE: JordanMeasurable E), (linear T hE).measure = D * hE.measure := by sorry /-- An invertible matrix defines a linear equivalence on Euclidean space. -/ noncomputable def Matrix.linear_equiv {d:ℕ} (A: Matrix (Fin d) (Fin d) ℝ) [Invertible A] :