prod_withDensity_left — Mathlib

English

If f is μ-measurable, then (μ.withDensity f) ⊗ ν = (μ ⊗ ν) with density f on the first coordinate: (μ_f) ⊗ ν = (μ ⊗ ν)^{f ∘ π1}.

Русский

Если f измерима по μ, то (μ с плотностью f) ⊗ ν = (μ ⊗ ν) с плотностью на первом координате: (μ_f) ⊗ ν = (μ ⊗ ν)^{f ∘ π1}.

LaTeX

$$$ (\mu_f) \otimes \nu = (\mu \otimes \nu)^{(f \circ \pi_1)} $$$

Lean4

theorem prod_withDensity_left {f : α → ℝ≥0∞} (hf : Measurable f) :
    (μ.withDensity f).prod ν = (μ.prod ν).withDensity (fun z ↦ f z.1) :=
  prod_withDensity_left₀ hf.aemeasurable

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