While this submission is a draft, it cannot be used by other submissions.

Proof of `The Bernstein index is the index of compactness` (1st statement)

groundedproofs/Lax606786Proofs/CompactnessIndexLimit.lean · lax-606786

What this proof establishes

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitLab

Description

The upper bound is ‖T‖c≤Ckρk(T)‖T‖_c ≤ C_k ρ_k(T) for each kk. For the lower bound, Kingman's theorem is applied to covering radii of the image of the unit ball, which are measurable and subadditive and lie below ‖⋅‖c‖·‖_c; the compactness seminorm itself is not known to be measurable in ωω. The counting argument of Lemma 34 of Lee (2024) then compares the two.