IdealCharacterMellin.lean

1 import PaperX.IdealCharacterMellinMeasurable
2 import PaperX.IdealClassCharacterBound
3 import PaperX.RealAxisMellinMoment
4 
5 /-! Logarithmic first moments and first-order Mellin endpoint control for sums
6 over actual integral ideals weighted by ordinary class characters. The power
7 saving and measurability are proved from the number field, not supplied as
8 analytic hypotheses. -/
9 
10 set_option autoImplicit false
11 noncomputable section
12 
13 open Ideal NumberField MeasureTheory Filter Set Asymptotics
14 open scoped nonZeroDivisors Classical BigOperators Topology
15 
16 namespace PaperX.IdealClassCharacter
17 
18 open PaperX.IdealClassQuantitative PaperX.RealAxisMellinMoment
19 
20 variable (K : Type*) [Field K] [NumberField K]
21 
22 /-- Any ordinary-class weighted sum over actual bounded ideals is measurable. -/
23 theorem measurable_weightedSum (w : ClassGroup (𝓞 K) → ℂ) :
24     Measurable (weightedSum K w) := by
25   change Measurable (fun x => weightedSum K w x)
26   simp_rw [weightedSum_eq_sum_classCount]
27   exact Finset.measurable_sum _ fun C _ =>
28     measurable_const.mul
29       ((measurable_of_countable (fun n : ℕ => (n : ℂ))).comp (measurable_classCount K C))
30 
31 /-- The actual real-parameter Mellin integral, with parameter h=s-1. -/
32 def classMellin (w : ClassGroup (𝓞 K) → ℂ) (h : ℝ) : ℂ :=
33   mellinIntegral (weightedSum K w) h
34 
35 /-- Cancellation of the common main term yields the logarithmic first moment. -/
36 theorem integrable_weightedSum_logMoment (w : ClassGroup (𝓞 K) → ℂ)
37     (hw : ∑ C, w C = 0) :
38     Integrable (fun x : ℝ =>
39       (1 + Real.log x) * ‖(x ^ (-2 : ℝ)) • weightedSum K w x‖)
40       (volume.restrict (Ioi 1)) := by
41   obtain ⟨M, _, hM⟩ := exists_weightedSum_bound K w hw
42   exact integrable_weighted_moment_of_power_bound
43     (measurable_weightedSum K w).aestronglyMeasurable (countExponent_lt_one K)
44     (fun x hx => hM x hx.le)
45 
46 /-- The Mellin endpoint error is O(h) for actual zero-mean class weights. -/
47 theorem classMellin_sub_isBigO (w : ClassGroup (𝓞 K) → ℂ)
48     (hw : ∑ C, w C = 0) :
49     (fun h => classMellin K w h - classMellin K w 0)
50       =O[𝓝[>] (0 : ℝ)] (fun h : ℝ => h) := by
51   obtain ⟨M, _, hM⟩ := exists_weightedSum_bound K w hw
52   exact mellinIntegral_sub_isBigO_of_power_bound
53     (measurable_weightedSum K w).aestronglyMeasurable (countExponent_lt_one K)
54     (fun x hx => hM x hx.le)
55 
56 /-- The finite logarithmic moment is an explicit error constant, valid for
57 every nonnegative real parameter. -/
58 theorem classMellin_sub_norm_le (w : ClassGroup (𝓞 K) → ℂ)
59     (hw : ∑ C, w C = 0) {h : ℝ} (hh : 0 ≤ h) :
60     ‖classMellin K w h - classMellin K w 0‖ ≤
61       h * ∫ x in Ioi (1 : ℝ),
62         (1 + Real.log x) * ‖(x ^ (-2 : ℝ)) • weightedSum K w x‖ := by
63   have hA : AEStronglyMeasurable
64       (fun x : ℝ => (x ^ (-2 : ℝ)) • weightedSum K w x)
65       (volume.restrict (Ioi 1)) := by
66     have hm : Measurable (fun x : ℝ => x ^ (-2 : ℝ)) := by fun_prop
67     exact hm.aestronglyMeasurable.smul (measurable_weightedSum K w).aestronglyMeasurable
68   have hu : ∀ᵐ x ∂volume.restrict (Ioi (1 : ℝ)), 0 ≤ Real.log x := by
69     filter_upwards [ae_restrict_mem measurableSet_Ioi] with x hx
70     exact Real.log_nonneg (le_of_lt hx)
71   simpa only [classMellin, mellinIntegral_eq_endpointIntegral] using
72     PaperX.RealAxisEndpointIntegral.endpointIntegral_sub_norm_le
73       (volume.restrict (Ioi 1)) hA Real.measurable_log hu
74       (integrable_weightedSum_logMoment K w hw) hh
75 
76 /-- In particular, every nontrivial ordinary class character has a finite
77 logarithmic first moment. -/
78 theorem integrable_character_logMoment (χ : ClassGroup (𝓞 K) →* ℂ)
79     (hχ : χ ≠ 1) :
80     Integrable (fun x : ℝ =>
81       (1 + Real.log x) * ‖(x ^ (-2 : ℝ)) • weightedSum K χ x‖)
82       (volume.restrict (Ioi 1)) :=
83   integrable_weightedSum_logMoment K χ (sum_character_eq_zero χ hχ)
84 
85 /-- The endpoint bound applies to the actual ideal sum of each nontrivial
86 ordinary class character. This does not assert that its endpoint value is nonzero. -/
87 theorem characterMellin_sub_isBigO (χ : ClassGroup (𝓞 K) →* ℂ)
88     (hχ : χ ≠ 1) :
89     (fun h => classMellin K χ h - classMellin K χ 0)
90       =O[𝓝[>] (0 : ℝ)] (fun h : ℝ => h) :=
91   classMellin_sub_isBigO K χ (sum_character_eq_zero χ hχ)
92 
93 end PaperX.IdealClassCharacter

Back to source controls