Lipschitz boundary charts and quantitative counting for the norm-one region

Restricting the smooth radial parametrizations to coordinate faces gives finitely many charts with field-degree-minus-one parameters. The general lattice-counting theorem applies after any real linear change of coordinates.

@[reducible, inline]

abbrev NairTenenbaum.NormRegionBoundaryIndex (K : Type u_1) [Field K] : Type u_1

The index set for the boundary charts of the norm region.

Equations

• NairTenenbaum.NormRegionBoundaryIndex K = (({ w : NumberField.InfinitePlace K // w.IsReal } → Bool) × NumberField.InfinitePlace K × Bool)

noncomputable def NairTenenbaum.normRegionBoundaryChart (K : Type u_1) [Field K] [NumberField K] (j : NormRegionBoundaryIndex K) (v : Fin (Fintype.card (NormRegionParameter K) - 1) → ℝ) : NumberField.mixedEmbedding.mixedSpace K

A chart covering one piece of the norm-region boundary.

Equations

• NairTenenbaum.normRegionBoundaryChart K j v = NairTenenbaum.normRegionRadialChart K j.1 (NairTenenbaum.cubeFaceMap (Sum.inl j.2.1) (if j.2.2 = true then 1 else 0) v)

theorem NairTenenbaum.contDiff_normRegionBoundaryChart (K : Type u_1) [Field K] [NumberField K] (j : NormRegionBoundaryIndex K) : ContDiff ℝ ⊤ (normRegionBoundaryChart K j)

theorem NairTenenbaum.normLeOne_frontier_boundaryChart (K : Type u_1) [Field K] [NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K} (hx : x ∈ frontier (NumberField.mixedEmbedding.fundamentalCone.normLeOne K)) : ∃ (j : NormRegionBoundaryIndex K), ∃ v ∈ Set.Icc (fun (x : Fin (Fintype.card (NormRegionParameter K) - 1)) => 0) fun (x : Fin (Fintype.card (NormRegionParameter K) - 1)) => 1, normRegionBoundaryChart K j v = x

theorem NairTenenbaum.exists_coordinate_normLeOne_lattice_error (K : Type u_1) [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] (e : NumberField.mixedEmbedding.mixedSpace K ≃L[ℝ] ι → ℝ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (t : ℝ), 1 ≤ t → |↑(integerLatticeCount (t • ⇑e '' NumberField.mixedEmbedding.fundamentalCone.normLeOne K)) - t ^ Fintype.card ι * MeasureTheory.volume.real (⇑e '' NumberField.mixedEmbedding.fundamentalCone.normLeOne K)| ≤ C * t ^ (Module.finrank ℚ K - 1)