feat: progress on computing modular characters in concrete types

FLT/FLT_files.lean

@@ -8,16 +8,28 @@ import FLT.EllipticCurve.Torsion
 import FLT.ForMathlib.ActionTopology
 import FLT.ForMathlib.Algebra
 import FLT.ForMathlib.DomMulActMeasure
+import FLT.ForMathlib.MeasurableSpacePadics
 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.HIMExperiments.flatness
+import FLT.HaarMeasure.ConcreteCharCalculations
 import FLT.HaarMeasure.DistribHaarChar
 import FLT.Hard.Results
-import FLT.HIMExperiments.flatness
+import FLT.Mathlib.Algebra.Order.Hom.Monoid
+import FLT.Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
+import FLT.Mathlib.Analysis.Complex.Basic
+import FLT.Mathlib.Data.Complex.Basic
+import FLT.Mathlib.Data.ENNReal.Inv
+import FLT.Mathlib.GroupTheory.Complement
+import FLT.Mathlib.LinearAlgebra.Determinant
+import FLT.Mathlib.MeasureTheory.Group.Action
+import FLT.Mathlib.NumberTheory.Padics.PadicIntegers
+import FLT.Mathlib.RingTheory.Norm.Defs
 import FLT.MathlibExperiments.Coalgebra.Monoid
 import FLT.MathlibExperiments.Coalgebra.Sweedler
 import FLT.MathlibExperiments.Coalgebra.TensorProduct

FLT/ForMathlib/MeasurableSpacePadics.lean

@@ -0,0 +1,50 @@
+import Mathlib.MeasureTheory.Measure.Haar.Basic
+import Mathlib.NumberTheory.Padics.ProperSpace
+
+open Topology TopologicalSpace MeasureTheory Measure
+
+variable {p : ℕ} [Fact p.Prime]
+
+instance : MeasurableSpace ℚ_[p] := borel _
+instance : BorelSpace ℚ_[p] := ⟨rfl⟩
+
+instance : MeasurableSpace ℤ_[p] := Subtype.instMeasurableSpace
+instance : BorelSpace ℤ_[p] := Subtype.borelSpace _
+
+lemma PadicInt.isOpenEmbedding_coe : IsOpenEmbedding ((↑) : ℤ_[p] → ℚ_[p]) := by
+  refine IsOpen.isOpenEmbedding_subtypeVal (?_ : IsOpen {y : ℚ_[p] | ‖y‖ ≤ 1})
+  simpa only [Metric.closedBall, dist_eq_norm_sub, sub_zero] using
+    IsUltrametricDist.isOpen_closedBall (0 : ℚ_[p]) one_ne_zero
+
+lemma PadicInt.isMeasurableEmbedding_coe : MeasurableEmbedding ((↑) : ℤ_[p] → ℚ_[p]) := by
+  convert PadicInt.isOpenEmbedding_coe.measurableEmbedding
+  exact inferInstanceAs (BorelSpace ℤ_[p])
+
+noncomputable instance : MeasureSpace ℤ_[p] := ⟨addHaarMeasure ⊤⟩
+
+instance : IsAddHaarMeasure (volume : Measure ℤ_[p]) := isAddHaarMeasure_addHaarMeasure _
+
+lemma PadicInt.volume_univ : volume (Set.univ : Set ℤ_[p]) = 1 := addHaarMeasure_self
+
+-- should we more generally make a map from `CompactOpens` to `PositiveCompacts`?
+private def Padic.unitBall_positiveCompact : PositiveCompacts ℚ_[p] where
+  carrier := {y | ‖y‖ ≤ 1}
+  isCompact' := by simpa only [Metric.closedBall, dist_zero_right] using
+    isCompact_closedBall (0 : ℚ_[p]) 1
+  interior_nonempty' := by
+    rw [IsOpen.interior_eq]
+    · exact ⟨0, by simp⟩
+    · simpa only [Metric.closedBall, dist_zero_right] using
+        IsUltrametricDist.isOpen_closedBall (0 : ℚ_[p]) one_ne_zero
+
+noncomputable instance : MeasureSpace ℚ_[p] := ⟨addHaarMeasure Padic.unitBall_positiveCompact⟩
+
+instance : IsAddHaarMeasure (volume : Measure ℚ_[p]) := isAddHaarMeasure_addHaarMeasure _
+
+lemma Padic.volume_closedBall : volume {x : ℚ_[p] | ‖x‖ ≤ 1} = 1 := addHaarMeasure_self
+
+lemma PadicInt.volume_addSubgroupClosure (x : ℤ_[p]ˣ) :
+    volume (AddSubgroup.closure {x.1} : Set ℤ_[p]) = ‖x.1‖₊⁻¹ := sorry
+
+lemma Padic.volume_smul (x : ℚ_[p]ˣ) : volume (AddSubgroup.closure {x.1} : Set ℚ_[p]) = ‖x.1‖₊⁻¹ :=
+  sorry

FLT/HaarMeasure/ConcreteCharCalculations.lean

@@ -0,0 +1,48 @@
+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.MeasureTheory.Group.Action
+import FLT.Mathlib.NumberTheory.Padics.PadicIntegers
+import FLT.Mathlib.RingTheory.Norm.Defs
+
+open Real Complex Padic MeasureTheory Measure NNReal Set TopologicalSpace
+open scoped Pointwise ENNReal
+
+lemma distribHaarChar_complex (z : ℂˣ) : distribHaarChar ℂ z = ‖(z : ℂ)‖₊ ^ (-2 : ℤ) := by
+  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]
+
+lemma distribHaarChar_real (x : ℝˣ) : distribHaarChar ℝ x = ‖(x : ℝ)‖₊⁻¹ := by
+  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]
+  simp [Real.ennnorm_eq_ofReal_abs, abs_inv, ENNReal.ofReal_inv_of_pos]
+
+variable {p : ℕ} [Fact p.Prime]
+
+noncomputable instance : Coe ℤ_[p]ˣ ℚ_[p]ˣ where coe := Units.map PadicInt.Coe.ringHom.toMonoidHom
+
+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

FLT/HaarMeasure/DistribHaarChar.lean

@@ -78,3 +78,8 @@ lemma distribHaarChar_mul (g : G) (s : Set A) : distribHaarChar A g * μ s = μ
 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]
+
+lemma distribHaarChar_eq_of_measure_smul_eq_mul (hs₀ : μ s ≠ 0) (hs : μ s ≠ ∞) {r : ℝ≥0}
+    (hμgs : μ (g⁻¹ • s) = r * μ s) : distribHaarChar A g = r := by
+  refine ENNReal.coe_injective ?_
+  rw [distribHaarChar_eq_div hs₀ hs, hμgs, ENNReal.mul_div_cancel_right hs₀ hs]

FLT/Mathlib/Analysis/Complex/Basic.lean

@@ -0,0 +1,9 @@
+
+import Mathlib.Analysis.Complex.Basic
+
+open Complex
+
+variable {s t : Set ℝ}
+
+lemma IsCompact.reProdIm (hs : IsCompact s) (ht : IsCompact t) : IsCompact (s ×ℂ t) :=
+  equivRealProdCLM.toHomeomorph.isCompact_preimage.2 (hs.prod ht)

FLT/Mathlib/Data/Complex/Basic.lean

@@ -0,0 +1,19 @@
+import Mathlib.Data.Complex.Basic
+
+open Set
+
+namespace Complex
+variable {s t : Set ℝ}
+
+open Set
+
+lemma «forall» {p : ℂ → Prop} : (∀ x, p x) ↔ ∀ a b, p ⟨a, b⟩ := by aesop
+lemma «exists» {p : ℂ → Prop} : (∃ x, p x) ↔ ∃ a b, p ⟨a, b⟩ := by aesop
+
+@[simp] lemma reProdIm_nonempty : (s ×ℂ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty := by
+  simp [Set.Nonempty, reProdIm, Complex.exists]
+
+@[simp] lemma reProdIm_eq_empty : s ×ℂ t = ∅ ↔ s = ∅ ∨ t = ∅ := by
+  simp [← not_nonempty_iff_eq_empty, reProdIm_nonempty, -not_and, not_and_or]
+
+end Complex

FLT/Mathlib/GroupTheory/Complement.lean

@@ -0,0 +1,18 @@
+import Mathlib.GroupTheory.Complement
+
+open Set
+open scoped Pointwise
+
+namespace Subgroup
+variable {G : Type*} [Group G] {H : Subgroup G} [H.FiniteIndex] {s : Set G}
+
+@[to_additive]
+lemma finite_of_mem_leftTransversals (hs : s ∈ leftTransversals H) : s.Finite := sorry
+
+@[to_additive]
+lemma finite_of_mem_rightTransversals (hs : s ∈ rightTransversals H) : s.Finite := sorry
+
+@[to_additive]
+lemma mul_of_mem_leftTransversals (hs : s ∈ leftTransversals H) : s * (H : Set G) = univ := sorry
+
+end Subgroup

FLT/Mathlib/LinearAlgebra/Determinant.lean

@@ -0,0 +1,8 @@
+import Mathlib.LinearAlgebra.Determinant
+
+namespace LinearMap
+variable {R : Type*} [CommRing R]
+
+variable (R) in
+@[simp] lemma det_mul (a : R) : (mul R R a).det = a := by
+  sorry

FLT/Mathlib/MeasureTheory/Group/Action.lean

@@ -0,0 +1,35 @@
+import Mathlib.MeasureTheory.Group.Action
+import Mathlib.MeasureTheory.Group.Pointwise
+import Mathlib.Topology.Algebra.InfiniteSum.ENNReal
+import FLT.Mathlib.GroupTheory.Complement
+
+/-!
+# TODO
+
+* Make `α` implicit in `SMulInvariantMeasure`
+* Rename `SMulInvariantMeasure` to `Measure.IsSMulInvariant`
+-/
+
+open Subgroup Set
+open scoped Pointwise
+
+namespace MeasureTheory
+variable {G α : Type*} [Group G] [MeasurableSpace G] [MeasurableMul G] [MeasurableSpace α]
+  {H : Subgroup G} [H.FiniteIndex]
+
+@[to_additive index_mul_addHaar_addSubgroup]
+lemma index_mul_haar_subgroup (hH : MeasurableSet (H : Set G)) (μ : Measure G)
+    [μ.IsMulLeftInvariant] : H.index * μ H = μ univ := by
+  obtain ⟨s, hs, -⟩ := H.exists_left_transversal 1
+  have hs' : Finite s := finite_of_mem_leftTransversals hs
+  calc
+    H.index * μ H = ∑' a : s, μ (a.val • H) := by
+      simp [measure_smul]
+      rw [← Set.Finite.cast_ncard_eq hs', ← Nat.card_coe_set_eq, card_left_transversal hs]
+      norm_cast
+    _ = μ univ := by
+      rw [← measure_iUnion _ fun _ ↦ hH.const_smul _]
+      · simp [mul_of_mem_leftTransversals hs]
+      · sorry
+
+end MeasureTheory

FLT/Mathlib/NumberTheory/Padics/PadicIntegers.lean

@@ -0,0 +1,14 @@
+import Mathlib.NumberTheory.Padics.PadicIntegers
+
+-- This is cool notation. Should mathlib have it?
+scoped[GroupTheory] notation "[" G ":" H "]" => @AddSubgroup.index G _ H
+
+open scoped GroupTheory
+
+namespace PadicInt
+variable {p : ℕ} [Fact p.Prime]
+
+lemma index_addSubgroupClosure (a : ℤ_[p]) : (AddSubgroup.closure {a}).index = ‖a‖⁻¹ := by
+  sorry
+
+end PadicInt

FLT/Mathlib/RingTheory/Norm/Defs.lean

@@ -0,0 +1,8 @@
+import Mathlib.RingTheory.Norm.Defs
+
+namespace LinearMap
+variable {M A B : Type*} [CommRing A] [CommRing B] [AddCommGroup M] [Algebra A B] [Module A M]
+  [Module B M] [IsScalarTower A B M] [Module.Finite A B] [Module.Finite B M]
+
+lemma det_restrictScalars (f : M →ₗ[B] M) : (f.restrictScalars A).det = Algebra.norm A f.det := by
+  sorry