English
In the unfolding set-up, for a function f: G→K and a function g: G/Γ→K, the integral of g(π(x)) f(x) over μ equals the integral of g(x) automorphize f(x) over μ_𝓕, i.e. the product structure is preserved under unfolding.
Русский
В рамках развёртывания для функции f: G→K и функции g: G/Γ→K интеграл g(π(x)) f(x) по μ равен интегралу g(x) automorphize f(x) по μ_𝓕.
LaTeX
$$$$\\int_G g(\\pi(x)) \\cdot f(x) \\, dμ = \\int_{G/Γ} g(x) \\cdot (\\mathrm{automorphize} f)(x) \\, dμ_𝓕.$$$$
Lean4
/-- This is the **Unfolding Trick**: Given a subgroup `Γ` of a group `G`, the integral of a
function `f` on `G` times the lift to `G` of a function `g` on the quotient `G ⧸ Γ` with respect
to a right-invariant measure `μ` on `G`, is equal to the integral over the quotient of the
automorphization of `f` times `g`. -/
theorem integral_mul_eq_integral_automorphize_mul {K : Type*} [NormedField K] [NormedSpace ℝ K] [μ.IsMulRightInvariant]
{f : G → K} (f_ℒ_1 : Integrable f μ) {g : G ⧸ Γ → K} (hg : AEStronglyMeasurable g μ_𝓕)
(g_ℒ_infinity : essSup (fun x ↦ ↑‖g x‖ₑ) μ_𝓕 ≠ ∞)
(F_ae_measurable : AEStronglyMeasurable (QuotientGroup.automorphize f) μ_𝓕) :
∫ x : G, g (x : G ⧸ Γ) * (f x) ∂μ = ∫ x : G ⧸ Γ, g x * (QuotientGroup.automorphize f x) ∂μ_𝓕 :=
by
let π : G → G ⧸ Γ := QuotientGroup.mk
have meas_π : Measurable π := continuous_quotient_mk'.measurable
have H₀ : QuotientGroup.automorphize ((g ∘ π) * f) = g * (QuotientGroup.automorphize f) := by
exact QuotientGroup.automorphize_smul_left f g
calc
∫ (x : G), g (π x) * (f x) ∂μ = ∫ (x : G ⧸ Γ), QuotientGroup.automorphize ((g ∘ π) * f) x ∂μ_𝓕 := ?_
_ = ∫ (x : G ⧸ Γ), g x * (QuotientGroup.automorphize f x) ∂μ_𝓕 := by simp [H₀]
have H₁ : Integrable ((g ∘ π) * f) μ :=
by
have : AEStronglyMeasurable (fun (x : G) ↦ g (x : (G ⧸ Γ))) μ :=
(hg.mono_ac h𝓕.absolutelyContinuous_map).comp_measurable meas_π
refine Integrable.essSup_smul f_ℒ_1 this ?_
have hg' : AEStronglyMeasurable (‖g ·‖ₑ) μ_𝓕 := continuous_enorm.comp_aestronglyMeasurable hg
rw [← essSup_comp_quotientGroup_mk h𝓕 hg'.aemeasurable]
exact g_ℒ_infinity
have H₂ : AEStronglyMeasurable (QuotientGroup.automorphize ((g ∘ π) * f)) μ_𝓕 :=
by
simp_rw [H₀]
exact hg.mul F_ae_measurable
apply QuotientGroup.integral_eq_integral_automorphize h𝓕 H₁ H₂
