IdealNormCharacterMellin.lean

1 import PaperX.IdealNormWeightedAttachment
2 import PaperX.RealAxisMellinMoment
3 import Mathlib.MeasureTheory.Function.Floor
4 
5 /-! Measurability and the real-axis Mellin transform for actual ideal
6 norm-weighted sums in one ideal class. -/
7 
8 set_option autoImplicit false
9 noncomputable section
10 
11 open Ideal MeasureTheory NumberField Filter Set Asymptotics
12 open scoped nonZeroDivisors Classical Topology
13 
14 namespace PaperX.IdealNormWeighted
15 
16 open PaperX.RealAxisMellinMoment
17 
18 variable (K : Type*) [Field K] [NumberField K]
19 
20 /-- Integral ideal norms make every fixed norm-weighted class sum constant on
21 integer steps. -/
22 theorem classNormSum_eq_floor (C : ClassGroup (𝓞 K)) (f : ℕ → ℂ) (x : ℝ) :
23     classNormSum K C f x = classNormSum K C f (Int.floor x : ℝ) := by
24   unfold classNormSum
25   let e : BoundedClassIdeals K C x ≃ BoundedClassIdeals K C (Int.floor x : ℝ) :=
26     Equiv.subtypeEquivProp (by
27       funext I
28       apply propext
29       have hn : ((absNorm (I : Ideal (𝓞 K)) : ℤ) : ℝ) =
30           (absNorm (I : Ideal (𝓞 K)) : ℝ) := by norm_cast
31       rw [and_congr_left_iff]
32       intro _
33       rw [← hn, Int.cast_le, Int.le_floor])
34   exact finsum_eq_of_bijective e e.bijective (fun _ => rfl)
35 
36 /-- Actual ideal norm-weighted class sums are measurable on the real line. -/
37 theorem measurable_classNormSum (C : ClassGroup (𝓞 K)) (f : ℕ → ℂ) :
38     Measurable (classNormSum K C f) := by
39   have h : Measurable (fun n : ℤ => classNormSum K C f (n : ℝ)) :=
40     measurable_of_countable _
41   convert h.comp (Int.measurable_floor (R := ℝ)) using 1
42   funext x
43   exact classNormSum_eq_floor K C f x
44 
45 /-- Mellin transform of an actual norm-weighted ideal-class summatory function,
46 with real parameter `h = s - 1`. -/
47 def normMellin (C : ClassGroup (𝓞 K)) (f : ℕ → ℂ) (h : ℝ) : ℂ :=
48   mellinIntegral (classNormSum K C f) h
49 
50 end PaperX.IdealNormWeighted

Back to source controls