English
If μ is Haar on a commutative group G and n ≠ 0 is an integer, then the map g ↦ g^n is measure preserving with respect to μ.
Русский
Если μ — мера Хаара на коммутативной группе G и n ≠ 0, то отображение g ↦ g^n сохраняет меру μ.
LaTeX
$$$\\forall G \\; [CommGroup G] \\; [CompactSpace G] \\; [RootableBy G \\mathbb{Z}] \\; {n : \\mathbb{Z}}, n \\neq 0 \\, \\Rightarrow \\text{MeasurePreserving } (\\lambda g. g^n) \\ μ \\ μ$$
Lean4
/-- A bounded convergence theorem for a finite measure:
If bounded continuous non-negative functions are uniformly bounded by a constant and tend to a
limit, then their integrals against the finite measure tend to the integral of the limit.
This formulation assumes:
* the functions tend to a limit along a countably generated filter;
* the limit is in the almost everywhere sense;
* boundedness holds almost everywhere;
* integration is `MeasureTheory.lintegral`, i.e., the functions and their integrals are
`ℝ≥0∞`-valued.
-/
theorem tendsto_lintegral_nn_filter_of_le_const {ι : Type*} {L : Filter ι} [L.IsCountablyGenerated] (μ : Measure Ω)
[IsFiniteMeasure μ] {fs : ι → Ω →ᵇ ℝ≥0} {c : ℝ≥0} (fs_le_const : ∀ᶠ i in L, ∀ᵐ ω : Ω ∂μ, fs i ω ≤ c) {f : Ω → ℝ≥0}
(fs_lim : ∀ᵐ ω : Ω ∂μ, Tendsto (fun i ↦ fs i ω) L (𝓝 (f ω))) :
Tendsto (fun i ↦ ∫⁻ ω, fs i ω ∂μ) L (𝓝 (∫⁻ ω, f ω ∂μ)) :=
by
refine
tendsto_lintegral_filter_of_dominated_convergence (fun _ ↦ c)
(Eventually.of_forall fun i ↦ (ENNReal.continuous_coe.comp (fs i).continuous).measurable) ?_
(@lintegral_const_lt_top _ _ μ _ _ (@ENNReal.coe_ne_top c)).ne ?_
· simpa only [Function.comp_apply, ENNReal.coe_le_coe] using fs_le_const
· simpa only [Function.comp_apply, ENNReal.tendsto_coe] using fs_lim
