haarProduct — Mathlib

English

For a fixed K0, haarProduct(K0) is the product over compact sets K of the intervals [0, index(K,K0)].

Русский

Для фиксированного K0 Haar-продукт задаётся как произведение по всем компакт-множестам K интервалов [0, index(K,K0)].

LaTeX

$$$\\text{haarProduct}(K_0) = \\pi_{K} \\; Icc\\,0\\;\\big(\\operatorname{index}(K,V)\\big)$$$

Lean4

/-- `haarProduct K₀` is the product of intervals `[0, (K : K₀)]`, for all compact sets `K`.
  For all `U`, we can show that `prehaar K₀ U ∈ haarProduct K₀`. -/
@[to_additive /-- additive version of `MeasureTheory.Measure.haar.haarProduct` -/
    ]
def haarProduct (K₀ : Set G) : Set (Compacts G → ℝ) :=
  pi univ fun K => Icc 0 <| index (K : Set G) K₀

Похожие утверждения