IdealCharacterMellinMeasurable.lean

1 import PaperX.IdealClassQuantitativeAttachment
2 import Mathlib.MeasureTheory.Function.Floor
3 
4 /-! The ordinary ideal-class counting functions are actual step functions on
5 the integer norm scale, and hence measurable. No regularity of an abstract
6 counting function is assumed. -/
7 
8 set_option autoImplicit false
9 noncomputable section
10 
11 open Ideal MeasureTheory NumberField
12 open scoped nonZeroDivisors
13 
14 namespace PaperX.IdealClassCharacter
15 
16 open PaperX.IdealClassQuantitative
17 
18 variable (K : Type*) [Field K] [NumberField K]
19 
20 /-- Integral ideal norms make the count constant on each integer step. -/
21 theorem classCount_eq_floor (C : ClassGroup (𝓞 K)) (x : ℝ) :
22     classCount K C x = classCount K C (Int.floor x : ℝ) := by
23   unfold classCount
24   apply Nat.card_congr
25   apply Equiv.subtypeEquivProp
26   funext I
27   apply propext
28   have hn : ((absNorm (I : Ideal (𝓞 K)) : ℤ) : ℝ) =
29       (absNorm (I : Ideal (𝓞 K)) : ℝ) := by norm_cast
30   rw [← hn, Int.cast_le, Int.le_floor]
31 
32 /-- Actual ordinary class counts are measurable on all of the real line. -/
33 theorem measurable_classCount (C : ClassGroup (𝓞 K)) :
34     Measurable (classCount K C) := by
35   have h : Measurable (fun n : ℤ => classCount K C (n : ℝ)) :=
36     measurable_of_countable _
37   convert h.comp (Int.measurable_floor (R := ℝ)) using 1
38   funext x
39   exact classCount_eq_floor K C x
40 
41 end PaperX.IdealClassCharacter

Back to source controls