English
Let f: α → ℝ≥0∞ be μ-almost everywhere measurable. Then the product of μ with density f and ν equals the product measure μ ⊗ ν equipped with density f on the first factor: (μ_f) ⊗ ν = (μ ⊗ ν)^{f ∘ π1}.
Русский
Пусть f: α → ℝ≥0∞ измерима почти всюду относительно μ. Тогда произведение μ с плотностью f и ν совпадает с произведением μ и ν, но с плотностью на первом факторе: (μ_f) ⊗ ν = (μ ⊗ ν)^{f ∘ π1}.
LaTeX
$$$ (\mu_f) \otimes \nu = (\mu \otimes \nu)^{(f \circ \pi_1)} $$$
Lean4
theorem prod_withDensity_left₀ {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) :
(μ.withDensity f).prod ν = (μ.prod ν).withDensity (fun z ↦ f z.1) :=
by
refine ext_of_lintegral _ fun φ hφ ↦ ?_
rw [lintegral_prod _ hφ.aemeasurable, lintegral_withDensity_eq_lintegral_mul₀ hf,
lintegral_withDensity_eq_lintegral_mul₀ _ hφ.aemeasurable, lintegral_prod]
· refine lintegral_congr (fun x ↦ ?_)
rw [Pi.mul_apply, ← lintegral_const_mul'' _ (by fun_prop)]
simp
all_goals fun_prop (disch := intro _ hs; simp [hs])
