limRatioMeas_measurable

Mathlib.MeasureTheory.Covering.Differentiation

URI: https://scilib.ai/kg/mathlib#VitaliFamily.limRatioMeas_measurable

English

The measure with density limRatioMeas equals ρ: μ with density v.limRatioMeas hρ equals ρ.

Русский

Мера с плотностью limRatioMeas hρ равна ρ: μ.withDensity(limRatioMeas hρ) = ρ.

LaTeX

$$$\mu withDensity (v.limRatioMeas hρ) = ρ$$$

Lean4

theorem limRatioMeas_measurable : Measurable (v.limRatioMeas hρ) :=
  AEMeasurable.measurable_mk _

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

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

Разделы

Аффилиация

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