English
In a commutative locally compact group, every regular Haar measure is invariant under inversion.
Русский
В коммутативной локально компактной группе любая регулярная мера Хаара инвариантна относительно инверсии.
LaTeX
$$$\\forall G \\, [CommGroup G] \\, [TopologicalSpace G] \\, [IsTopologicalGroup G] \\, [MeasurableSpace G] \\, [BorelSpace G] \\, (μ : \\mathrm{Measure}(G)) \\, [\\text{Haar } μ] \\, [\\text{LocallyCompactSpace } G] \\, [\\text{Regular } μ] \\, IsInvInvariant μ$$
Lean4
/-- The integrals of thickened indicators of a closed set against a finite measure tend to the
measure of the closed set if the thickening radii tend to zero. -/
theorem tendsto_lintegral_thickenedIndicator_of_isClosed {Ω : Type*} [MeasurableSpace Ω] [PseudoEMetricSpace Ω]
[OpensMeasurableSpace Ω] (μ : Measure Ω) [IsFiniteMeasure μ] {F : Set Ω} (F_closed : IsClosed F) {δs : ℕ → ℝ}
(δs_pos : ∀ n, 0 < δs n) (δs_lim : Tendsto δs atTop (𝓝 0)) :
Tendsto (fun n ↦ lintegral μ fun ω ↦ (thickenedIndicator (δs_pos n) F ω : ℝ≥0∞)) atTop (𝓝 (μ F)) :=
by
apply
measure_of_cont_bdd_of_tendsto_indicator μ F_closed.measurableSet (fun n ↦ thickenedIndicator (δs_pos n) F)
fun n ω ↦ thickenedIndicator_le_one (δs_pos n) F ω
have key := thickenedIndicator_tendsto_indicator_closure δs_pos δs_lim F
rwa [F_closed.closure_eq] at key
