rnDeriv_le_one_of_le — Mathlib

English

If μ ≤ ν and ν is σ-finite, then the Radon–Nikodym derivative μ.rnDeriv ν is almost everywhere at most 1 with respect to ν.

Русский

Если μ ≤ ν и ν σ-конечна, то RN-дериватив μ.rnDeriv ν не больше единицы почти наверняка по ν.

LaTeX

$$$$ μ.rnDeriv ν \leq^{\mathrm{ae}}_ν 1 $$$$

Lean4

theorem rnDeriv_le_one_of_le (hμν : μ ≤ ν) [SigmaFinite ν] : μ.rnDeriv ν ≤ᵐ[ν] 1 :=
  by
  refine ae_le_of_forall_setLIntegral_le_of_sigmaFinite (μ.measurable_rnDeriv ν) fun s _ _ ↦ ?_
  simp only [Pi.one_apply, MeasureTheory.setLIntegral_one]
  exact (Measure.setLIntegral_rnDeriv_le s).trans (hμν s)

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