isProbabilityMeasure_tilted — Mathlib

English

If exp(f) is μ-integrable, then the tilted measure μ.tilted f is a probability measure.

Русский

Если exp(f) интегрируема по μ, то μ.tilted f — мера вероятности.

LaTeX

$$$$\\text{If } \\int e^{f} d\\mu < \\infty, \\; \\mu^{\\mathrm{tilted}} f \\text{ is probability}.$$$$

Lean4

theorem isProbabilityMeasure_tilted [NeZero μ] (hf : Integrable (fun x ↦ exp (f x)) μ) :
    IsProbabilityMeasure (μ.tilted f) := by
  constructor
  simp_rw [tilted_apply' _ _ MeasurableSet.univ, setLIntegral_univ, ENNReal.ofReal_div_of_pos (integral_exp_pos hf),
    div_eq_mul_inv]
  rw [lintegral_mul_const'' _ hf.1.aemeasurable.ennreal_ofReal, ←
    ofReal_integral_eq_lintegral_ofReal hf (ae_of_all _ fun _ ↦ (exp_pos _).le), ENNReal.mul_inv_cancel]
  · simp only [ne_eq, ENNReal.ofReal_eq_zero, not_le]
    exact integral_exp_pos hf
  · simp

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