withDensity_ofReal — Mathlib

English

If f is continuous real-valued, then μ with density of f via ENNReal.ofReal is locally finite.

Русский

Если f непрерывна и принимает вещественные значения, то μ с плотностью через ENNReal.ofReal локально конечна.

LaTeX

$$$ \text{If } f \in C(\alpha,\mathbb{R}),\; \mu^{\mathrm{ofReal}(f)} \text{ locally finite}$$$

Lean4

theorem withDensity_ofReal {f : α → ℝ} (hf : Continuous f) :
    IsLocallyFiniteMeasure (μ.withDensity fun x ↦ .ofReal (f x)) :=
  .withDensity_coe <| continuous_real_toNNReal.comp hf

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