tilted_neg_same' — Mathlib

English

If hf ensures exp(f) is integrable with μ, tilting by f and then by −f yields (μ(Ω))^{-1} μ.

Русский

Если f интегрируема, то тильтовая мера по f и затем по −f равна нормированной μ.

LaTeX

$$$$ (\\mu^{\\mathrm{tilted}} f)^{\\mathrm{tilted}}(-f) = \\mu(\\mathcal{U})^{-1}\\cdot \\mu. $$$$

Lean4

@[simp]
theorem tilted_neg_same' (hf : Integrable (fun x ↦ exp (f x)) μ) : (μ.tilted f).tilted (-f) = (μ Set.univ)⁻¹ • μ := by
  rw [tilted_tilted hf]; simp

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