English
A streamlined version of ae_ae_of_ae_compProd showing how almost-everywhere properties transfer through compProd.
Русский
Упрощённая версия ae_ae_of_ae_compProd, показывающая перенос almost-everywhere свойств через compProd.
LaTeX
$$$$ (ae\_ae\_of\_ae\_compProd) \Rightarrow (ae\_kernel\_lt\_top) $$$$
Lean4
/-- Lebesgue integral against the composition-product of two kernels. -/
theorem lintegral_compProd₀ (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel (α × β) γ) [IsSFiniteKernel η] (a : α)
{f : β × γ → ℝ≥0∞} (hf : AEMeasurable f ((κ ⊗ₖ η) a)) :
∫⁻ z, f z ∂(κ ⊗ₖ η) a = ∫⁻ x, ∫⁻ y, f (x, y) ∂η (a, x) ∂κ a :=
by
have A : ∫⁻ z, f z ∂(κ ⊗ₖ η) a = ∫⁻ z, hf.mk f z ∂(κ ⊗ₖ η) a := lintegral_congr_ae hf.ae_eq_mk
have B : ∫⁻ x, ∫⁻ y, f (x, y) ∂η (a, x) ∂κ a = ∫⁻ x, ∫⁻ y, hf.mk f (x, y) ∂η (a, x) ∂κ a :=
by
apply lintegral_congr_ae
filter_upwards [ae_ae_of_ae_compProd hf.ae_eq_mk] with _ ha using lintegral_congr_ae ha
rw [A, B, lintegral_compProd]
exact hf.measurable_mk
