English
An unfolding identity with a product structure: the integral of g(π(x)) f(x) equals the integral over the quotient of g times automorphize f, under suitable integrability and measurability assumptions.
Русский
Идентичность развёртывания с произведением: интеграл g(π(x)) f(x) равен интегралу по фактор-пространству от g множителя на automorphize f, при подходящих условия интегрируемости и измеримости.
LaTeX
$$$$\\int_G g(π(x)) \\cdot f(x) \\, dμ = \\int_{G/Γ} g(x) \\cdot (\\mathrm{automorphize} f)(x) \\, dμ_𝓕.$$$$
Lean4
/-- The parameterized integral `x ↦ ∫ y, g (y⁻¹ * x) ∂μ` depends continuously on `y` when `g` is a
compactly supported continuous function on a topological group `G`, and `μ` is finite on compact
sets. -/
@[to_additive]
theorem continuous_integral_apply_inv_mul {G : Type*} [TopologicalSpace G] [LocallyCompactSpace G] [Group G]
[IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] {μ : Measure G} [IsFiniteMeasureOnCompacts μ] {E : Type*}
[NormedAddCommGroup E] [NormedSpace ℝ E] {g : G → E} (hg : Continuous g) (h'g : HasCompactSupport g) :
Continuous (fun (x : G) ↦ ∫ y, g (y⁻¹ * x) ∂μ) :=
by
let k := tsupport g
have k_comp : IsCompact k := h'g
apply continuous_iff_continuousAt.2 (fun x₀ ↦ ?_)
obtain ⟨t, t_comp, ht⟩ : ∃ t, IsCompact t ∧ t ∈ 𝓝 x₀ := exists_compact_mem_nhds x₀
let k' : Set G := t • k⁻¹
have k'_comp : IsCompact k' := t_comp.smul_set k_comp.inv
have A : ContinuousOn (fun (x : G) ↦ ∫ y, g (y⁻¹ * x) ∂μ) t :=
by
apply continuousOn_integral_of_compact_support k'_comp
· exact (hg.comp (continuous_snd.inv.mul continuous_fst)).continuousOn
· intro p x hp hx
contrapose! hx
refine ⟨p, hp, p⁻¹ * x, ?_, by simp⟩
simpa only [Set.mem_inv, mul_inv_rev, inv_inv] using subset_tsupport _ hx
exact A.continuousAt ht
