English
A technical relation expresses the integral of a function against a product measure in terms of a divisive expression involving ν' and the preimage of s.
Русский
Техническое соотношение выражает интеграл по произведенной мере через делящее выражение, связанное с ν' и предобразом s.
LaTeX
$$$(\\text{sm} : \\text{MeasurableSet } s) \\Rightarrow (\\mu' s) \\cdot \\int f \\, d\\nu' = \\int f \\, d\\mu' \\, + \\text{(сквозное преобразование)}$$$
Lean4
@[to_additive]
theorem ae_measure_preimage_mul_right_lt_top (hμs : μ' s ≠ ∞) : ∀ᵐ x ∂μ', ν' ((· * x) ⁻¹' s) < ∞ :=
by
wlog sm : MeasurableSet s generalizing s
·
filter_upwards [this ((measure_toMeasurable _).trans_ne hμs) (measurableSet_toMeasurable ..)] with x hx using
lt_of_le_of_lt (by gcongr; apply subset_toMeasurable) hx
refine ae_of_forall_measure_lt_top_ae_restrict' ν'.inv _ ?_
intro A hA _ h3A
simp only [ν'.inv_apply] at h3A
apply ae_lt_top (measurable_measure_mul_right ν' sm)
have h1 := measure_mul_lintegral_eq μ' ν' sm (A⁻¹.indicator 1) (measurable_one.indicator hA.inv)
rw [lintegral_indicator hA.inv] at h1
simp_rw [Pi.one_apply, setLIntegral_one, ← image_inv_eq_inv, indicator_image inv_injective, image_inv_eq_inv, ←
indicator_mul_right _ fun x => ν' ((· * x) ⁻¹' s), Function.comp, Pi.one_apply, mul_one] at h1
rw [← lintegral_indicator hA, ← h1]
finiteness
