English
This is a simple version of the Unfolding Trick: the integral of a function f on G with respect to a right-invariant measure μ equals the integral over the quotient G/Γ of the automorphization of f with respect to the restricted measure μ_𝓕.
Русский
Это простая версия разворачивающего приема: интеграл функции f по G по мере μ совпадает с интегралом по фактор-пространству G/Γ от автоморфизованной функции f по мере μ_𝓕.
LaTeX
$$$$\\int_G f \\; dμ = \\int_{G/Γ} \\mathrm{automorphize} f \\; dμ_𝓕.$$$$
Lean4
/-- This is a simple version of the **Unfolding Trick**: Given a subgroup `Γ` of a group `G`, the
integral of a function `f` on `G` with respect to a right-invariant measure `μ` is equal to the
integral over the quotient `G ⧸ Γ` of the automorphization of `f`. -/
@[to_additive /-- This is a simple version of the **Unfolding Trick**: Given a subgroup `Γ` of an
additive group `G`, the integral of a function `f` on `G` with respect to a right-invariant
measure `μ` is equal to the integral over the quotient `G ⧸ Γ` of the automorphization of `f`. -/
]
theorem integral_eq_integral_automorphize {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [μ.IsMulRightInvariant]
{f : G → E} (hf₁ : Integrable f μ) (hf₂ : AEStronglyMeasurable (automorphize f) μ_𝓕) :
∫ x : G, f x ∂μ = ∫ x : G ⧸ Γ, automorphize f x ∂μ_𝓕 :=
by
calc
∫ x : G, f x ∂μ = ∑' γ : Γ.op, ∫ x in 𝓕, f (γ • x) ∂μ := h𝓕.integral_eq_tsum'' f hf₁
_ = ∫ x in 𝓕, ∑' γ : Γ.op, f (γ • x) ∂μ := ?_
_ = ∫ x : G ⧸ Γ, automorphize f x ∂μ_𝓕 := (integral_map continuous_quotient_mk'.aemeasurable hf₂).symm
rw [integral_tsum]
· exact fun i ↦ (hf₁.1.comp_quasiMeasurePreserving (measurePreserving_smul i μ).quasiMeasurePreserving).restrict
· rw [← h𝓕.lintegral_eq_tsum'' (‖f ·‖ₑ)]
exact
ne_of_lt
hf₁.2
-- we can't use `to_additive`, because it tries to translate `*` into `+`
