English
The map (x,y) ↦ x*y is quasi-measure-preserving from μ×ν to ν under suitable left-invariance assumptions.
Русский
Отображение (x,y)↦xy является квази-меропрошым в указанных условиях слева-инвариантности.
LaTeX
$$$\text{QuasiMeasurePreserving}( (p_1,p_2) \mapsto p_1 p_2) (\mu \times \nu) \; \nu$$$
Lean4
/-- A technical lemma relating two different measures. This is basically [Halmos, §60 Th. A].
Note that if `f` is the characteristic function of a measurable set `t` this states that
`μ t = c * μ s` for a constant `c` that does not depend on `μ`.
Note: There is a gap in the last step of the proof in [Halmos].
In the last line, the equality `g(x⁻¹)ν(sx⁻¹) = f(x)` holds if we can prove that
`0 < ν(sx⁻¹) < ∞`. The first inequality follows from §59, Th. D, but the second inequality is
not justified. We prove this inequality for almost all `x` in
`MeasureTheory.ae_measure_preimage_mul_right_lt_top_of_ne_zero`. -/
@[to_additive /-- A technical lemma relating two different measures. This is basically [Halmos, §60 Th. A]. Note
that if `f` is the characteristic function of a measurable set `t` this states that `μ t = c * μ s`
for a constant `c` that does not depend on `μ`.
Note: There is a gap in the last step of the proof in [Halmos]. In the last line, the equality
`g(-x) + ν(s - x) = f(x)` holds if we can prove that `0 < ν(s - x) < ∞`. The first inequality
follows from §59, Th. D, but the second inequality is not justified. We prove this inequality for
almost all `x` in `MeasureTheory.ae_measure_preimage_add_right_lt_top_of_ne_zero`. -/
]
theorem measure_lintegral_div_measure (sm : MeasurableSet s) (h2s : ν' s ≠ 0) (h3s : ν' s ≠ ∞) (f : G → ℝ≥0∞)
(hf : Measurable f) : (μ' s * ∫⁻ y, f y⁻¹ / ν' ((· * y⁻¹) ⁻¹' s) ∂ν') = ∫⁻ x, f x ∂μ' :=
by
set g := fun y => f y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s)
have hg : Measurable g := (hf.comp measurable_inv).div ((measurable_measure_mul_right ν' sm).comp measurable_inv)
simp_rw [measure_mul_lintegral_eq μ' ν' sm g hg, g, inv_inv]
refine lintegral_congr_ae ?_
refine (ae_measure_preimage_mul_right_lt_top_of_ne_zero μ' ν' h2s h3s).mono fun x hx => ?_
simp_rw [ENNReal.mul_div_cancel (measure_mul_right_ne_zero ν' h2s _) hx.ne]
