Radial and unit-coordinate faces of the norm-one region

Every boundary point has radial coordinate zero or one, or a unit coordinate at an endpoint. This isolates the lower-dimensional parameter faces before introducing signs and complex angles.

theorem NairTenenbaum.normLeOne_interior_of_radial_coordinates (K : Type u_1) [Field K] [NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K} {r : ℝ} {u : NumberField.mixedEmbedding.realSpace K} (hr0 : 0 < r) (hr1 : r < 1) (hu0 : u NumberField.Units.dirichletUnitTheorem.w₀ = 0) (hu : ∀ (w : NumberField.InfinitePlace K), w ≠ NumberField.Units.dirichletUnitTheorem.w₀ → 0 < u w ∧ u w < 1) (hx : NumberField.mixedEmbedding.normAtAllPlaces x = r • ↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis u) : x ∈ interior (NumberField.mixedEmbedding.fundamentalCone.normLeOne K)

theorem NairTenenbaum.normLeOne_frontier_radial_faces (K : Type u_1) [Field K] [NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K} (hx : x ∈ frontier (NumberField.mixedEmbedding.fundamentalCone.normLeOne K)) : ∃ (r : ℝ) (u : NumberField.mixedEmbedding.realSpace K), r ∈ Set.Icc 0 1 ∧ u NumberField.Units.dirichletUnitTheorem.w₀ = 0 ∧ (∀ (w : NumberField.InfinitePlace K), w ≠ NumberField.Units.dirichletUnitTheorem.w₀ → u w ∈ Set.Icc 0 1) ∧ NumberField.mixedEmbedding.normAtAllPlaces x = r • ↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis u ∧ (r = 0 ∨ r = 1 ∨ ∃ (w : NumberField.InfinitePlace K), w ≠ NumberField.Units.dirichletUnitTheorem.w₀ ∧ (u w = 0 ∨ u w = 1))