withDensity_rnDeriv_le — Mathlib

English

For any measures μ and ν on α, the measure obtained by weighting ν with the density μ.rnDer ν is dominated by μ; that is, ν.withDensity(μ.rnDer ν) ≤ μ.

Русский

Для любых мер μ и ν на пространстве α мера, получаемая взвешиванием ν плотностью μ.rnDer ν, не превосходит μ; то есть ν.withDensity(μ.rnDer ν) ≤ μ.

LaTeX

$$$$ \nu.withDensity(\mu.rnDer \\nu) \le \\mu $$$$

Lean4

theorem withDensity_rnDeriv_le (μ ν : Measure α) : ν.withDensity (μ.rnDeriv ν) ≤ μ :=
  by
  by_cases hl : HaveLebesgueDecomposition μ ν
  · conv_rhs => rw [haveLebesgueDecomposition_add μ ν]
    exact Measure.le_add_left le_rfl
  · rw [rnDeriv, dif_neg hl, withDensity_zero]
    exact Measure.zero_le μ

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