English
For a left-invariant μ', almost every x makes the ν' preimage of s under right-translation finite.
Русский
Почти каждое x по μ' делает предобраз ν' по правому сдвигу множества s конечным.
LaTeX
$$$\mathrm{ae}_{x \sim \mu'}\,\bigl(\nu'((\cdot * x)^{-1} s) < \infty\bigr)$$$
Lean4
/-- This is the computation performed in the proof of [Halmos, §60 Th. A]. -/
@[to_additive /-- This is the computation performed in the proof of [Halmos, §60 Th. A]. -/
]
theorem measure_mul_lintegral_eq [IsMulLeftInvariant ν] (sm : MeasurableSet s) (f : G → ℝ≥0∞) (hf : Measurable f) :
(μ s * ∫⁻ y, f y ∂ν) = ∫⁻ x, ν ((fun z => z * x) ⁻¹' s) * f x⁻¹ ∂μ :=
by
rw [← setLIntegral_one, ← lintegral_indicator sm, ←
lintegral_lintegral_mul (measurable_const.indicator sm).aemeasurable hf.aemeasurable, ←
lintegral_lintegral_mul_inv μ ν]
swap
· exact (((measurable_const.indicator sm).comp measurable_fst).mul (hf.comp measurable_snd)).aemeasurable
have ms : ∀ x : G, Measurable fun y => ((fun z => z * x) ⁻¹' s).indicator (fun _ => (1 : ℝ≥0∞)) y := fun x =>
measurable_const.indicator (measurable_mul_const _ sm)
have : ∀ x y, s.indicator (fun _ : G => (1 : ℝ≥0∞)) (y * x) = ((fun z => z * x) ⁻¹' s).indicator (fun b : G => 1) y :=
by intro x y; symm; convert indicator_comp_right (M := ℝ≥0∞) fun y => y * x using 2; ext1; rfl
simp_rw [this, lintegral_mul_const _ (ms _), lintegral_indicator (measurable_mul_const _ sm), setLIntegral_one]
