tilted_eq_withDensity_nnreal — Mathlib

English

There is a representation μ.tilted f = μ.withDensity h where h(x) = ENNReal.ofNNReal ⟨exp(f(x)) / ∫ exp(f) dμ, proof⟩, i.e., tilting is density with respect to μ given by exp(f).

Русский

Существует представление μ.tilted f = μ.withDensity h, где плотность h(x) пропорциональна exp(f(x)) и нормирована на ∫ exp(f) dμ.

LaTeX

$$$$\\mu^{\\mathrm{tilted}} f = \\mu.\\text{withDensity} \\bigl(\\lambda x. ENNReal.ofNNReal\\left(\\left\\langle e^{f(x)}, \\int e^{f} d\\mu \\right\\rangle \\right)\\bigr).$$$$

Lean4

theorem tilted_eq_withDensity_nnreal (μ : Measure α) (f : α → ℝ) :
    μ.tilted f = μ.withDensity (fun x ↦ ((↑) : ℝ≥0 → ℝ≥0∞) (⟨exp (f x) / ∫ x, exp (f x) ∂μ, by positivity⟩ : ℝ≥0)) :=
  by
  rw [Measure.tilted]
  congr with x
  rw [ENNReal.ofReal_eq_coe_nnreal]

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