tilted_neg_same — Mathlib

English

For probability μ, Integrable exp(f) ensures (μ.tilted f).tilted (−f) = μ.

Русский

Для μ, являющейся вероятностью, интегрируемость exp(f) обеспечивает (μ.tilted f).tilted (−f) = μ.

LaTeX

$$$$ (\\mu^{\\mathrm{tilted}} f)^{\\mathrm{tilted}}(-f) = \\mu. $$$$

Lean4

theorem tilted_neg_same [IsProbabilityMeasure μ] (hf : Integrable (fun x ↦ exp (f x)) μ) :
    (μ.tilted f).tilted (-f) = μ := by simp [hf]

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