rnDeriv_tilted_right — Mathlib

English

Let μ and ν be σ-finite measures on α and f: α → ℝ with exp(f) integrable w.r.t ν. Then the Radon-Nikodym derivative of μ with respect to the tilted ν is ν-almost everywhere equal to ENNReal.ofReal(exp(-f) · ∫ exp(f) dν) times μ.rnDeriv ν.

Русский

Пусть μ и ν — нормируемые по объёму меры на α, и f: α → ℝ так, что exp(f) интегрируема по ν. Тогда радиодериватив μ по отношению к наклонённой ν равен ν-почти всюду ENNReal.ofReal(exp(-f) · ∫ exp(f) dν) умноженное на RN-дериватив μ по отношению к ν.

LaTeX

$$$\\mu\\mathrm{rnDeriv}(\\nu^{\\tilde f}) =_{\\nu}^{\\mathrm{ae}} x \\mapsto \\mathrm{ENNReal.ofReal}\\big( e^{-f(x)} \\int x e^{f} \\,d\\nu \\big) \\cdot \\mu\\mathrm{rnDeriv}_{\\nu}(x).$$$

Lean4

theorem rnDeriv_tilted_right (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] (hf : Integrable (fun x ↦ exp (f x)) ν) :
    μ.rnDeriv (ν.tilted f) =ᵐ[ν] fun x ↦ ENNReal.ofReal (exp (-f x) * ∫ x, exp (f x) ∂ν) * μ.rnDeriv ν x := by
  cases eq_zero_or_neZero ν with
  | inl h => simp_rw [h, ae_zero, Filter.EventuallyEq]; exact Filter.eventually_bot
  | inr h0 =>
    refine (Measure.rnDeriv_withDensity_right μ ν ?_ ?_ ?_).trans ?_
    · exact (hf.1.aemeasurable.div_const _).ennreal_ofReal
    · filter_upwards
      simp only [ne_eq, ENNReal.ofReal_eq_zero, not_le]
      exact fun _ ↦ div_pos (exp_pos _) (integral_exp_pos hf)
    · refine ae_of_all _ (by simp)
    · filter_upwards with x
      congr
      rw [← ENNReal.ofReal_inv_of_pos, inv_div', ← exp_neg, div_eq_mul_inv, inv_inv]
      exact div_pos (exp_pos _) (integral_exp_pos hf)

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