tilted_apply — Mathlib

English

For a finite μ (SFinite μ), the tilted measure μ.tilted f evaluated on a set s is given by the integral of the density with respect to μ over s: μ.tilted f(s) = ∫⁻ a in s ENNReal.ofReal(exp(f(a))/∫ exp(f) dμ) dμ.

Русский

Для конечной меры μ tilting по f на множество s даёт ∫⁻ a в s … dμ.

LaTeX

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

Lean4

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

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