tilted_zero

Mathlib.MeasureTheory.Measure.Tilted

URI: https://scilib.ai/kg/mathlib#MeasureTheory.tilted_zero

English

If μ is a probability measure, tilting by the zero density leaves μ unchanged: μ.tilted 0 = μ.

Русский

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

LaTeX

$$$$\\mu^{\\mathrm{tilted}}(0) = \\mu,$$$$

Lean4

theorem tilted_zero (μ : Measure α) [IsProbabilityMeasure μ] : μ.tilted 0 = μ := by simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru