English
A Haar measure image under a left action map is Haar.
Русский
Образ меры Хаара под отображением левого действия остаётся мерой Хаара.
LaTeX
$$$\text{IsHaarMeasure}(\text{Measure.map } (a \cdot \cdot)\, \mu)$$$
Lean4
/-- The image of a Haar measure under map of a left action is again a Haar measure. -/
@[to_additive /-- The image of a Haar measure under map of a left additive action is again a Haar measure -/
]
instance isHaarMeasure_map_smul {α} [BorelSpace G] [IsTopologicalGroup G] [Group α] [MulAction α G]
[SMulCommClass α G G] [MeasurableSpace α] [MeasurableSMul α G] [ContinuousConstSMul α G] (a : α) :
IsHaarMeasure (Measure.map (a • · : G → G) μ)
where
toIsMulLeftInvariant := isMulLeftInvariant_map_smul _
lt_top_of_isCompact K
hK := by
let F := (Homeomorph.smul a (α := G)).toMeasurableEquiv
change map F μ K < ∞
rw [F.map_apply K]
exact IsCompact.measure_lt_top <| (Homeomorph.isCompact_preimage (Homeomorph.smul a)).2 hK
toIsOpenPosMeasure := (continuous_const_smul a).isOpenPosMeasure_map (MulAction.surjective a)
