Documentation

TauCeti.NumberTheory.NumberField.Units.Log.Ball

The logarithmic ℓ¹ ball #

The closed ℓ¹ unit ball in the logarithmic space of a number field is a compact, symmetric, convex neighborhood of zero. Its gauge is the sum of the absolute values of the coordinates, and its volume in unit rank r is 2 ^ r / r!, including rank zero.

Together with the height comparison for the logarithmic embedding, this ball lets geometry of numbers produce fundamental units with a bounded product of heights. The norm on Mathlib's logSpace is the supremum norm, so this ball is not its metric unit ball. We use the finite-coordinate ball TauCeti.l1Ball for its geometry, gauge and product volume.

References #

source
noncomputable def TauCeti.NumberField.Units.logBall (K : Type u_1) [Field K] [NumberField K] :
Set (NumberField.Units.dirichletUnitTheorem.logSpace K)

The closed ℓ¹ unit ball in the logarithmic space of a number field.

Instances For
    source
    @[simp]
    theorem TauCeti.NumberField.Units.mem_logBall (K : Type u_1) [Field K] [NumberField K] (x : NumberField.Units.dirichletUnitTheorem.logSpace K) :
    x ∈ logBall K ↔ ∑ w : { w : NumberField.InfinitePlace K // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }, |x w| ≤ 1

    Membership in the logarithmic ball is the ℓ¹ bound on the coordinates.

    source
    theorem TauCeti.NumberField.Units.logBall_eq_l1Ball (K : Type u_1) [Field K] [NumberField K] :
    logBall K = l1Ball { w : NumberField.InfinitePlace K // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }

    The logarithmic ball is the ℓ¹ unit ball on the coordinates away from w₀.

    source
    theorem TauCeti.NumberField.Units.convex_logBall (K : Type u_1) [Field K] [NumberField K] :
    Convex ℝ (logBall K)

    The logarithmic ball is convex.

    source
    theorem TauCeti.NumberField.Units.neg_mem_logBall (K : Type u_1) [Field K] [NumberField K] (x : NumberField.Units.dirichletUnitTheorem.logSpace K) :
    -x ∈ logBall K ↔ x ∈ logBall K

    The logarithmic ball is symmetric about zero.

    source
    theorem TauCeti.NumberField.Units.isCompact_logBall (K : Type u_1) [Field K] [NumberField K] :
    IsCompact (logBall K)

    The logarithmic ball is compact, also when the unit rank is zero.

    source
    theorem TauCeti.NumberField.Units.isClosed_logBall (K : Type u_1) [Field K] [NumberField K] :
    IsClosed (logBall K)

    The logarithmic ball is closed.

    source
    theorem TauCeti.NumberField.Units.isBounded_logBall (K : Type u_1) [Field K] [NumberField K] :
    Bornology.IsBounded (logBall K)

    The logarithmic ball is bounded in the supremum norm on logSpace K.

    source
    theorem TauCeti.NumberField.Units.zero_mem_interior_logBall (K : Type u_1) [Field K] [NumberField K] :
    0 ∈ interior (logBall K)

    Zero is an interior point of the logarithmic ball.

    source
    theorem TauCeti.NumberField.Units.absorbent_logBall (K : Type u_1) [Field K] [NumberField K] :
    Absorbent ℝ (logBall K)

    The logarithmic ball absorbs every vector in the logarithmic space.

    source
    theorem TauCeti.NumberField.Units.gauge_logBall (K : Type u_1) [Field K] [NumberField K] (x : NumberField.Units.dirichletUnitTheorem.logSpace K) :
    gauge (logBall K) x = ∑ w : { w : NumberField.InfinitePlace K // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }, |x w|

    The gauge of the logarithmic ball is the ℓ¹ norm, rather than the ambient supremum norm.

    source
    theorem TauCeti.NumberField.Units.volume_logBall (K : Type u_1) [Field K] [NumberField K] :
    MeasureTheory.volume (logBall K) = ENNReal.ofReal (2 ^ NumberField.Units.rank K / ↑(NumberField.Units.rank K).factorial)

    The logarithmic ball has volume 2 ^ r / r! in unit rank r. In rank zero its volume is one, the volume of the whole zero-dimensional logarithmic space.