integral_tilted — Mathlib

English

For finite μ, the tilted integral over all x equals the original integral with the density factor: ∫ g d(μ.tilted f) = ∫ (e^{f}/∫ e^{f} dμ) • g dμ.

Русский

Для конечной меры μ интеграл по т tilting удерживает плотность: ∫ g d(μ.tilted f) = ∫ density • g dμ.

LaTeX

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

Lean4

theorem integral_tilted (f : α → ℝ) (g : α → E) :
    ∫ x, g x ∂(μ.tilted f) = ∫ x, (exp (f x) / ∫ x, exp (f x) ∂μ) • (g x) ∂μ := by
  rw [← setIntegral_univ, setIntegral_tilted' f g MeasurableSet.univ, setIntegral_univ]

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