tilted — Mathlib

English

Exponentially tilting a finite measure by a function f yields a new measure μ.tilted f, defined by a density proportional to exp(f).

Русский

Экспоненциально сдвигая меру μ по функции f, получаем новую меру μ.tilted f, плотность пропорциональна exp(f).

LaTeX

$$Measure.tilted μ f$$

Lean4

/-- Exponentially tilted measure. When `x ↦ exp (f x)` is integrable, `μ.tilted f` is the
probability measure with density with respect to `μ` proportional to `exp (f x)`. Otherwise it is 0.
-/
noncomputable def tilted (μ : Measure α) (f : α → ℝ) : Measure α :=
  μ.withDensity (fun x ↦ ENNReal.ofReal (exp (f x) / ∫ x, exp (f x) ∂μ))

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