bump

FLT/HaarMeasure/ConcreteCharCalculations.lean

@@ -1,35 +1,24 @@
-import Mathlib.Analysis.Complex.ReImTopology
-import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
-import Mathlib.RingTheory.Complex
 import FLT.ForMathlib.MeasurableSpacePadics
 import FLT.HaarMeasure.DistribHaarChar
 import FLT.Mathlib.Analysis.Complex.Basic
 import FLT.Mathlib.Data.Complex.Basic
-import FLT.Mathlib.LinearAlgebra.Determinant
-import FLT.Mathlib.RingTheory.Norm.Defs
+import Mathlib.Analysis.Complex.ReImTopology
+import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
 
 open Real Complex Padic MeasureTheory Measure NNReal Set TopologicalSpace
 open scoped Pointwise ENNReal
 open TopologicalRing
 
 
 lemma distribHaarChar_complex (z : ℂˣ) : distribHaarChar ℂ z = ‖(z : ℂ)‖₊ ^ (-2 : ℤ) := by
+  -- Use the (0, 1) + i(0, 1) open
   refine distribHaarChar_eq_of_measure_smul_eq_mul (s := Icc 0 1 ×ℂ Icc 0 1) (μ := volume)
     (measure_pos_of_nonempty_interior _ <| by simp [interior_reProdIm]).ne'
     (isCompact_Icc.reProdIm isCompact_Icc).measure_ne_top ?_
-  have key : ((LinearMap.mul ℂ ℂ z).restrictScalars ℝ).det = ‖z.val‖₊ ^ 2 := by
-    refine Complex.ofReal_injective ?_
-    rw [LinearMap.det_restrictScalars]
-    simp [Algebra.norm_complex_apply, normSq_eq_norm_sq, zpow_ofNat]
-  have := addHaar_preimage_linearMap (E := ℂ) volume
-    (f := (LinearMap.mul ℂ ℂ z).restrictScalars ℝ)
-  simp [key] at this
-  convert this _ using 2
-  · symm
-    exact Set.preimage_smul z _
-  · simp [← Real.ennnorm_eq_ofReal_abs, ← Complex.norm_eq_abs, zpow_ofNat]
+  sorry
 
 lemma distribHaarChar_real (x : ℝˣ) : distribHaarChar ℝ x = ‖(x : ℝ)‖₊⁻¹ := by
+  let K : Set ℝ := Icc 0 1
   refine distribHaarChar_eq_of_measure_smul_eq_mul (s := Icc 0 1) (μ := volume)
     (measure_pos_of_nonempty_interior _ <| by simp).ne' isCompact_Icc.measure_ne_top ?_
   rw [Units.smul_def, Measure.addHaar_smul]
@@ -49,16 +38,17 @@ lemma volume_smul_integral (x : ℤ_[p]ˣ): volume (AddSubgroup.closure {x.1}).c
 
 lemma volume_smul (x : ℚ_[p]ˣ): volume (AddSubgroup.closure {x.1}).carrier = ‖x.1‖₊⁻¹  := sorry
 
-lemma PadicInt.coe_injective {x y : ℤ_[p]}: ((x : ℚ_[p]) = (y : ℚ_[p])) ↔ (x = y) := by
+lemma PadicInt.coe_injective {x y : ℤ_[p]}: (x = y) ↔ ((x : ℚ_[p]) = (y : ℚ_[p])) := by
   sorry
 
 instance : Coe ℤ_[p] ℚ_[p] := by infer_instance
-instance : Coe ℤ_[p]ˣ ℚ_[p]ˣ where
-  coe u := sorry
+noncomputable instance : Coe ℤ_[p]ˣ ℚ_[p]ˣ where
+  coe u := ⟨u.1, u.1⁻¹,
+    by sorry,
+    by sorry⟩
 
 lemma distribHaarChar_padic_integral (x : ℤ_[p]ˣ) : distribHaarChar ℚ_[p] (x : ℚ_[p]ˣ) = ‖(x : ℚ_[p])‖₊⁻¹ := by
   let K : Set ℚ_[p] := {x : ℚ_[p] | ‖x‖ ≤ 1}
   refine distribHaarChar_eq_of_measure_smul_eq_mul (s := K) (μ := volume) (G := ℚ_[p]ˣ)
     (by simp [K, Padic.volume_closedBall]) (by simp [K, Padic.volume_closedBall]) ?_
   rw [Units.smul_def]
-  sorry