setIntegral_tilted — Mathlib

English

For f, g: α → E, s measurable, the tilted integral over s equals the restricted μ integral with density multiplied by g.

Русский

Для f, g: α → E и измеримого s интеграл по тильтированной мере равен интегралу по μ на s плотности и умноженной на g.

LaTeX

$$$$\\int_{s} g(x) \\, d(\\mu^{\\mathrm{tilted}} f)(x) = \\int_{s} \\left(\\frac{e^{f(x)}}{\\int e^{f} d\\mu}\\right) \\cdot g(x) \\, d\\mu(x).$$$$

Lean4

theorem setIntegral_tilted [SFinite μ] (f : α → ℝ) (g : α → E) (s : Set α) :
    ∫ x in s, g x ∂(μ.tilted f) = ∫ x in s, (exp (f x) / ∫ x, exp (f x) ∂μ) • (g x) ∂μ :=
  by
  by_cases hf : AEMeasurable f μ
  · rw [tilted_eq_withDensity_nnreal, setIntegral_withDensity_eq_setIntegral_smul₀']
    · congr
    · suffices AEMeasurable (fun x ↦ exp (f x) / ∫ x, exp (f x) ∂μ) μ
        by
        rw [← aemeasurable_coe_nnreal_real_iff]
        refine AEMeasurable.restrict ?_
        simpa only [NNReal.coe_mk]
      exact (measurable_exp.comp_aemeasurable hf).div_const _
  · have hf' : ¬Integrable (fun x ↦ exp (f x)) μ := by
      exact fun h ↦ hf (aemeasurable_of_aemeasurable_exp h.1.aemeasurable)
    simp only [hf, not_false_eq_true, tilted_of_not_aemeasurable, Measure.restrict_zero, integral_zero_measure]
    rw [integral_undef hf']
    simp

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