prod_withDensity — Mathlib

English

For measurable f,g, (μ_f) ⊗ (ν_g) = (μ ⊗ ν) with density (f ∘ π1)(g ∘ π2).

Русский

Для измеримых f,g: (μ_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 : Measurable f) (hg : Measurable g) :
    (μ.withDensity f).prod (ν.withDensity g) = (μ.prod ν).withDensity (fun z ↦ f z.1 * g z.2) :=
  prod_withDensity₀ hf.aemeasurable hg.aemeasurable

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