A Lipschitz parametrization of the frontier of the ray fundamental domain

TauCeti.NumberTheory.GeometryOfNumbers.LatticePointCount counts lattice points in a dilated region with a power-saving error term, but only for regions whose frontier is Lipschitz parametrizable in codimension one. NormLeOneLipschitz discharges that hypothesis for Mathlib's normLeOne K, the norm-≤-one section of the fundamental cone. This file lifts it to the section rayFundamentalDomain 𝔪 ∩ {x | mixedEmbedding.norm x ≤ 1} of the ray fundamental domain of an arbitrary modulus, which is the region whose lattice points count the algebraic integers in a fixed ray class.

rayFundamentalDomain_inter_normLeOne_eq presents that section as posRegion 𝔪 ∩ A, where A = ⋃ q, rayUnitRepresentative 𝔪 q • normLeOne K is a finite union of unit translates: the unit action preserves the mixed norm, so it commutes with the norm condition.

The two factors are of opposite character. A is bounded, with a complicated boundary; posRegion 𝔪 is an unbounded finite intersection of open half spaces, with a boundary made of hyperplanes. So the naive frontier (A ∩ B) ⊆ frontier A ∪ frontier B is useless here: the frontier of posRegion 𝔪 is unbounded, and a Lipschitz-parametrizable set is a finite union of Lipschitz images of a compact cube, hence bounded — so that union is parametrizable in no dimension whatsoever. Mathlib's sharp form frontier_inter_subset keeps each frontier paired with the closure of the other factor, and that pairing is what makes the argument work:

• frontier A ∩ closure (posRegion 𝔪) lies in frontier A, which lies in the union of the frontiers of the finitely many translates; each frontier (u • normLeOne K) is a Lipschitz image of frontier (normLeOne K), because a unit acts by a homeomorphism;
• closure A ∩ frontier (posRegion 𝔪) is a bounded subset of finitely many coordinate hyperplanes, and a bounded subset of a hyperplane is Lipschitz parametrizable in codimension one (TauCeti.IsLipschitzParametrizable.of_isBounded_of_subset_ker).

Main results

• TauCeti.GlobalNumberFields.isLipschitzParametrizable_frontier_rayFundamentalDomain: the norm-≤-one section of the ray fundamental domain is bounded and measurable, and its frontier is Lipschitz parametrizable in dimension finrank ℝ (mixedSpace K) - 1, which is [K:ℚ] - 1 by mixedEmbedding.finrank. These are exactly the three hypotheses the lattice-point count with a power-saving error consumes, so they are stated together;
• TauCeti.GlobalNumberFields.isBounded_rayFundamentalDomain_inter_normLeOne and TauCeti.GlobalNumberFields.measurableSet_rayFundamentalDomain_inter_normLeOne: the first two conclusions on their own, for callers that need only one of them;
• TauCeti.GlobalNumberFields.rayFundamentalDomain_inter_normLeOne_eq: that section is the positivity region cut by a finite union of unit translates of normLeOne K;
• TauCeti.GlobalNumberFields.frontier_posRegion_subset: the frontier of the positivity region lies in the coordinate hyperplanes prescribed by the infinite part of the modulus.

References

• C. Birkbeck, AINTLIB at commit db14b34cc5e3d79603e67c205dfa86b7b989000c (Apache-2.0), projects/Chebotarev/CebotarevDensity/ForMathlib/IdealCongruenceCount.lean, which carries out the same argument for a sign orthant cut out of a bounded region of ι → ℝ: frontier_posRegion_subset here is that file's frontier_signOrthant_subset, and isLipschitzParametrizable_frontier_rayFundamentalDomain follows its exists_frontier_cover_inter_orthant, including the use of frontier_inter_subset to pair each frontier with the other factor's closure. The bounded hyperplane pieces are handled here by the general TauCeti.IsLipschitzParametrizable.of_isBounded_of_subset_ker rather than by that file's explicit slab chart exists_lipschitz_cube_cover_hyperplane_slab.

theorem TauCeti.GlobalNumberFields.frontier_posRegion_subset {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : frontier (posRegion 𝔪) ⊆ ⋃ w ∈ 𝔪.infinitePart, {x : NumberField.mixedEmbedding.mixedSpace K | x.1 w = 0}

The frontier of the positivity region lies in the prescribed coordinate hyperplanes. The region is cut out by finitely many strict inequalities, so a boundary point satisfies all of them non-strictly yet must fail one of them: that coordinate vanishes. Mathlib's frontier_lt_subset_eq is the single-inequality case; the content here is that a finite intersection of such regions still confines its frontier to those level sets.

theorem TauCeti.GlobalNumberFields.rayFundamentalDomain_inter_normLeOne_eq {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : rayFundamentalDomain 𝔪 ∩ {x : NumberField.mixedEmbedding.mixedSpace K | NumberField.mixedEmbedding.norm x ≤ 1} = posRegion 𝔪 ∩ ⋃ (q : (NumberField.RingOfIntegers K)ˣ ⧸ unitsCongruenceSubgroupSupTorsion 𝔪), rayUnitRepresentative 𝔪 q • NumberField.mixedEmbedding.fundamentalCone.normLeOne K

The norm-≤-one section of the ray fundamental domain, as the positivity region cut by a finite union of unit translates of Mathlib's norm-≤-one region. The unit action preserves the mixed norm, so it commutes with the norm condition.

theorem TauCeti.GlobalNumberFields.isBounded_rayFundamentalDomain_inter_normLeOne {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : Bornology.IsBounded (rayFundamentalDomain 𝔪 ∩ {x : NumberField.mixedEmbedding.mixedSpace K | NumberField.mixedEmbedding.norm x ≤ 1})

The norm-≤-one section of the ray fundamental domain is bounded. It is carved out of a finite union of unit translates of Mathlib's norm-≤-one region, and each translate is bounded because the unit acts by a Lipschitz map.

theorem TauCeti.GlobalNumberFields.measurableSet_rayFundamentalDomain_inter_normLeOne {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : MeasurableSet (rayFundamentalDomain 𝔪 ∩ {x : NumberField.mixedEmbedding.mixedSpace K | NumberField.mixedEmbedding.norm x ≤ 1})

The norm-≤-one section of the ray fundamental domain is measurable: the domain itself is measurable and the mixed norm is continuous.

theorem TauCeti.GlobalNumberFields.isLipschitzParametrizable_frontier_rayFundamentalDomain {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : Bornology.IsBounded (rayFundamentalDomain 𝔪 ∩ {x : NumberField.mixedEmbedding.mixedSpace K | NumberField.mixedEmbedding.norm x ≤ 1}) ∧ MeasurableSet (rayFundamentalDomain 𝔪 ∩ {x : NumberField.mixedEmbedding.mixedSpace K | NumberField.mixedEmbedding.norm x ≤ 1}) ∧ IsLipschitzParametrizable (Module.finrank ℝ (NumberField.mixedEmbedding.mixedSpace K) - 1) (frontier (rayFundamentalDomain 𝔪 ∩ {x : NumberField.mixedEmbedding.mixedSpace K | NumberField.mixedEmbedding.norm x ≤ 1}))

The norm-≤-one section of the ray fundamental domain is bounded and measurable, and its frontier is Lipschitz parametrizable in codimension one. The first and third conclusions are exactly the two hypotheses hDb and hDfr of TauCeti.exists_abs_ncard_smul_inter_vadd_sub_le, the lattice-point count with a power-saving error, applied to the region counting the algebraic integers of a fixed ray class; the second is what gives that region a measure at all. This is the analogue, for an arbitrary modulus, of isLipschitzParametrizable_frontier_normLeOne for the trivial one, whose ray fundamental domain is Mathlib's fundamental cone.

The section is posRegion 𝔪 intersected with finitely many unit translates of normLeOne K. The translates are bounded and each has a frontier that is a Lipschitz image of frontier (normLeOne K); the positivity region is unbounded, but frontier_inter_subset pairs its frontier with the closure of the translates, so the piece it contributes is a bounded subset of the finitely many coordinate hyperplanes prescribed by the infinite part of 𝔪.