English
Even removing measurability from the closure condition, Haar-like equality persists for left-invariant measures under compact closure by InnerRegularTop assumptions.
Русский
Даже если убрать условие измеримости в отношении компактного замыкания, свойство Хааровской массы сохраняется для левых инвариантных мер при компактном замыкании по предположениям InnerRegularTop.
LaTeX
$$$$ μ' s = haarScalarFactor μ' μ · μ s, \\text{ for measurable } s, \\text{ closure }(s) \\text{ compact}. $$$$
Lean4
/-- Given an invariant measure then it gives the same mass to measurable sets with
compact closure as any other invariant measure, up to the scalar `haarScalarFactor μ' μ`.
Auxiliary lemma in the proof of the more general
`measure_isMulInvariant_eq_smul_of_isCompact_closure`, which removes the
measurability assumption. -/
@[to_additive measure_isAddInvariant_eq_smul_of_isCompact_closure_of_measurableSet /--
Given an invariant measure then it gives the same mass to measurable sets with
compact closure as any other invariant measure, up to the scalar `addHaarScalarFactor μ' μ`.
Auxiliary lemma in the proof of the more general
`measure_isAddInvariant_eq_smul_of_isCompact_closure`, which removes the
measurability assumption. -/
]
theorem measure_isMulInvariant_eq_smul_of_isCompact_closure_of_measurableSet [LocallyCompactSpace G] (μ' μ : Measure G)
[IsHaarMeasure μ] [IsFiniteMeasureOnCompacts μ'] [IsMulLeftInvariant μ'] {s : Set G} (hs : MeasurableSet s)
(h's : IsCompact (closure s)) : μ' s = haarScalarFactor μ' μ • μ s :=
by
let ν : Measure G := haar
have A : μ' s = haarScalarFactor μ' ν • ν s :=
measure_isMulInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop μ' ν hs h's
have B : μ s = haarScalarFactor μ ν • ν s :=
measure_isMulInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop μ ν hs h's
rw [A, B, smul_smul, haarScalarFactor_eq_mul μ' μ ν]
