integral_mul_eq_integral_automorphize_mul

English

For a function f: G→K integrable with μ, and a function g: G/Γ→K with suitable decay, the bilinear unfolding identity holds: the integral over G of g(π(x)) f(x) matches the integral over G/Γ of g(x) automorphize f(x).

Русский

Для функции f: G→K интегрируемой по μ и функции g: G/Γ→K с гладкостью, выполняется билinear-формула развёртывания: интеграл по G от g(π(x)) f(x) равен интегралу по G/Γ от g(x) automorphize f(x).

LaTeX

$$$$\\int_G g(\\pi(x)) f(x) \\, dμ = \\int_{G/Γ} g(x) \\cdot (\\mathrm{automorphize} f)(x) \\, dμ_𝓕.$$$$

Lean4

/-- This is the **Unfolding Trick**: Given an additive subgroup `Γ'` of an additive 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] [μ'.IsAddRightInvariant]
    {f : G' → K} (f_ℒ_1 : Integrable f μ') {g : G' ⧸ Γ' → K} (hg : AEStronglyMeasurable g μ_𝓕)
    (g_ℒ_infinity : essSup (‖g ·‖ₑ) μ_𝓕 ≠ ∞)
    (F_ae_measurable : AEStronglyMeasurable (QuotientAddGroup.automorphize f) μ_𝓕) :
    ∫ x : G', g (x : G' ⧸ Γ') * (f x) ∂μ' = ∫ x : G' ⧸ Γ', g x * (QuotientAddGroup.automorphize f x) ∂μ_𝓕 :=
  by
  let π : G' → G' ⧸ Γ' := QuotientAddGroup.mk
  have meas_π : Measurable π := continuous_quotient_mk'.measurable
  have H₀ : QuotientAddGroup.automorphize ((g ∘ π) * f) = g * (QuotientAddGroup.automorphize f) := by
    exact QuotientAddGroup.automorphize_smul_left f g
  calc
    ∫ (x : G'), g (π x) * f x ∂μ' = ∫ (x : G' ⧸ Γ'), QuotientAddGroup.automorphize ((g ∘ π) * f) x ∂μ_𝓕 := ?_
    _ = ∫ (x : G' ⧸ Γ'), g x * (QuotientAddGroup.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_quotientAddGroup_mk h𝓕 hg'.aemeasurable]
    exact g_ℒ_infinity
  have H₂ : AEStronglyMeasurable (QuotientAddGroup.automorphize ((g ∘ π) * f)) μ_𝓕 :=
    by
    simp_rw [H₀]
    exact hg.mul F_ae_measurable
  apply QuotientAddGroup.integral_eq_integral_automorphize h𝓕 H₁ H₂

Похожие утверждения