withDensity_mul — Mathlib

English

If f and g are measurable, then density by f·g equals successive densities by f and then g.

Русский

Если f и g измеримы, плотность f·g равна плотности по f затем по g.

LaTeX

$$$\mu.withDensity (f \cdot g) = (\mu.withDensity f).withDensity g$$$

Lean4

theorem withDensity_mul (μ : Measure α) {f g : α → ℝ≥0∞} (hf : Measurable f) (hg : Measurable g) :
    μ.withDensity (f * g) = (μ.withDensity f).withDensity g :=
  withDensity_mul₀ hf.aemeasurable hg.aemeasurable

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