A Lipschitz parametrization of the frontier of the norm-≤-one region

TauCeti.NumberTheory.GeometryOfNumbers.LatticePointCount counts lattice points in a dilated region with a power-saving error, but only for regions whose frontier is Lipschitz parametrizable: exists_abs_ncard_smul_inter_vadd_sub_le takes IsLipschitzParametrizable (finrank ℝ E - 1) (frontier D) as a hypothesis. Mathlib proves that frontier (normLeOne K) is null (volume_frontier_normLeOne), which is what a rate-free limit needs and is strictly weaker: a null frontier does not provide a quantitative or power-saving error bound.

This file discharges that hypothesis for normLeOne K. Mathlib presents the region through expMapBasis, a partial homeomorphism of realSpace K whose image of the box paramSet K = univ.pi fun w ↦ if w = w₀ then Iic 0 else Ico 0 1 is the norm-≤-one region up to normAtAllPlaces. The frontier of a box is the union of its faces, so a Lipschitz cover of the image reduces to parametrizing the image of each face — which is what the maps here do.

The w₀ face is where the unbounded Iic 0 direction is pinned at its endpoint; the side faces pin one of the bounded Ico 0 1 directions, and there the substitution t = exp (x w₀) turns the unbounded direction into the freed cube coordinate.

Main results

• isLipschitzParametrizable_frontier_normLeOne: the frontier of normLeOne K is Lipschitz parametrizable in dimension finrank ℝ (mixedSpace K) - 1, one less than that of the mixed space.
• frontier_normLeOne_subset_preimage: that frontier lies over the frontier of the box image, through normAtAllPlaces.
• isLipschitzParametrizable_frontier_image_paramSet: the frontier of the box image is Lipschitz parametrizable in dimension rank K, one less than that of realSpace K.
• contDiff_expMapBasis: the box parametrization is smooth.
• closure_image_paramSet_subset: the closure of the box image adds only the origin.
• frontier_image_paramSet_subset: the frontier of the box image lies in the image of the box's frontier, together with the origin.

The face maps that decompose the box's frontier, the lifts that cover the fibres of normAtAllPlaces, and the lemmas supporting them, are private: they implement the parametrization and are not independently reusable.

References

• C. Birkbeck, AINTLIB at commit db14b34cc5e3d79603e67c205dfa86b7b989000c (Apache-2.0), projects/Chebotarev/CebotarevDensity/ForMathlib/NormLeOneLipschitz.lean, from which the face decomposition is adapted: faceMapZero, faceMapSide, contDiff_faceMapZero, contDiff_faceMapSide, frontier_image_subset_of_closure_subset and frontier_image_paramSet_subset follow that file's declarations of the same names. isLipschitzParametrizable_frontier_normLeOne is that file's normLeOne_frontier_lipschitz_cover, and the circle direction of liftMap follows its lipschitzWith_exp_ofReal_mul_I; the sign and angle bookkeeping is arranged differently here, through a single globally C¹ lift rather than that file's cubeRelabel scaffolding.

theorem NumberField.mixedEmbedding.fundamentalCone.contDiff_expMapBasis (K : Type u_1) [Field K] [NumberField K] {n : WithTop ℕ∞} : ContDiff ℝ n ↑expMapBasis

expMapBasis is C^n for every n: it is an exponential in the w₀ coordinate times a product of real powers of the positive reals w (fundSystem ...) in the others.

theorem NumberField.mixedEmbedding.fundamentalCone.closure_image_paramSet_subset (K : Type u_1) [Field K] [NumberField K] : closure (↑expMapBasis '' paramSet K) ⊆ ↑expMapBasis '' closure (paramSet K) ∪ {0}

The closure of the box image adds only the origin. The origin is what the w₀ coordinate escapes to as it runs to -∞, and it is the sole reason the closure of the image is not the image of the closure.

theorem NumberField.mixedEmbedding.fundamentalCone.frontier_image_paramSet_subset (K : Type u_1) [Field K] [NumberField K] : frontier (↑expMapBasis '' paramSet K) ⊆ ↑expMapBasis '' frontier (paramSet K) ∪ {0}

The frontier of the box image lies in the image of the box boundary, plus the origin. This is the reduction the Lipschitz cover runs on: the boundary of a product of intervals is a finite union of faces, so parametrizing it reduces to parametrizing each face.

theorem NumberField.mixedEmbedding.fundamentalCone.isLipschitzParametrizable_frontier_image_paramSet (K : Type u_1) [Field K] [NumberField K] : TauCeti.IsLipschitzParametrizable (Units.rank K) (frontier (↑expMapBasis '' paramSet K))

The frontier of the box image is Lipschitz parametrizable in codimension one. This is the hypothesis TauCeti.IsLipschitzParametrizable.exists_ncard_smul_add_inter_le needs to turn a lattice-point count into a count with a power-saving error term; Mathlib's volume_frontier_normLeOne gives only that the frontier is null, which yields a rate-free asymptotic but no quantitative error bound.

The dimension is rank K = #(InfinitePlace K) - 1, one less than that of realSpace K.

theorem NumberField.mixedEmbedding.fundamentalCone.frontier_normLeOne_subset_preimage (K : Type u_1) [Field K] [NumberField K] : frontier (normLeOne K) ⊆ normAtAllPlaces ⁻¹' frontier (↑expMapBasis '' paramSet K)

The frontier of the norm-≤-one region sits over the frontier of the box image. normLeOne K is the preimage of expMapBasis '' paramSet K under the continuous normAtAllPlaces, and the frontier of a preimage lies in the preimage of the frontier.

theorem NumberField.mixedEmbedding.fundamentalCone.isLipschitzParametrizable_frontier_normLeOne (K : Type u_1) [Field K] [NumberField K] : TauCeti.IsLipschitzParametrizable (Module.finrank ℝ (mixedSpace K) - 1) (frontier (normLeOne K))

The frontier of the norm-≤-one region is Lipschitz parametrizable in codimension one. This discharges the boundary hypothesis of TauCeti.exists_abs_ncard_smul_inter_vadd_sub_le for normLeOne K, whose frontier Mathlib knows only to be null (volume_frontier_normLeOne) — a null frontier supports a rate-free limit but gives no quantitative or power-saving error bound.

The frontier lies over the frontier of the box image, which is parametrizable in dimension rank K; each fibre of normAtAllPlaces adds the r₂ angles at the complex places and a choice of sign at each of the r₁ real places, and rank K + r₂ = finrank ℝ (mixedSpace K) - 1.