instRegularOfIsHaarMeasureOfCompactSpace

English

For a locally compact group, if μ' μ are Haar-like, then μ' s = haarScalarFactor μ' μ · μ s for all measurable s.

Русский

Для локально компактной группы, если μ' и μ подобны Хаару, тогда μ' s = haarScalarFactor μ' μ · μ s для всех измеримых s.

LaTeX

$$$$ μ'(s) = haarScalarFactor μ' μ · μ(s) $$$$

Lean4

@[to_additive]
instance (priority := 100) instRegularOfIsHaarMeasureOfCompactSpace [CompactSpace G] (μ : Measure G)
    [IsMulLeftInvariant μ] [IsFiniteMeasureOnCompacts μ] : Regular μ :=
  by
  rw [isMulInvariant_eq_smul_of_compactSpace μ haar]
  infer_instance

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