English
Swapping the order of the inner lintegrals after applying a certain left-invariant transformation leads to an equivalent expression.
Русский
Замена порядка вложенных линтегралов после применения определённого левоинвариантного преобразования приводит к эквивалентному выражению.
LaTeX
$$$\iint f(yx)\, x^{-1} \, d\nu(y) \, d\mu(x) = \iint f(x,y) \, d\nu(y) \, d\mu(x)$$$
Lean4
@[to_additive]
theorem lintegral_lintegral_mul_inv [IsMulLeftInvariant ν] (f : G → G → ℝ≥0∞)
(hf : AEMeasurable (uncurry f) (μ.prod ν)) : (∫⁻ x, ∫⁻ y, f (y * x) x⁻¹ ∂ν ∂μ) = ∫⁻ x, ∫⁻ y, f x y ∂ν ∂μ :=
by
have h : Measurable fun z : G × G => (z.2 * z.1, z.1⁻¹) :=
(measurable_snd.mul measurable_fst).prodMk measurable_fst.inv
have h2f : AEMeasurable (uncurry fun x y => f (y * x) x⁻¹) (μ.prod ν) :=
hf.comp_quasiMeasurePreserving (measurePreserving_mul_prod_inv μ ν).quasiMeasurePreserving
simp_rw [lintegral_lintegral h2f, lintegral_lintegral hf]
conv_rhs => rw [← (measurePreserving_mul_prod_inv μ ν).map_eq]
symm
exact lintegral_map' (hf.mono' (measurePreserving_mul_prod_inv μ ν).map_eq.absolutelyContinuous) h.aemeasurable
