English
Let g: β → ℝ≥0∞ be ν-almost everywhere measurable. Then μ ⊗ (ν_g) = (μ ⊗ ν) with density g on the second coordinate: μ ⊗ (ν_g) = (μ ⊗ ν)^{g ∘ π2}.
Русский
Пусть g: β → ℝ≥0∞ измерима почти всюду относительно ν. Тогда μ ⊗ (ν с плотностью g) совпадает с μ ⊗ ν с плотностью на втором координате: μ ⊗ (ν_g) = (μ ⊗ ν)^{g ∘ π2}.
LaTeX
$$$ \mu \otimes (\nu_{g}) = (\mu \otimes \nu)^{(g \circ \pi_2)} $$$
Lean4
theorem prod_withDensity_right₀ {g : β → ℝ≥0∞} (hg : AEMeasurable g ν) :
μ.prod (ν.withDensity g) = (μ.prod ν).withDensity (fun z ↦ g z.2) :=
by
refine ext_of_lintegral _ fun φ hφ ↦ ?_
rw [lintegral_prod _ hφ.aemeasurable, lintegral_withDensity_eq_lintegral_mul₀ _ hφ.aemeasurable, lintegral_prod]
· refine lintegral_congr (fun x ↦ ?_)
rw [lintegral_withDensity_eq_lintegral_mul₀ hg (by fun_prop)]
simp
all_goals fun_prop (disch := intro _ hs; simp [hs])
