chore: rename modularHaarChar to distribHaarChar

FLT/FLT_files.lean

@@ -7,15 +7,15 @@ import FLT.DivisionAlgebra.Finiteness
 import FLT.EllipticCurve.Torsion
 import FLT.ForMathlib.ActionTopology
 import FLT.ForMathlib.Algebra
+import FLT.ForMathlib.DomMulActMeasure
 import FLT.ForMathlib.MiscLemmas
 import FLT.FromMathlib.Algebra
 import FLT.GaloisRepresentation.Cyclotomic
 import FLT.GaloisRepresentation.HardlyRamified
 import FLT.GlobalLanglandsConjectures.GLnDefs
 import FLT.GlobalLanglandsConjectures.GLzero
 import FLT.GroupScheme.FiniteFlat
-import FLT.HaarMeasure.Map
-import FLT.HaarMeasure.ModularCharacter
+import FLT.HaarMeasure.DistribHaarChar
 import FLT.Hard.Results
 import FLT.HIMExperiments.flatness
 import FLT.MathlibExperiments.Coalgebra.Monoid

FLT/HaarMeasure/ModularCharacter.lean → FLT/ForMathlib/DomMulActMeasure.lean

@@ -12,8 +12,8 @@ namespace MeasureTheory.Measure
 variable {G A : Type*} [Group G] [AddCommGroup A] [DistribMulAction G A]
   [MeasurableSpace A]
   [MeasurableSpace G] -- not needed actually
-  [MeasurableSMul G A] -- only need `MeasurableConstSMul` but we don't have this class.
-variable (μ ν : Measure A)
+  [MeasurableSMul G A] -- We only need `MeasurableConstSMul` but we don't have this class.
+variable {μ ν : Measure A} {g : G}
 
 noncomputable
 instance : DistribMulAction Gᵈᵐᵃ (Measure A) where
@@ -33,7 +33,7 @@ instance : DistribMulAction Gᵈᵐᵃ (Measure A) where
     rw [Measure.map_add]
     exact measurable_const_smul ..
 
-lemma dma_smul_apply (g : Gᵈᵐᵃ) (s : Set A) :
+lemma dma_smul_apply (μ : Measure A) (g : Gᵈᵐᵃ) (s : Set A) :
     (g • μ) s = μ ((DomMulAct.mk.symm g) • s) := by
   refine ((MeasurableEquiv.smul ((DomMulAct.mk.symm g : G)⁻¹)).map_apply _).trans ?_
   congr 1
@@ -47,9 +47,7 @@ variable [TopologicalSpace A] [BorelSpace A] [TopologicalAddGroup A] [LocallyCom
   [ContinuousConstSMul G A] [μ.IsAddHaarMeasure] [ν.IsAddHaarMeasure]
 
 instance : SMulCommClass ℝ≥0 Gᵈᵐᵃ (Measure A) where
-  smul_comm r g μ := by
-    show r • μ.map _ = (r • μ).map _
-    simp
+  smul_comm r g μ := show r • μ.map _ = (r • μ).map _ by simp
 
 instance : SMulCommClass Gᵈᵐᵃ ℝ≥0 (Measure A) := .symm ..
 
@@ -60,6 +58,7 @@ instance (g : Gᵈᵐᵃ) : (g • μ).IsAddHaarMeasure :=
   (DistribMulAction.toAddEquiv _ (DomMulAct.mk.symm g⁻¹)).isAddHaarMeasure_map _
     (continuous_const_smul _) (continuous_const_smul _)
 
+variable (μ ν) in
 lemma addHaarScalarFactor_dma_smul (g : Gᵈᵐᵃ) :
     addHaarScalarFactor (g • μ) (g • ν) = addHaarScalarFactor μ ν := by
   obtain ⟨⟨f, f_cont⟩, f_comp, f_nonneg, f_zero⟩ :
@@ -74,44 +73,8 @@ lemma addHaarScalarFactor_dma_smul (g : Gᵈᵐᵃ) :
   · rw [← integral_dma_smul]
     exact (f_cont.integral_pos_of_hasCompactSupport_nonneg_nonzero f_comp f_nonneg f_zero).ne'
 
+variable (μ) in
 lemma addHaarScalarFactor_smul_congr (g : Gᵈᵐᵃ) :
     addHaarScalarFactor μ (g • μ) = addHaarScalarFactor ν (g • ν) := by
   rw [addHaarScalarFactor_eq_mul _ (g • ν), addHaarScalarFactor_dma_smul,
     mul_comm, ← addHaarScalarFactor_eq_mul]
-
-variable (A) in
-@[simps (config := .lemmasOnly)]
-noncomputable def modularHaarChar : G →* ℝ≥0 where
-  toFun g := addHaarScalarFactor (addHaar (G := A)) (DomMulAct.mk g • addHaar)
-  map_one' := by simp
-  map_mul' g g' := by
-    simp
-    rw [addHaarScalarFactor_eq_mul _ (DomMulAct.mk g • addHaar (G := A))]
-    congr 1
-    simp_rw [mul_smul]
-    exact addHaarScalarFactor_smul_congr ..
-
-lemma addHaarScalarFactor_smul_eq_modularHaarChar (g : G) :
-  addHaarScalarFactor μ (DomMulAct.mk g • μ) = modularHaarChar A g :=
-  addHaarScalarFactor_smul_congr ..
-
-lemma addHaarScalarFactor_smul_inv_eq_modularHaarChar (g : G) :
-    addHaarScalarFactor ((DomMulAct.mk g)⁻¹ • μ) μ = modularHaarChar A g := by
-  rw [← addHaarScalarFactor_dma_smul _ _ (DomMulAct.mk g)]
-  simp_rw [← mul_smul, mul_inv_cancel, one_smul]
-  exact addHaarScalarFactor_smul_eq_modularHaarChar ..
-
-lemma addHaarScalarFactor_smul_eq_modularHaarChar_inv (g : G) :
-    addHaarScalarFactor (DomMulAct.mk g • μ) μ = (modularHaarChar A g)⁻¹ := by
-  rw [← map_inv, ← addHaarScalarFactor_smul_inv_eq_modularHaarChar μ, DomMulAct.mk_inv, inv_inv]
-
-variable (A) in
-lemma modularHaarChar_pos (g : G) : 0 < modularHaarChar A g :=
-  pos_iff_ne_zero.mpr ((Group.isUnit g).map (modularHaarChar A)).ne_zero
-
-lemma modularHaarChar_smul [IsFiniteMeasureOnCompacts μ] [Regular μ] (g : G) {s : Set A} :
-    modularHaarChar A g • μ s = μ (g⁻¹ • s) := by
-  have : (DomMulAct.mk g⁻¹ • μ) s = μ (g⁻¹ • s) := by simp [dma_smul_apply]
-  rw [eq_comm, ← inv_smul_eq_iff₀ (modularHaarChar_pos A g).ne', ← map_inv,
-    ← addHaarScalarFactor_smul_eq_modularHaarChar μ,
-    ← this, ← smul_apply, ← isAddLeftInvariant_eq_smul_of_regular μ (DomMulAct.mk g⁻¹ • μ)]

FLT/HaarMeasure/DistribHaarChar.lean

@@ -0,0 +1,80 @@
+/-
+Copyright (c) 2024 Andrew Yang, Yaël Dillies, Javier López-Contreras. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang, Yaël Dillies, Javier López-Contreras
+-/
+import FLT.Mathlib.Data.ENNReal.Inv
+import FLT.ForMathlib.DomMulActMeasure
+
+/-!
+# The distributive character of Haar measures
+
+Given a group `G` acting on an measurable additive commutative group `A`, and an element `g : G`,
+one can pull back the Haar measure `μ` of `A` along the map `(g • ·) : A → A` to get another Haar
+measure `μ'` on `A`. By unicity of Haar measures, there exists some nonnegative real number `r` such
+that `μ' = r • μ`. We can thus define a map `distribHaarChar : G → ℝ≥0` sending `g` to its
+associated real number `r`. Furthermore, this number doesn't depend on the Haar measure `μ` we
+started with, and `distribHaarChar` is a group homomorphism.
+
+## See also
+
+[Zulip](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/canonical.20norm.20coming.20from.20Haar.20measure/near/480050592)
+-/
+
+open scoped NNReal Pointwise ENNReal
+
+namespace MeasureTheory.Measure
+
+variable {G A : Type*} [Group G] [AddCommGroup A] [DistribMulAction G A]
+  [MeasurableSpace A]
+  [MeasurableSpace G] -- not needed actually
+  [MeasurableSMul G A] -- only need `MeasurableConstSMul` but we don't have this class.
+variable {μ ν : Measure A} {g : G}
+
+variable [TopologicalSpace A] [BorelSpace A] [TopologicalAddGroup A] [LocallyCompactSpace A]
+  [ContinuousConstSMul G A] [μ.IsAddHaarMeasure] [ν.IsAddHaarMeasure]
+
+variable (μ A) in
+@[simps (config := .lemmasOnly)]
+noncomputable def distribHaarChar : G →* ℝ≥0 where
+  toFun g := addHaarScalarFactor (addHaar (G := A)) (DomMulAct.mk g • addHaar)
+  map_one' := by simp
+  map_mul' g g' := by
+    simp
+    rw [addHaarScalarFactor_eq_mul _ (DomMulAct.mk g • addHaar (G := A))]
+    congr 1
+    simp_rw [mul_smul]
+    exact addHaarScalarFactor_smul_congr ..
+
+variable (μ) in
+lemma addHaarScalarFactor_smul_eq_distribHaarChar (g : G) :
+    addHaarScalarFactor μ (DomMulAct.mk g • μ) = distribHaarChar A g :=
+  addHaarScalarFactor_smul_congr ..
+
+variable (μ) in
+lemma addHaarScalarFactor_smul_inv_eq_distribHaarChar (g : G) :
+    addHaarScalarFactor ((DomMulAct.mk g)⁻¹ • μ) μ = distribHaarChar A g := by
+  rw [← addHaarScalarFactor_dma_smul _ _ (DomMulAct.mk g)]
+  simp_rw [← mul_smul, mul_inv_cancel, one_smul]
+  exact addHaarScalarFactor_smul_eq_distribHaarChar ..
+
+variable (μ) in
+lemma addHaarScalarFactor_smul_eq_distribHaarChar_inv (g : G) :
+    addHaarScalarFactor (DomMulAct.mk g • μ) μ = (distribHaarChar A g)⁻¹ := by
+  rw [← map_inv, ← addHaarScalarFactor_smul_inv_eq_distribHaarChar μ, DomMulAct.mk_inv, inv_inv]
+
+lemma distribHaarChar_pos : 0 < distribHaarChar A g :=
+  pos_iff_ne_zero.mpr ((Group.isUnit g).map (distribHaarChar A)).ne_zero
+
+variable [IsFiniteMeasureOnCompacts μ] [Regular μ] {s : Set A}
+
+variable (μ) in
+lemma distribHaarChar_mul (g : G) (s : Set A) : distribHaarChar A g * μ s = μ (g⁻¹ • s) := by
+  have : (DomMulAct.mk g⁻¹ • μ) s = μ (g⁻¹ • s) := by simp [dma_smul_apply]
+  rw [eq_comm, ← nnreal_smul_coe_apply, ← inv_smul_eq_iff₀ distribHaarChar_pos.ne', ← map_inv,
+    ← addHaarScalarFactor_smul_eq_distribHaarChar μ,
+    ← this, ← smul_apply, ← isAddLeftInvariant_eq_smul_of_regular μ (DomMulAct.mk g⁻¹ • μ)]
+
+lemma distribHaarChar_eq_div (hs₀ : μ s ≠ 0) (hs : μ s ≠ ∞) (g : G) :
+    distribHaarChar A g = μ (g⁻¹ • s) / μ s := by
+  rw [← distribHaarChar_mul, ENNReal.mul_div_cancel_right hs₀ hs]

FLT/Mathlib/Data/ENNReal/Inv.lean

@@ -0,0 +1,8 @@
+import Mathlib.Data.ENNReal.Inv
+
+namespace ENNReal
+
+protected lemma mul_div_cancel_right {b : ℝ≥0∞} (hb₀ : b ≠ 0) (hb : b ≠ ∞) (a : ℝ≥0∞) :
+    a * b / b = a := by rw [ENNReal.mul_div_right_comm, ENNReal.div_mul_cancel hb₀ hb]
+
+end ENNReal