prod_withDensity₀ — Mathlib

English

Let f: α → ℝ≥0∞ and g: β → ℝ≥0∞ be densities. Then (μ_f) ⊗ (ν_g) equals (μ ⊗ ν) with density (f ∘ π1) · (g ∘ π2) on (α × β).

Русский

Пусть f: α → ℝ≥0∞ и g: β → ℝ≥0∞ — плотности. Тогда (μ_f) ⊗ (ν_g) равна (μ ⊗ ν) с плотностью (f ∘ π1) · (g ∘ π2) на (α × β).

LaTeX

$$$ (\mu_{f}) \otimes (\nu_{g}) = (\mu \otimes \nu)^{(f \circ \pi_1) \cdot (g \circ \pi_2)} $$$

Lean4

theorem prod_withDensity₀ {f : α → ℝ≥0∞} {g : β → ℝ≥0∞} (hf : AEMeasurable f μ) (hg : AEMeasurable g ν) :
    (μ.withDensity f).prod (ν.withDensity g) = (μ.prod ν).withDensity (fun z ↦ f z.1 * g z.2) :=
  by
  rw [prod_withDensity_left₀ hf, prod_withDensity_right₀ hg, ← withDensity_mul₀, mul_comm]
  · rfl
  all_goals fun_prop (disch := intro _ hs; simp [hs])

Похожие утверждения