tilted_apply' — Mathlib

English

For a measurable set s, the tilted measure of f assigns to s the Levy measure given by ENNReal.ofReal(exp(f(x))/∫ exp(f) dμ) integrated over s with respect to μ.

Русский

Для измеримого множества s тильтованная мера f отдает долю, равную интегралу ENNReal.ofReal(exp(f(x))/∫ exp(f) dμ) по μ на s.

LaTeX

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

Lean4

theorem tilted_apply' (μ : Measure α) (f : α → ℝ) {s : Set α} (hs : MeasurableSet s) :
    μ.tilted f s = ∫⁻ a in s, ENNReal.ofReal (exp (f a) / ∫ x, exp (f x) ∂μ) ∂μ := by
  rw [Measure.tilted, withDensity_apply _ hs]

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