Documentation

TauCeti.Analysis.Convex.L1Ball

The finite-dimensional ℓ¹ unit ball #

The set l1Ball ι is the closed ℓ¹ unit ball on ι → ℝ, equipped with its usual supremum norm and product volume. It is a compact, symmetric, convex neighborhood of zero, its gauge is the sum of the absolute coordinates, and its volume is 2 ^ n / n!, where n is the cardinality of ι. The statements include the empty index type.

These facts provide a convex body for lattice estimates in coordinate spaces, including the logarithmic space of a number field. The geometry uses Mathlib's PiLp closed ball; the volume specializes MeasureTheory.volume_sum_rpow_le to exponent one.

source
def TauCeti.l1Ball (ι : Type u_1) [Fintype ι] :
Set (ι → ℝ)

The closed ℓ¹ unit ball in a finite real coordinate space.

Instances For
    source
    @[simp]
    theorem TauCeti.mem_l1Ball (ι : Type u_1) [Fintype ι] (x : ι → ℝ) :
    x ∈ l1Ball ι ↔ ∑ i : ι, |x i| ≤ 1

    Membership in the ℓ¹ unit ball is a bound on the sum of absolute coordinates.

    source
    theorem TauCeti.convex_l1Ball (ι : Type u_1) [Fintype ι] :
    Convex ℝ (l1Ball ι)

    The ℓ¹ unit ball is convex.

    source
    theorem TauCeti.neg_mem_l1Ball (ι : Type u_1) [Fintype ι] (x : ι → ℝ) :
    -x ∈ l1Ball ι ↔ x ∈ l1Ball ι

    The ℓ¹ unit ball is symmetric about zero.

    source
    theorem TauCeti.isCompact_l1Ball (ι : Type u_1) [Fintype ι] :
    IsCompact (l1Ball ι)

    The ℓ¹ unit ball is compact, including in dimension zero.

    source
    theorem TauCeti.isClosed_l1Ball (ι : Type u_1) [Fintype ι] :
    IsClosed (l1Ball ι)

    The ℓ¹ unit ball is closed.

    source
    theorem TauCeti.isBounded_l1Ball (ι : Type u_1) [Fintype ι] :
    Bornology.IsBounded (l1Ball ι)

    The ℓ¹ unit ball is bounded in the ambient supremum norm.

    source
    theorem TauCeti.zero_mem_interior_l1Ball (ι : Type u_1) [Fintype ι] :
    0 ∈ interior (l1Ball ι)

    Zero is an interior point of the ℓ¹ unit ball.

    source
    theorem TauCeti.absorbent_l1Ball (ι : Type u_1) [Fintype ι] :
    Absorbent ℝ (l1Ball ι)

    The ℓ¹ unit ball absorbs every vector.

    source
    theorem TauCeti.gauge_l1Ball (ι : Type u_1) [Fintype ι] (x : ι → ℝ) :
    gauge (l1Ball ι) x = ∑ i : ι, |x i|

    The gauge of the ℓ¹ unit ball is the sum of absolute coordinates.

    source
    theorem TauCeti.volume_l1Ball (ι : Type u_1) [Fintype ι] :
    MeasureTheory.volume (l1Ball ι) = ENNReal.ofReal (2 ^ Fintype.card ι / ↑(Fintype.card ι).factorial)

    The ℓ¹ unit ball has volume 2 ^ n / n! in dimension n, also when n = 0.