tilted_const — Mathlib

English

If μ is a probability measure, tilting μ by any constant density c leaves μ unchanged: μ.tilted (fun _ ↦ c) = μ.

Русский

Если μ—мера вероятности, то тильтование μ константной плотностью не изменяет её: μ.tilted (константа) = μ.

LaTeX

$$$$\\mu^{\\mathrm{tilted}}(c) = \\mu \\quad\\text{when } \\mu \\text{ is a probability measure}.$$$$

Lean4

theorem tilted_const (μ : Measure α) [IsProbabilityMeasure μ] (c : ℝ) : μ.tilted (fun _ ↦ c) = μ := by simp

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