rnDeriv_tilted_left_self — Mathlib

English

For a σ-finite μ, the tilted measure μ.tilted f has RN-derivative with respect to μ given a.e. by ENNReal.ofReal(exp(f)/∫ exp(f) dμ).

Русский

Для σ-частичной μ т.д. наклонённая мера μ.tilted f имеет RN-дериватив по отношению к μ, почти везде равный ENNReal.ofReal(exp(f)/∫ exp(f) dμ).

LaTeX

$$$(μ^{\\tilted f})\\mathrm{rnDeriv}_{μ} =_{μ}^{\\mathrm{ae}} x \\mapsto \\mathrm{ENNReal.ofReal}\\left( \\frac{e^{f(x)}}{\\int e^{f} dμ} \\right).$$$

Lean4

theorem rnDeriv_tilted_left_self [SigmaFinite μ] (hf : AEMeasurable f μ) :
    (μ.tilted f).rnDeriv μ =ᵐ[μ] fun x ↦ ENNReal.ofReal (exp (f x) / ∫ x, exp (f x) ∂μ) :=
  by
  refine (rnDeriv_tilted_left μ hf).trans ?_
  filter_upwards [Measure.rnDeriv_self μ] with x hx
  rw [hx, mul_one]

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