tilted_comm — Mathlib

English

If both f and g are integrable exponentials, tilting by f then g equals tilting by g then f: (μ.tilted f).tilted g = (μ.tilted g).tilted f.

Русский

Если экспоненты по f и по g интегрируемы, тильтование по f и затем по g равно тильтованию по g и затем по f.

LaTeX

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

Lean4

theorem tilted_comm (hf : Integrable (fun x ↦ exp (f x)) μ) {g : α → ℝ} (hg : Integrable (fun x ↦ exp (g x)) μ) :
    (μ.tilted f).tilted g = (μ.tilted g).tilted f := by rw [tilted_tilted hf, add_comm, tilted_tilted hg]

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