tilted_apply_eq_ofReal_integral — Mathlib

English

For any μ and f, and any s, the tilted measure is given by the same formula as in the previous item, regardless of integrability, using the appropriate case distinction.

Русский

Для любых μ и f и любого s тильтовая мера задаётся тем же выражением: в зависимости от интегрируемости применяется соответствующее определение.

LaTeX

$$$$\\text{(same as previous item with appropriate case distinction)}$$$$

Lean4

theorem tilted_apply_eq_ofReal_integral [SFinite μ] (f : α → ℝ) (s : Set α) :
    μ.tilted f s = ENNReal.ofReal (∫ a in s, exp (f a) / ∫ x, exp (f x) ∂μ ∂μ) :=
  by
  by_cases hf : Integrable (fun x ↦ exp (f x)) μ
  · rw [tilted_apply _ _, ← ofReal_integral_eq_lintegral_ofReal]
    · exact hf.integrableOn.div_const _
    · exact ae_of_all _ (fun _ ↦ by positivity)
  · simp [tilted_of_not_integrable hf, integral_undef hf]

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