MATHLIBANNEX / CANONICAL DECLARATION CARD

A compact proper subset of a seminorm ball has smaller Haar measure

MathlibAnnex.SeminormBall.measure_lt

theorem

Finds a nonempty open part of the missing set and uses finiteness of the compact set to make the measure comparison strict.

Statement

Let be a real normed space with its Borel measurable structure, let be an additive Haar measure, and let be a continuous seminorm. Put . If is compact, then

Assumptions

The measure is an additive Haar measure: in particular it is finite on compact sets and positive on nonempty open sets. The seminorm is continuous for the given norm topology; it need not be definite. The set is compact, is contained in , and is not equal to . No convexity of , finite-dimensionality of , or finiteness of is added.

Conclusion

The measure inequality is strict in the extended nonnegative reals . Compactness ensures , while is allowed to be infinite.

The key geometric input is a nonempty interior of . It concerns the ambient norm topology, even when has a kernel. Taking gives the separately cited norm-ball specialization, without imposing convexity on .

Proof route

Choose . Compactness makes closed, so its complement contains a neighbourhood of . An inward point with sufficiently close to remains outside . By seminorm homogeneity,

Continuity of therefore makes a nonempty open subset of . Positivity of Haar measure on nonempty open sets implies . The sets and are measurable and disjoint, with union . Hence

where strictness uses , obtained from compactness. This reasoning remains valid if the second summand is infinite.

Proof steps

  1. To make the inward choice explicit, take with the open norm ball of radius about contained in . Set

    Then , so , and

    Thus . The strict inequality for supplies an interior point of ; intersecting its open neighbourhood with gives the nonempty open defect.

  2. The compact set is closed and Borel measurable. Continuity of makes closed and hence measurable, so its difference with is measurable. The containment gives the disjoint decomposition . Additivity and the finite compact measure now justify the strict inequality, without subtracting infinite measures.

Main citations

Lean source signature (exact)

theorem measure_lt
    [NormedAddCommGroup E] [NormedSpace ℝ E]
    [MeasurableSpace E] [BorelSpace E]
    (μ : Measure E) [Measure.IsAddHaarMeasure μ]
    (p : Seminorm ℝ E) (hp : Continuous p)
    {K : Set E} (hKcompact : IsCompact K)
    (hsub : K ⊆ p.closedBall 0 1) (hne : K ≠ p.closedBall 0 1) :
    μ K < μ (p.closedBall 0 1)
In the source Mathematical meaning
[NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] The real normed space carries its Borel measurable structure.
(μ : Measure E) [Measure.IsAddHaarMeasure μ] The additive Haar measure , finite on compact sets and positive on nonempty open sets.
(p : Seminorm ℝ E) (hp : Continuous p) The seminorm is continuous for the ambient norm topology; it may have a nontrivial kernel.
p.closedBall 0 1 The closed seminorm unit ball .
{K : Set E} (hKcompact : IsCompact K) The set is compact. This ensures ; it does not assert compactness of .
In the source Mathematical meaning
(hsub : K ⊆ p.closedBall 0 1) (hne : K ≠ p.closedBall 0 1) The containment and inequality together say .
μ K < μ (p.closedBall 0 1) The conclusion in . The right-hand measure may be infinite.
Exact surrounding binder context (separate excerpt) 
noncomputable section

open Set MeasureTheory
open scoped ENNReal

namespace MathlibAnnex

namespace SeminormBall

variable {E F : Type*}

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project

Exact content identity

Declaration: MathlibAnnex.SeminormBall.measure_lt

Accepted content SHA-256: cf91ef813d756e6a74e3bad4ef03ea2d2e828b67ce7a7e9ab4ff1ebd54f8c6c0

Accepted source guide SHA-256: c99001ecaddc5c97f3a2895ac44b059d204ed125a1e2c6ff7e5724147ae1b72a

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑