lintegral_rnDeriv_le

Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.lintegral_rnDeriv_le

English

The total ν-integral of the RN-derivative is bounded by μ(⋯).

Русский

Общая интеграция по ν RN-дериватива ограничена μ(⋯).

LaTeX

$$$\\int \\! \\! ν.\\mathrm{rnDeriv}(\\mu, x) \\, dν(x) ≤ μ(Set.univ)$$$

Lean4

theorem lintegral_rnDeriv_le : ∫⁻ x, μ.rnDeriv ν x ∂ν ≤ μ Set.univ :=
  (setLIntegral_univ _).symm ▸ Measure.setLIntegral_rnDeriv_le Set.univ

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru