withDensity_mul₀ — Mathlib

English

The density operation is associative: applying density f then density g equals applying density f·g at once.

Русский

Операция плотности ассоциативна: применение плотности f затем плотности g эквивалентно плотности f·g за один раз.

LaTeX

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

Lean4

theorem withDensity_mul₀ {μ : Measure α} {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
    μ.withDensity (f * g) = (μ.withDensity f).withDensity g :=
  by
  ext1 s hs
  rw [withDensity_apply _ hs, withDensity_apply _ hs, restrict_withDensity hs,
    lintegral_withDensity_eq_lintegral_mul₀ hf.restrict hg.restrict]

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