English
The Haar index (K,V) counts the minimal number of left translates of V required to cover K; it is defined to be 0 if such a finite covering is impossible.
Русский
Индекс Хаара (K,V) равен минимальному числу левых переносов V, необходимых для покрытия K; если такого конечного покрытия нельзя достичь, индекс равен 0.
LaTeX
$$\\mathrm{haar.index}(K,V) = \\inf\\{ |t| : K \\subseteq \\bigcup_{g\\in t} (g * V) \\} \\, (\\text{над } \\mathbb{N})$$
Lean4
/-- The index or Haar covering number or ratio of `K` w.r.t. `V`, denoted `(K : V)`:
it is the smallest number of (left) translates of `V` that is necessary to cover `K`.
It is defined to be 0 if no finite number of translates cover `K`. -/
@[to_additive addIndex /-- additive version of `MeasureTheory.Measure.haar.index` -/
]
noncomputable def index (K V : Set G) : ℕ :=
sInf <| Finset.card '' {t : Finset G | K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}
