From aabb68aae44a0f265af0ac7b01c0e340f1f387a0 Mon Sep 17 00:00:00 2001 From: Stefano Rocca Date: Tue, 25 Nov 2025 20:08:01 +0100 Subject: [PATCH 1/3] =?UTF-8?q?feat(MeasureTheory\Group\Action):=20add=20l?= =?UTF-8?q?emmas=20=CE=BC(c=20=E2=8B=85=20s=20=E2=88=A9=20t)=20=3D=20?= =?UTF-8?q?=CE=BC(s=20=E2=88=A9=20c=E2=81=BB=C2=B9=20=E2=8B=85=20t)=20and?= =?UTF-8?q?=20similar?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib/MeasureTheory/Group/Action.lean | 34 ++++++++++++++++++++++++- 1 file changed, 33 insertions(+), 1 deletion(-) diff --git a/Mathlib/MeasureTheory/Group/Action.lean b/Mathlib/MeasureTheory/Group/Action.lean index f4119cdeb5daa9..2d6f83a6e529a5 100644 --- a/Mathlib/MeasureTheory/Group/Action.lean +++ b/Mathlib/MeasureTheory/Group/Action.lean @@ -25,7 +25,7 @@ some basic properties of such measures. @[expose] public section -open scoped ENNReal NNReal Pointwise Topology +open scoped ENNReal NNReal Pointwise Topology symmDiff open MeasureTheory.Measure Set Function Filter namespace MeasureTheory @@ -105,6 +105,38 @@ theorem measure_preimage_smul (c : G) (s : Set α) : μ ((c • ·) ⁻¹' s) = theorem measure_smul (c : G) (s : Set α) : μ (c • s) = μ s := by simpa only [preimage_smul_inv] using measure_preimage_smul μ c⁻¹ s +@[to_additive] +theorem measure_smul_inter (c : G) (s t : Set α) : μ (c • s ∩ t) = μ (s ∩ c⁻¹ • t) := by + rw[← measure_smul _ c (s ∩ c⁻¹ • t), smul_set_inter, smul_smul, mul_inv_cancel, one_smul] + +@[to_additive] +theorem measure_inter_smul (c : G) (s t : Set α) : μ (s ∩ c • t) = μ (c⁻¹ • s ∩ t) := by + simp [measure_smul_inter] + +@[to_additive] +theorem measure_smul_union (c : G) (s t : Set α) : μ (c • s ∪ t) = μ (s ∪ c⁻¹ • t) := by + rw[← measure_smul _ c (s ∪ c⁻¹ • t), smul_set_union, smul_smul, mul_inv_cancel, one_smul] + +@[to_additive] +theorem measure_union_smul (c : G) (s t : Set α) : μ (s ∪ c • t) = μ (c⁻¹ • s ∪ t) := by + simp [measure_smul_union] + +@[to_additive] +theorem measure_smul_sdiff (c : G) (s t : Set α) : μ (c • s \ t) = μ (s \ c⁻¹ • t) := by + rw[← measure_smul _ c (s \ c⁻¹ • t), smul_set_sdiff, smul_smul, mul_inv_cancel, one_smul] + +@[to_additive] +theorem measure_sdiff_smul (c : G) (s t : Set α) : μ (s \ c • t) = μ (c⁻¹ • s \ t) := by + simp [measure_smul_sdiff] + +@[to_additive] +theorem measure_smul_symmDiff (c : G) (s t : Set α) : μ ((c • s) ∆ t) = μ (s ∆ (c⁻¹ • t)) := by + rw[← measure_smul _ c (s ∆ (c⁻¹ • t)), smul_set_symmDiff, smul_smul, mul_inv_cancel, one_smul] + +@[to_additive] +theorem measure_symmDiff_smul (c : G) (s t : Set α) : μ (s ∆ (c • t)) = μ ((c⁻¹ • s) ∆ t) := by + simp [measure_smul_symmDiff] + variable {μ} @[to_additive] From 17084d501156ea1ab41fc94c586557c8b66ac96b Mon Sep 17 00:00:00 2001 From: Stefano Rocca Date: Thu, 27 Nov 2025 19:01:31 +0100 Subject: [PATCH 2/3] fixes & simp lemmas --- Mathlib/MeasureTheory/Group/Action.lean | 48 ++++++++++++------------- 1 file changed, 24 insertions(+), 24 deletions(-) diff --git a/Mathlib/MeasureTheory/Group/Action.lean b/Mathlib/MeasureTheory/Group/Action.lean index 2d6f83a6e529a5..b5f9b70e36f1ea 100644 --- a/Mathlib/MeasureTheory/Group/Action.lean +++ b/Mathlib/MeasureTheory/Group/Action.lean @@ -105,37 +105,37 @@ theorem measure_preimage_smul (c : G) (s : Set α) : μ ((c • ·) ⁻¹' s) = theorem measure_smul (c : G) (s : Set α) : μ (c • s) = μ s := by simpa only [preimage_smul_inv] using measure_preimage_smul μ c⁻¹ s -@[to_additive] -theorem measure_smul_inter (c : G) (s t : Set α) : μ (c • s ∩ t) = μ (s ∩ c⁻¹ • t) := by - rw[← measure_smul _ c (s ∩ c⁻¹ • t), smul_set_inter, smul_smul, mul_inv_cancel, one_smul] +@[to_additive (attr := simp)] +theorem measure_smul_inter (c : G) (s t : Set α) : μ (s ∩ c⁻¹ • t) = μ (c • s ∩ t) := by + rw [← measure_smul _ c, smul_set_inter, smul_smul, mul_inv_cancel, one_smul] -@[to_additive] -theorem measure_inter_smul (c : G) (s t : Set α) : μ (s ∩ c • t) = μ (c⁻¹ • s ∩ t) := by - simp [measure_smul_inter] +@[to_additive (attr := simp)] +theorem measure_inter_smul (c : G) (s t : Set α) : μ (c⁻¹ • s ∩ t) = μ (s ∩ c • t) := by + simpa [inv_inv] using (measure_smul_inter _ c⁻¹ _ _).symm -@[to_additive] -theorem measure_smul_union (c : G) (s t : Set α) : μ (c • s ∪ t) = μ (s ∪ c⁻¹ • t) := by - rw[← measure_smul _ c (s ∪ c⁻¹ • t), smul_set_union, smul_smul, mul_inv_cancel, one_smul] +@[to_additive (attr := simp)] +theorem measure_smul_union (c : G) (s t : Set α) : μ (s ∪ c⁻¹ • t) = μ (c • s ∪ t) := by + rw [← measure_smul _ c, smul_set_union, smul_smul, mul_inv_cancel, one_smul] -@[to_additive] -theorem measure_union_smul (c : G) (s t : Set α) : μ (s ∪ c • t) = μ (c⁻¹ • s ∪ t) := by - simp [measure_smul_union] +@[to_additive (attr := simp)] +theorem measure_union_smul (c : G) (s t : Set α) : μ (c⁻¹ • s ∪ t) = μ (s ∪ c • t) := by + simpa [inv_inv] using (measure_smul_union _ c⁻¹ _ _).symm -@[to_additive] -theorem measure_smul_sdiff (c : G) (s t : Set α) : μ (c • s \ t) = μ (s \ c⁻¹ • t) := by - rw[← measure_smul _ c (s \ c⁻¹ • t), smul_set_sdiff, smul_smul, mul_inv_cancel, one_smul] +@[to_additive (attr := simp)] +theorem measure_smul_sdiff (c : G) (s t : Set α) : μ (s \ c⁻¹ • t) = μ (c • s \ t) := by + rw [← measure_smul _ c, smul_set_sdiff, smul_smul, mul_inv_cancel, one_smul] -@[to_additive] -theorem measure_sdiff_smul (c : G) (s t : Set α) : μ (s \ c • t) = μ (c⁻¹ • s \ t) := by - simp [measure_smul_sdiff] +@[to_additive (attr := simp)] +theorem measure_sdiff_smul (c : G) (s t : Set α) : μ (c⁻¹ • s \ t) = μ (s \ c • t) := by + simpa [inv_inv] using (measure_smul_sdiff _ c⁻¹ _ _).symm -@[to_additive] -theorem measure_smul_symmDiff (c : G) (s t : Set α) : μ ((c • s) ∆ t) = μ (s ∆ (c⁻¹ • t)) := by - rw[← measure_smul _ c (s ∆ (c⁻¹ • t)), smul_set_symmDiff, smul_smul, mul_inv_cancel, one_smul] +@[to_additive (attr := simp)] +theorem measure_smul_symmDiff (c : G) (s t : Set α) : μ (s ∆ (c⁻¹ • t)) = μ ((c • s) ∆ t) := by + rw [← measure_smul _ c, smul_set_symmDiff, smul_smul, mul_inv_cancel, one_smul] -@[to_additive] -theorem measure_symmDiff_smul (c : G) (s t : Set α) : μ (s ∆ (c • t)) = μ ((c⁻¹ • s) ∆ t) := by - simp [measure_smul_symmDiff] +@[to_additive (attr := simp)] +theorem measure_symmDiff_smul (c : G) (s t : Set α) : μ ((c⁻¹ • s) ∆ t) = μ (s ∆ (c • t)) := by + simpa [inv_inv] using (measure_smul_symmDiff _ c⁻¹ _ _).symm variable {μ} From a19cba43e5e6c539753c8c13f8ba3509fca47e08 Mon Sep 17 00:00:00 2001 From: Stefano Rocca Date: Thu, 27 Nov 2025 19:22:40 +0100 Subject: [PATCH 3/3] adding inv to lemmas name --- Mathlib/MeasureTheory/Group/Action.lean | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/Mathlib/MeasureTheory/Group/Action.lean b/Mathlib/MeasureTheory/Group/Action.lean index b5f9b70e36f1ea..320c9ad6429ba4 100644 --- a/Mathlib/MeasureTheory/Group/Action.lean +++ b/Mathlib/MeasureTheory/Group/Action.lean @@ -106,36 +106,36 @@ theorem measure_smul (c : G) (s : Set α) : μ (c • s) = μ s := by simpa only [preimage_smul_inv] using measure_preimage_smul μ c⁻¹ s @[to_additive (attr := simp)] -theorem measure_smul_inter (c : G) (s t : Set α) : μ (s ∩ c⁻¹ • t) = μ (c • s ∩ t) := by +theorem measure_inter_inv_smul (c : G) (s t : Set α) : μ (s ∩ c⁻¹ • t) = μ (c • s ∩ t) := by rw [← measure_smul _ c, smul_set_inter, smul_smul, mul_inv_cancel, one_smul] @[to_additive (attr := simp)] -theorem measure_inter_smul (c : G) (s t : Set α) : μ (c⁻¹ • s ∩ t) = μ (s ∩ c • t) := by - simpa [inv_inv] using (measure_smul_inter _ c⁻¹ _ _).symm +theorem measure_inv_smul_inter (c : G) (s t : Set α) : μ (c⁻¹ • s ∩ t) = μ (s ∩ c • t) := by + simpa [inv_inv] using (measure_inter_inv_smul _ c⁻¹ _ _).symm @[to_additive (attr := simp)] -theorem measure_smul_union (c : G) (s t : Set α) : μ (s ∪ c⁻¹ • t) = μ (c • s ∪ t) := by +theorem measure_union_inv_smul (c : G) (s t : Set α) : μ (s ∪ c⁻¹ • t) = μ (c • s ∪ t) := by rw [← measure_smul _ c, smul_set_union, smul_smul, mul_inv_cancel, one_smul] @[to_additive (attr := simp)] -theorem measure_union_smul (c : G) (s t : Set α) : μ (c⁻¹ • s ∪ t) = μ (s ∪ c • t) := by - simpa [inv_inv] using (measure_smul_union _ c⁻¹ _ _).symm +theorem measure_inv_smul_union (c : G) (s t : Set α) : μ (c⁻¹ • s ∪ t) = μ (s ∪ c • t) := by + simpa [inv_inv] using (measure_union_inv_smul _ c⁻¹ _ _).symm @[to_additive (attr := simp)] -theorem measure_smul_sdiff (c : G) (s t : Set α) : μ (s \ c⁻¹ • t) = μ (c • s \ t) := by +theorem measure_sdiff_inv_smul (c : G) (s t : Set α) : μ (s \ c⁻¹ • t) = μ (c • s \ t) := by rw [← measure_smul _ c, smul_set_sdiff, smul_smul, mul_inv_cancel, one_smul] @[to_additive (attr := simp)] -theorem measure_sdiff_smul (c : G) (s t : Set α) : μ (c⁻¹ • s \ t) = μ (s \ c • t) := by - simpa [inv_inv] using (measure_smul_sdiff _ c⁻¹ _ _).symm +theorem measure_inv_smul_sdiff (c : G) (s t : Set α) : μ (c⁻¹ • s \ t) = μ (s \ c • t) := by + simpa [inv_inv] using (measure_sdiff_inv_smul _ c⁻¹ _ _).symm @[to_additive (attr := simp)] -theorem measure_smul_symmDiff (c : G) (s t : Set α) : μ (s ∆ (c⁻¹ • t)) = μ ((c • s) ∆ t) := by +theorem measure_symmDiff_inv_smul (c : G) (s t : Set α) : μ (s ∆ (c⁻¹ • t)) = μ ((c • s) ∆ t) := by rw [← measure_smul _ c, smul_set_symmDiff, smul_smul, mul_inv_cancel, one_smul] @[to_additive (attr := simp)] -theorem measure_symmDiff_smul (c : G) (s t : Set α) : μ ((c⁻¹ • s) ∆ t) = μ (s ∆ (c • t)) := by - simpa [inv_inv] using (measure_smul_symmDiff _ c⁻¹ _ _).symm +theorem measure_inv_smul_symmDiff (c : G) (s t : Set α) : μ ((c⁻¹ • s) ∆ t) = μ (s ∆ (c • t)) := by + simpa [inv_inv] using (measure_symmDiff_inv_smul _ c⁻¹ _ _).symm variable {μ}