cleanup

FLT/FLT_files.lean

@@ -13,14 +13,16 @@ 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.HaarMeasure.DistribHaarChar.Basic
+import FLT.HaarMeasure.DistribHaarChar.Padic
+import FLT.HaarMeasure.DistribHaarChar.RealComplex
 import FLT.HaarMeasure.MeasurableSpacePadics
 import FLT.Hard.Results
 import FLT.Junk.Algebra
 import FLT.Junk.Algebra2
 import FLT.Mathlib.Algebra.Algebra.Subalgebra.Pi
 import FLT.Mathlib.Algebra.Group.Subgroup.Defs
+import FLT.Mathlib.Algebra.Group.Subgroup.Pointwise
 import FLT.Mathlib.Algebra.Group.Units.Hom
 import FLT.Mathlib.Algebra.GroupWithZero.NonZeroDivisors
 import FLT.Mathlib.Algebra.Module.End

FLT/HaarMeasure/DistribHaarChar/Padic.lean

@@ -0,0 +1,108 @@
+/-
+Copyright (c) 2024 Yaël Dillies, Javier Lopez-Contreras. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies, Javier Lopez-Contreras
+-/
+import FLT.Mathlib.MeasureTheory.Group.Action
+import FLT.HaarMeasure.DistribHaarChar.Basic
+import FLT.HaarMeasure.MeasurableSpacePadics
+
+/-!
+# The distributive Haar characters of the p-adics
+
+This file computes `distribHaarChar` in the case of the actions of `ℤ_[p]ˣ` on `ℤ_[p]` and of
+`ℚ_[p]ˣ` on `ℚ_[p]`.
+
+This lets us know what `volume (x • s)` is in terms of `‖x‖` and `volume s`, when `x` is a
+p-adic/p-adic integer and `s` is a set of p-adics/p-adic integers.
+
+## Main declarations
+
+* `distribHaarChar_padic`: `distribHaarChar ℚ_[p]` is the usual p-adic norm on `ℚ_[p]`.
+* `distribHaarChar_padicInt`: `distribHaarChar ℤ_[p]` is the usual p-adic norm on `ℤ_[p]`.
+* `Padic.volume_padic_smul`: `volume (x • s) = ‖x‖₊ * volume s` for all `x : ℚ_[p]` and
+  `s : Set ℚ_[p]`.
+* `PadicInt.volume_padicInt_smul`: `volume (x • s) = ‖x‖₊ * volume s` for all `x : ℤ_[p]` and
+  `s : Set ℤ_[p]`.
+-/
+
+open Padic MeasureTheory Measure Metric Set
+open scoped Pointwise ENNReal NNReal nonZeroDivisors
+
+variable {p : ℕ} [Fact p.Prime]
+
+private lemma submoduleSpan_padicInt_one :
+    Submodule.span ℤ_[p] (1 : Set ℚ_[p]) = closedBall (0 : ℚ_[p]) 1 := by
+  rw [← Submodule.one_eq_span_one_set]
+  ext x
+  simp
+  simp [PadicInt]
+
+private lemma distribHaarChar_padic_padicInt (x : ℤ_[p]⁰) :
+    distribHaarChar ℚ_[p] (x : ℚ_[p]ˣ) = ‖(x : ℚ_[p])‖₊ := by
+  let K : AddSubgroup ℚ_[p] := (Submodule.span ℤ_[p] 1).toAddSubgroup
+  let H := (x : ℚ_[p]) • K
+  refine distribHaarChar_eq_of_measure_smul_eq_mul (s := K) (μ := volume) (G := ℚ_[p]ˣ)
+    (by simp [K, submoduleSpan_padicInt_one, closedBall, Padic.volume_closedBall_one])
+    (by simp [K, submoduleSpan_padicInt_one, closedBall, Padic.volume_closedBall_one]) (?_)
+  change volume (H : Set ℚ_[p]) = ‖(x : ℚ_[p])‖₊ * volume (K : Set ℚ_[p])
+  have hHK : H ≤ K := by
+    simpa [H, K, -Submodule.smul_le_self_of_tower]
+      using (.span _ 1 : Submodule ℤ_[p] ℚ_[p]).smul_le_self_of_tower (x : ℤ_[p])
+  have : H.FiniteRelIndex K :=
+    PadicInt.smul_submoduleSpan_finiteRelIndex_submoduleSpan (p := p)
+      (mem_nonZeroDivisors_iff_ne_zero.1 x.2) {1}
+  have H_relindex_Z : (H.relindex K : ℝ≥0∞) = ‖(x : ℚ_[p])‖₊⁻¹ :=
+    congr(ENNReal.ofNNReal $(PadicInt.smul_submoduleSpan_relindex_submoduleSpan (p := p) x {1}))
+  rw [← index_mul_addHaar_addSubgroup_eq_addHaar_addSubgroup hHK, H_relindex_Z, ENNReal.coe_inv,
+    ENNReal.mul_inv_cancel_left]
+  · simp
+  · simp
+  · simp
+  · simpa [H, K, submoduleSpan_padicInt_one] using measurableSet_closedBall.const_smul (x : ℚ_[p]ˣ)
+  · simpa [K, submoduleSpan_padicInt_one] using measurableSet_closedBall
+
+/-- The distributive Haar character of the action of `ℚ_[p]ˣ` on `ℚ_[p]` is the usual p-adic norm.
+
+This means that `volume (x • s) = ‖x‖ * volume s` for all `x : ℚ_[p]` and `s : Set ℚ_[p]`.
+See `Padic.volume_padic_smul` -/
+lemma distribHaarChar_padic (x : ℚ_[p]ˣ) : distribHaarChar ℚ_[p] x = ‖(x : ℚ_[p])‖₊ := by
+  -- Write the RHS as the application of a monoid hom `g`.
+  let g : ℚ_[p]ˣ →* ℝ≥0 := {
+    toFun := fun x => ‖(x : ℚ_[p])‖₊
+    map_one' := by simp
+    map_mul' := by simp
+  }
+  revert x
+  suffices distribHaarChar ℚ_[p] = g by simp [this, g]
+  -- By density of `ℤ_[p]⁰` inside `ℚ_[p]ˣ`, it's enough to check that `distribHaarChar ℚ_[p]` and
+  -- `g` agree on `ℤ_[p]⁰`.
+  refine MonoidHom.eq_of_eqOn_dense (PadicInt.closure_nonZeroDivisors_padicInt (p := p)) ?_
+  -- But this is what we proved in `distribHaarChar_padic_padicInt`.
+  simp
+  ext x
+  simp [g]
+  rw [distribHaarChar_padic_padicInt]
+  rfl
+
+@[simp]
+lemma Padic.volume_padic_smul (x : ℚ_[p]) (s : Set ℚ_[p]) : volume (x • s) = ‖x‖₊ * volume s := by
+  obtain rfl | hx := eq_or_ne x 0
+  · simp [(finite_zero.subset s.zero_smul_set_subset).measure_zero]
+  · lift x to ℚ_[p]ˣ using hx.isUnit
+    rw [← distribHaarChar_padic, distribHaarChar_mul, Units.smul_def]
+
+@[simp] lemma Padic.volume_padicInt_smul (x : ℤ_[p]) (s : Set ℚ_[p]) :
+    volume (x • s) = ‖x‖₊ * volume s := by simpa [-volume_padic_smul] using volume_padic_smul x s
+
+@[simp] lemma PadicInt.volume_padicInt_smul (x : ℤ_[p]) (s : Set ℤ_[p]) :
+    volume (x • s) = ‖x‖₊ * volume s := by
+  simpa [-volume_padicInt_smul, ← image_coe_smul_set] using Padic.volume_padicInt_smul x ((↑) '' s)
+
+/-- The distributive Haar character of the action of `ℤ_[p]ˣ` on `ℤ_[p]` is the usual p-adic norm.
+
+This means that `volume (x • s) = ‖x‖ * volume s` for all `x : ℤ_[p]` and `s : Set ℤ_[p]`.
+See `PadicInt.volume_padicInt_smul` -/
+lemma distribHaarChar_padicInt (x : ℤ_[p]ˣ) : distribHaarChar ℤ_[p] x = ‖(x : ℤ_[p])‖₊ :=
+  distribHaarChar_eq_of_measure_smul_eq_mul (s := univ) (μ := volume) (by simp) (measure_ne_top _ _)
+    (PadicInt.volume_padicInt_smul ..)

FLT/HaarMeasure/DistribHaarChar/RealComplex.lean

@@ -0,0 +1,73 @@
+/-
+Copyright (c) 2024 Yaël Dillies, Javier Lopez-Contreras. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies, Javier Lopez-Contreras
+-/
+import Mathlib.Analysis.Complex.ReImTopology
+import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
+import Mathlib.RingTheory.Complex
+import FLT.HaarMeasure.DistribHaarChar.Basic
+import FLT.Mathlib.Analysis.Complex.Basic
+import FLT.Mathlib.Data.Complex.Basic
+import FLT.Mathlib.LinearAlgebra.Determinant
+import FLT.Mathlib.RingTheory.Norm.Defs
+
+/-!
+# The distributive Haar characters of `ℝ` and `ℂ`
+
+This file computes `distribHaarChar` in the case of the actions of `ℝˣ` on `ℝ` and of `ℂˣ` on `ℂ`.
+
+This lets us know what `volume (x • s)` is in terms of `‖x‖` and `volume s`, when `x` is a
+real/complex number and `s` is a set of reals/complex numbers.
+
+## Main declarations
+
+* `distribHaarChar_real`: `distribHaarChar ℝ` is the usual norm on `ℝ`.
+* `distribHaarChar_complex`: `distribHaarChar ℂ` is the usual norm on `ℂ` squared.
+* `Real.volume_real_smul`: `volume (x • s) = ‖x‖₊ * volume s` for all `x : ℝ` and `s : Set ℝ`.
+* `Complex.volume_complex_smul`: `volume (z • s) = ‖z‖₊ ^ 2 * volume s` for all `z : ℂ` and
+  `s : Set ℂ`.
+-/
+
+open Real Complex MeasureTheory Measure Set
+open scoped Pointwise
+
+lemma Real.volume_real_smul (x : ℝ) (s : Set ℝ) : volume (x • s) = ‖x‖₊ * volume s := by
+  simp [← ennnorm_eq_ofReal_abs]
+
+/-- The distributive Haar character of the action of `ℝˣ` on `ℝ` is the usual norm.
+
+This means that `volume (x • s) = ‖x‖ * volume s` for all `x : ℝ` and `s : Set ℝ`.
+See `Real.volume_real_smul`. -/
+lemma distribHaarChar_real (x : ℝˣ) : distribHaarChar ℝ x = ‖(x : ℝ)‖₊ :=
+  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
+      (Real.volume_real_smul ..)
+
+/-- The distributive Haar character of the action of `ℂˣ` on `ℂ` is the usual norm squared.
+
+This means that `volume (z • s) = ‖z‖ ^ 2 * volume s` for all `z : ℂ` and `s : Set ℂ`.
+See `Complex.volume_complex_smul`. -/
+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
+    simpa [LinearMap.mul, LinearMap.mk₂, LinearMap.mk₂', LinearMap.mk₂'ₛₗ, Units.smul_def]
+      using preimage_smul_inv z (Icc 0 1 ×ℂ Icc 0 1)
+  · simp [ofReal_norm_eq_coe_nnnorm, ← Complex.norm_eq_abs, ENNReal.ofReal_pow, zpow_ofNat]
+  · simp [zpow_ofNat]
+
+lemma Complex.volume_complex_smul (z : ℂ) (s : Set ℂ) : volume (z • s) = ‖z‖₊ ^ 2 * volume s := by
+  obtain rfl | hz := eq_or_ne z 0
+  · simp [(finite_zero.subset s.zero_smul_set_subset).measure_zero]
+  · lift z to ℂˣ using hz.isUnit
+    rw [← ENNReal.coe_pow, ← distribHaarChar_complex, distribHaarChar_mul, Units.smul_def]

FLT/HaarMeasure/MeasurableSpacePadics.lean

@@ -1,19 +1,29 @@
+/-
+Copyright (c) 2024 Yaël Dillies, David Loeffler. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies, David Loeffler
+-/
 import Mathlib.MeasureTheory.Measure.Haar.Basic
 import Mathlib.NumberTheory.Padics.ProperSpace
-import FLT.Mathlib.MeasureTheory.Group.Action
 import FLT.Mathlib.NumberTheory.Padics.PadicIntegers
 
-open Topology TopologicalSpace MeasureTheory Measure
-open scoped Pointwise nonZeroDivisors
+/-!
+# Measurability and measures on the p-adics
+
+This file endows `ℤ_[p]` and `ℚ_[p]` with their Borel sigma-algebra and their Haar measure that
+makes `ℤ_[p]` (or the copy of `ℤ_[p]` inside `ℚ_[p]`) have norm `1`.
+-/
+
+open MeasureTheory Measure TopologicalSpace Topology
 
 variable {p : ℕ} [Fact p.Prime]
 
 namespace Padic
 
-instance : MeasurableSpace ℚ_[p] := borel _
-instance : BorelSpace ℚ_[p] := ⟨rfl⟩
+instance instMeasurableSpace : MeasurableSpace ℚ_[p] := borel _
+instance instBorelSpace : BorelSpace ℚ_[p] := ⟨rfl⟩
 
--- should we more generally make a map from `CompactOpens` to `PositiveCompacts`?
+-- Should we more generally make a map from `CompactOpens` to `PositiveCompacts`?
 private def unitBall_positiveCompact : PositiveCompacts ℚ_[p] where
   carrier := {y | ‖y‖ ≤ 1}
   isCompact' := by simpa only [Metric.closedBall, dist_zero_right] using
@@ -24,41 +34,36 @@ private def unitBall_positiveCompact : PositiveCompacts ℚ_[p] where
     · simpa only [Metric.closedBall, dist_zero_right] using
         IsUltrametricDist.isOpen_closedBall (0 : ℚ_[p]) one_ne_zero
 
-noncomputable instance : MeasureSpace ℚ_[p] := ⟨addHaarMeasure Padic.unitBall_positiveCompact⟩
+noncomputable instance instMeasureSpace : MeasureSpace ℚ_[p] :=
+  ⟨addHaarMeasure unitBall_positiveCompact⟩
 
-instance : IsAddHaarMeasure (volume : Measure ℚ_[p]) := isAddHaarMeasure_addHaarMeasure _
+instance instIsAddHaarMeasure : IsAddHaarMeasure (volume : Measure ℚ_[p]) :=
+  isAddHaarMeasure_addHaarMeasure _
 
-lemma volume_closedBall : volume {x : ℚ_[p] | ‖x‖ ≤ 1} = 1 := addHaarMeasure_self
+lemma volume_closedBall_one : volume {x : ℚ_[p] | ‖x‖ ≤ 1} = 1 := addHaarMeasure_self
 
 end Padic
 
 namespace PadicInt
 
-instance : MeasurableSpace ℤ_[p] := Subtype.instMeasurableSpace
-instance : BorelSpace ℤ_[p] := Subtype.borelSpace _
-
-lemma 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
+instance instMeasurableSpace : MeasurableSpace ℤ_[p] := Subtype.instMeasurableSpace
+instance instBorelSpace : BorelSpace ℤ_[p] := Subtype.borelSpace _
 
 lemma isMeasurableEmbedding_coe : MeasurableEmbedding ((↑) : ℤ_[p] → ℚ_[p]) := by
   convert isOpenEmbedding_coe.measurableEmbedding
   exact inferInstanceAs (BorelSpace ℤ_[p])
 
-noncomputable instance : MeasureSpace ℤ_[p] := ⟨addHaarMeasure ⊤⟩
+noncomputable instance instMeasureSpace : MeasureSpace ℤ_[p] := ⟨addHaarMeasure ⊤⟩
 
-instance : IsAddHaarMeasure (volume : Measure ℤ_[p]) := isAddHaarMeasure_addHaarMeasure _
+instance instIsAddHaarMeasure : IsAddHaarMeasure (volume : Measure ℤ_[p]) :=
+  isAddHaarMeasure_addHaarMeasure _
 
 @[simp] lemma volume_univ : volume (Set.univ : Set ℤ_[p]) = 1 := addHaarMeasure_self
 
-lemma volume_smul {x : ℤ_[p]} (hx : x ∈ ℤ_[p]⁰) : volume (x • ⊤ : Set ℤ_[p]) = ‖x.1‖₊ := by
-  sorry
-  -- rw [← index_smul_top]
+instance instIsFiniteMeasure : IsFiniteMeasure (volume : Measure ℤ_[p]) where
+  measure_univ_lt_top := by simp
 
-end PadicInt
+-- https://github.com/ImperialCollegeLondon/FLT/issues/278
+@[simp] lemma volume_coe (s : Set ℤ_[p]) : volume ((↑) '' s : Set ℚ_[p]) = volume s := sorry
 
-lemma Padic.volume_smul {x : ℚ_[p]} (hx : x ≠ 0) : volume (x • {y : ℚ_[p] | ‖y‖ ≤ 1}) = ‖x‖₊ := by
-  obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective (A := ℤ_[p]) x
-  simp
-  sorry
+end PadicInt