Smooth compact parametrizations of the norm-one region

The parameter indexed by the distinguished infinite place is radial; the other infinite-place parameters are unit coordinates. Complex places contribute one angular parameter each. The total parameter count is the field degree.

@[reducible, inline]

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

The parameter space for radial charts of the number-field norm region.

Equations

• NairTenenbaum.NormRegionParameter K = (NumberField.InfinitePlace K ⊕ { w : NumberField.InfinitePlace K // w.IsComplex })

noncomputable def NairTenenbaum.normRegionUnitCoordinates (K : Type u_1) [Field K] [NumberField K] (v : NormRegionParameter K → ℝ) : NumberField.mixedEmbedding.realSpace K

Unit directions used in the radial parametrization of the norm region.

Equations

• NairTenenbaum.normRegionUnitCoordinates K v w = if w = NumberField.Units.dirichletUnitTheorem.w₀ then 0 else v (Sum.inl w)

noncomputable def NairTenenbaum.normRegionRadialChart (K : Type u_1) [Field K] [NumberField K] (σ : { w : NumberField.InfinitePlace K // w.IsReal } → Bool) (v : NormRegionParameter K → ℝ) : NumberField.mixedEmbedding.mixedSpace K

The radial chart associated with a norm-region parameter.

Equations

• One or more equations did not get rendered due to their size.

theorem NairTenenbaum.card_normRegionParameter (K : Type u_1) [Field K] [NumberField K] : Fintype.card (NormRegionParameter K) = Module.finrank ℚ K

theorem NairTenenbaum.contDiff_expMapBasis (K : Type u_1) [Field K] [NumberField K] : ContDiff ℝ ⊤ ↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis

theorem NairTenenbaum.contDiff_normRegionRadialChart (K : Type u_1) [Field K] [NumberField K] (σ : { w : NumberField.InfinitePlace K // w.IsReal } → Bool) : ContDiff ℝ ⊤ (normRegionRadialChart K σ)

theorem NairTenenbaum.normLeOne_frontier_radialChart (K : Type u_1) [Field K] [NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K} (hx : x ∈ frontier (NumberField.mixedEmbedding.fundamentalCone.normLeOne K)) : ∃ (σ : { w : NumberField.InfinitePlace K // w.IsReal } → Bool), ∃ v ∈ Set.Icc (fun (x : NormRegionParameter K) => 0) fun (x : NormRegionParameter K) => 1, normRegionRadialChart K σ v = x ∧ ∃ (w : NumberField.InfinitePlace K), v (Sum.inl w) = 0 ∨ v (Sum.inl w) = 1