NormSignResidueCounting.lean

1 import PaperX.NormSignGeometry
2 import PaperX.ResidueLatticeIdeal
3 import PaperX.ResidueLatticeWeights
4 
5 /-! Actual additive residue counts in each sign portion of the number-field cone. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperX.NormSignGeometry
9 open Set MeasureTheory Module Ideal
10 open NumberField NumberField.mixedEmbedding NumberField.mixedEmbedding.euclidean
11 open PaperX.IdealClassQuantitative PaperX.ResidueLattice
12 open scoped nonZeroDivisors Classical Pointwise
13 
14 variable (K : Type*) [Field K] [NumberField K]
15 
16 /-- The actual sign portion, in the Euclidean mixed coordinates used for ideal lattices. -/
17 def signRegion (positive : Bool) : Set (euclidean.mixedSpace K) :=
18   toMixed K ⁻¹' signCone K positive
19 
20 theorem signRegion_measurable (positive : Bool) : MeasurableSet (signRegion K positive) :=
21   (toMixed K).continuous.measurable (signCone_measurable K positive)
22 
23 theorem signRegion_bounded (positive : Bool) : Bornology.IsBounded (signRegion K positive) :=
24   (toMixed K).antilipschitz.isBounded_preimage (signCone_bounded K positive)
25 
26 /-- The sign-region boundary atlas in any basis of an actual ideal lattice. -/
27 theorem nonempty_signRegionAtlas (M : (Ideal (𝓞 K))⁰) {ι : Type*} [Fintype ι]
28     (b : Basis ι ℤ (idealEuclideanLattice K M)) (positive : Bool) :
29     Nonempty (LatticeCounting.LipschitzBoundaryAtlas ι
30       (LatticeCountingTransport.coordinates (idealEuclideanLattice K M) b ''
31         signRegion K positive)) := by
32   let e := (toMixed K).symm.trans
33     (LatticeCountingTransport.coordinates (idealEuclideanLattice K M) b)
34   have h := signConeAtlas K e (ideal_basis_card K b) positive
35   apply Nonempty.intro
36   convert h using 1
37   rw [signRegion, ← (toMixed K).image_symm_eq_preimage, ← Set.image_comp]
38   rfl
39 
40 /-- Actual additive residue points with a prescribed real norm sign. -/
41 def signFiberCount (M J : (Ideal (𝓞 K))⁰) (positive : Bool)
42     (c : IdealResidues K M J) (t : ℝ) : ℕ :=
43   fiberCount (idealEuclideanLattice K M) (idealEuclideanLattice K J)
44     (signRegion K positive) c t
45 
46 /-- Every residue has the same sign-region density; the constant is uniform in the residue. -/
47 theorem exists_signFiber_bound {M J : (Ideal (𝓞 K))⁰}
48     (h : (M : Ideal (𝓞 K)) ≤ J) (positive : Bool) :
49     ∃ B : ℝ, 0 ≤ B ∧ ∀ (c : IdealResidues K M J) (t : ℝ), 1 ≤ t →
50       |(signFiberCount K M J positive c t : ℝ) -
51         t ^ Module.finrank ℚ K *
52           ((volume.real (signRegion K positive) / ZLattice.covolume (idealEuclideanLattice K J)) /
53             Nat.card (IdealResidues K M J))| ≤
54         B * (t ^ (Module.finrank ℚ K - 1) + 1) := by
55   let b := Module.Free.chooseBasis ℤ (idealEuclideanLattice K M)
56   obtain ⟨A⟩ := nonempty_signRegionAtlas K M b positive
57   obtain ⟨B, hB0, hB⟩ := exists_fiber_discrepancy_bound
58     (idealEuclideanLattice K M) (idealEuclideanLattice K J) (idealLattice_mono K h) b
59     (signRegion_measurable K positive) (signRegion_bounded K positive) A
60   refine ⟨B, hB0, fun c t ht => ?_⟩
61   simpa only [ideal_basis_card K b, signFiberCount] using hB c t ht
62 
63 /-- Zero-mean finite residue weights have a surface-order bound separately on each sign region. -/
64 theorem exists_sign_zeroMean_bound {M J : (Ideal (𝓞 K))⁰}
65     (h : (M : Ideal (𝓞 K)) ≤ J) [Fintype (IdealResidues K M J)] (positive : Bool) :
66     ∃ B : ℝ, 0 ≤ B ∧ ∀ (w : IdealResidues K M J → ℂ), (∑ c : IdealResidues K M J, w c) = 0 →
67       ∀ t : ℝ, 1 ≤ t →
68         ‖weightedFiberCount (idealEuclideanLattice K M) (idealEuclideanLattice K J)
69           (signRegion K positive) w t‖ ≤
70           (∑ c : IdealResidues K M J, ‖w c‖) * B * (t ^ (Module.finrank ℚ K - 1) + 1) := by
71   let b := Module.Free.chooseBasis ℤ (idealEuclideanLattice K M)
72   obtain ⟨A⟩ := nonempty_signRegionAtlas K M b positive
73   obtain ⟨B, hB0, hB⟩ := exists_zeroMean_weightedFiber_bound
74     (idealEuclideanLattice K M) (idealEuclideanLattice K J) (idealLattice_mono K h) b
75     (signRegion_measurable K positive) (signRegion_bounded K positive) A
76   refine ⟨B, hB0, fun w hw t ht => ?_⟩
77   simpa only [ideal_basis_card K b, weightedFiberCount] using hB w hw t ht
78 
79 end PaperX.NormSignGeometry

Back to source controls