lintegral_tilted — Mathlib

English

The global lintegral against the tilted measure equals the original lintegral against μ with the density factor: ∫ g d(μ.tilted f) = ∫ (exp(f)/∫ exp(f)) g dμ.

Русский

Линегральный интеграл по тильтированной мере равен интегралу по μ с плотностью exp(f)/∫ exp(f) dμ.

LaTeX

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

Lean4

theorem lintegral_tilted (f : α → ℝ) (g : α → ℝ≥0∞) :
    ∫⁻ x, g x ∂(μ.tilted f) = ∫⁻ x, ENNReal.ofReal (exp (f x) / ∫ x, exp (f x) ∂μ) * (g x) ∂μ := by
  rw [← setLIntegral_univ, setLIntegral_tilted' f g MeasurableSet.univ, setLIntegral_univ]

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