English
The weighted version of the index: prehaar(K0,U,K) = index(K,U) / index(K0,U).
Русский
Усильнённая верcия индекса: prehaar(K0,U,K) = индекс(K,U) / индекс(K0,U).
LaTeX
$$$\\mathrm{prehaar}(K_0,U,K) = \\dfrac{\\mathrm{index}(K,U)}{\\mathrm{index}(K_0,U)}$$$
Lean4
/-- `prehaar K₀ U K` is a weighted version of the index, defined as `(K : U)/(K₀ : U)`.
In the applications `K₀` is compact with non-empty interior, `U` is open containing `1`,
and `K` is any compact set.
The argument `K` is a (bundled) compact set, so that we can consider `prehaar K₀ U` as an
element of `haarProduct` (below). -/
@[to_additive /-- additive version of `MeasureTheory.Measure.haar.prehaar` -/
]
noncomputable def prehaar (K₀ U : Set G) (K : Compacts G) : ℝ :=
(index (K : Set G) U : ℝ) / index K₀ U
