limRatioMeas — Mathlib

English

The limit ratio measurable version: limRatioMeas hρ is almost everywhere the limit of ρ a / μ a with respect to μ.

Русский

Измеримая версия limRatioMeas: limRatioMeas есть предел отношения ρ(a)/μ(a) почти везде по μ.

LaTeX

$$$\text{Measurability of } v.limRatioMeas\text{: }\forall a, ρ a/ μ a \to v.limRatioMeas x$ a.e.$$

Lean4

/-- A measurable version of `v.limRatio ρ`. Do *not* use this definition: it is only a temporary
device to show that `v.limRatio` is almost everywhere equal to the Radon-Nikodym derivative. -/
noncomputable def limRatioMeas : α → ℝ≥0∞ :=
  (v.aemeasurable_limRatio hρ).mk _

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