English
Continuing the theme, the image of an inner regular measure under left multiplication is inner regular (alternative formulation).
Русский
Продолжение темы: образ при левом умножении сохраняет внутреннюю регулярность (альтернативная формулировка).
LaTeX
$$$ \text{InnerRegular}(\mu) \Rightarrow \text{InnerRegular}(\mathrm{map}(g * \cdot)(\mu)) $$$
Lean4
/-- Continuity of the measure of translates of a compact set: Given a compact set `k` in a
topological group, for `g` close enough to the origin, `μ (g • k \ k)` is arbitrarily small. -/
@[to_additive]
theorem eventually_nhds_one_measure_smul_diff_lt [LocallyCompactSpace G] [IsFiniteMeasureOnCompacts μ]
[InnerRegularCompactLTTop μ] {k : Set G} (hk : IsCompact k) (h'k : IsClosed k) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
∀ᶠ g in 𝓝 (1 : G), μ (g • k \ k) < ε :=
by
obtain ⟨U, hUk, hU, hμUk⟩ : ∃ (U : Set G), k ⊆ U ∧ IsOpen U ∧ μ U < μ k + ε := hk.exists_isOpen_lt_add hε
obtain ⟨V, hV1, hVkU⟩ : ∃ V ∈ 𝓝 (1 : G), V * k ⊆ U := compact_open_separated_mul_left hk hU hUk
filter_upwards [hV1] with g hg
calc
μ (g • k \ k) ≤ μ (U \ k) := by
gcongr
exact (smul_set_subset_smul hg).trans hVkU
_ < ε := measure_diff_lt_of_lt_add h'k.nullMeasurableSet hUk hk.measure_lt_top.ne hμUk
