chore: fix sign in DistribHaarChar (#274)

#223 made me realise that the definition of  `DistribHaarChar` was off by a "multiplicative sign" i.e. an inverse (for example `lemma distribHaarChar_real (x : ℝˣ) : distribHaarChar ℝ x = ‖(x : ℝ)‖₊⁻¹ := ...` is proved in that PR, which was not what was supposed to happen) . The sign in the Lean currently doesn't agree with the sign in the docstring or the sign in the associated Zulip discussion. This PR changes the definition to make it correct.

FLT/ForMathlib/DomMulActMeasure.lean

@@ -78,3 +78,9 @@ 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 (μ) 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]

FLT/HaarMeasure/DistribHaarChar.lean

@@ -37,30 +37,32 @@ variable [TopologicalSpace A] [BorelSpace A] [TopologicalAddGroup A] [LocallyCom
 variable (μ A) in
 @[simps (config := .lemmasOnly)]
 noncomputable def distribHaarChar : G →* ℝ≥0 where
-  toFun g := addHaarScalarFactor (addHaar (G := A)) (DomMulAct.mk g • addHaar)
+  toFun g := addHaarScalarFactor (DomMulAct.mk g • addHaar) (addHaar (G := A))
   map_one' := by simp
   map_mul' g g' := by
-    simp
-    rw [addHaarScalarFactor_eq_mul _ (DomMulAct.mk g • addHaar (G := A))]
+    simp_rw [DomMulAct.mk_mul]
+    rw [addHaarScalarFactor_eq_mul _ (DomMulAct.mk g' • addHaar (G := A))]
     congr 1
     simp_rw [mul_smul]
-    exact addHaarScalarFactor_smul_congr ..
+    rw [addHaarScalarFactor_dma_smul]
 
 variable (μ) in
 lemma addHaarScalarFactor_smul_eq_distribHaarChar (g : G) :
-    addHaarScalarFactor μ (DomMulAct.mk g • μ) = distribHaarChar A g :=
-  addHaarScalarFactor_smul_congr ..
+    addHaarScalarFactor (DomMulAct.mk g • μ) μ = distribHaarChar A g := by
+  unfold distribHaarChar
+  dsimp
+  exact addHaarScalarFactor_smul_congr' ..
 
 variable (μ) in
 lemma addHaarScalarFactor_smul_inv_eq_distribHaarChar (g : G) :
-    addHaarScalarFactor ((DomMulAct.mk g)⁻¹ • μ) μ = distribHaarChar A g := by
+    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
+    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 :=
@@ -69,12 +71,13 @@ lemma distribHaarChar_pos : 0 < distribHaarChar A g :=
 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⁻¹ • μ)]
+omit [IsFiniteMeasureOnCompacts μ] 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, ← addHaarScalarFactor_smul_eq_distribHaarChar μ,
+    ← this, ← smul_apply, ← isAddLeftInvariant_eq_smul_of_regular]
 
+omit [IsFiniteMeasureOnCompacts μ] in
 lemma distribHaarChar_eq_div (hs₀ : μ s ≠ 0) (hs : μ s ≠ ∞) (g : G) :
-    distribHaarChar A g = μ (g⁻¹ • s) / μ s := by
+    distribHaarChar A g = μ (g • s) / μ s := by
   rw [← distribHaarChar_mul, ENNReal.mul_div_cancel_right hs₀ hs]