English
Let G be a locally compact group and μ be a left-invariant measure with μ finite on compacts and inner regular. For a compact k that is closed, the measure of the translate-difference g k \ k tends to 0 as g tends to the identity.
Русский
Пусть G — локально компактная группа, μ — лево-инвариантная мера, конечная на компактных множествах и внутри-регулярная. Пусть k — компактное множество, что является замкнутым. Тогда μ(g · k \ k) → 0 при g → 1.
LaTeX
$$$\displaystyle \text{Tendsto}\bigl(g \mapsto \mu(g \cdot k \setminus k)\bigr)\left(\mathcal{N}(1)\right) = \mathcal{N}(0)\quad\text{(for } k \text{ compact, closed)}$$$
Lean4
/-- Continuity of the measure of translates of a compact set:
Given a closed compact set `k` in a topological group,
the measure of `g • k \ k` tends to zero as `g` tends to `1`. -/
@[to_additive]
theorem tendsto_measure_smul_diff_isCompact_isClosed [LocallyCompactSpace G] [IsFiniteMeasureOnCompacts μ]
[InnerRegularCompactLTTop μ] {k : Set G} (hk : IsCompact k) (h'k : IsClosed k) :
Tendsto (fun g : G ↦ μ (g • k \ k)) (𝓝 1) (𝓝 0) :=
ENNReal.nhds_zero_basis.tendsto_right_iff.mpr <| fun _ h ↦ eventually_nhds_one_measure_smul_diff_lt hk h'k h.ne'
