NormResidueExactScalarCriterion.lean

1 import PaperX.NormResidueAutomaticCounting
2 
3 /-!
4 # Exact scalar-norm witness criterion
5 
6 Degree--totient coprimality is a convenient sufficient condition for a scalar
7 unit witness, but it is stronger than necessary.  The exact scalar criterion is
8 simply the existence of a residue unit `a` on which the character is nontrivial
9 after the field-degree power map.  This module exposes that weaker hypothesis
10 and keeps automatic inverse-class representative selection.
11 -/
12 
13 set_option autoImplicit false
14 noncomputable section
15 
16 open Ideal NumberField MeasureTheory Filter Set Asymptotics
17 open scoped NumberField nonZeroDivisors Classical Topology
18 
19 namespace PaperX.NormResidue
20 
21 variable (K : Type*) [Field K] [NumberField K]
22 
23 /-- A scalar residue unit whose field-degree norm has nontrivial character value
24 is already the quotient-unit witness needed by the counting argument. -/
25 theorem exists_scalarResidueUnit_witness_of_scalar_power
26     (m : ℕ) (hm : m ≠ 0) (χ : ZMod m →*₀ ℂ)
27     (a : (ZMod m)ˣ)
28     (ha : χ ((a : ZMod m) ^ Module.finrank ℚ K) ≠ 1) :
29     ∃ u : (𝓞 K ⧸ modulusIdeal (𝓞 K) m)ˣ,
30       χ (integerQuotientNorm K m
31         (u : 𝓞 K ⧸ modulusIdeal (𝓞 K) m)) ≠ 1 := by
32   refine ⟨scalarResidueUnit K m hm a, ?_⟩
33   rw [integerQuotientNorm_scalarResidueUnit]
34   exact ha
35 
36 end PaperX.NormResidue
37 
38 namespace PaperX.NormResidueLattice
39 
40 open PaperX.NormResidue
41 open PaperX.IdealClassQuantitative PaperX.IdealNormWeighted
42 open PaperX.RealAxisMellinMoment
43 
44 variable (K : Type*) [Field K] [NumberField K]
45 
46 /-- Exact-scalar-criterion form of the norm-character power saving.  This drops
47 the degree--totient coprimality assumption when a direct scalar witness is
48 available. -/
49 theorem exists_classNormSum_bound_of_scalar_power_autoRep
50     (C : ClassGroup (𝓞 K)) (m : ℕ) (hm : m ≠ 0) (χ : ZMod m →*₀ ℂ)
51     (hpow : ∃ a : (ZMod m)ˣ,
52       χ ((a : ZMod m) ^ Module.finrank ℚ K) ≠ 1) :
53     ∃ B : ℝ, 0 ≤ B ∧ ∀ X : ℝ, 1 ≤ X →
54       ‖classNormSum K C (fun n => χ (n : ZMod m)) X‖ ≤
55         B * X ^ countExponent K := by
56   obtain ⟨J, hJ, hJcop⟩ :=
57     exists_coprime_inverse_class_representative K C m hm
58   obtain ⟨a, ha⟩ := hpow
59   obtain ⟨u, hu⟩ :=
60     exists_scalarResidueUnit_witness_of_scalar_power K m hm χ a ha
61   exact exists_classNormSum_bound_of_unit K hJ m hm χ u hu
62     (character_natCast_ne_zero_of_coprime m (absNorm (J : Ideal (𝓞 K))) χ hJcop)
63 
64 /-- Exact-scalar-criterion endpoint variation for the actual norm-character
65 Mellin factor. -/
66 theorem normCharacterMellin_sub_isBigO_of_scalar_power_autoRep
67     (C : ClassGroup (𝓞 K)) (m : ℕ) (hm : m ≠ 0) (χ : ZMod m →*₀ ℂ)
68     (hpow : ∃ a : (ZMod m)ˣ,
69       χ ((a : ZMod m) ^ Module.finrank ℚ K) ≠ 1) :
70     (fun h => normCharacterMellin K C m χ h - normCharacterMellin K C m χ 0)
71       =O[𝓝[>] (0 : ℝ)] (fun h : ℝ => h) := by
72   obtain ⟨B, _, hB⟩ :=
73     exists_classNormSum_bound_of_scalar_power_autoRep K C m hm χ hpow
74   exact mellinIntegral_sub_isBigO_of_power_bound
75     (measurable_classNormSum K C (fun n => χ (n : ZMod m))).aestronglyMeasurable
76     (PaperX.IdealClassCharacter.countExponent_lt_one K) (fun x hx => hB x hx.le)
77 
78 end PaperX.NormResidueLattice

Back to source controls