charFun_zero

Mathlib.MeasureTheory.Measure.CharacteristicFunction

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

English

For any measured space E and any t, the characteristic function of the zero measure is identically zero: χ_0(t) = 0.

Русский

Для нулевой меры χ_0(t) ≡ 0 для всех t.

LaTeX

$$$$\\chi_{0}(t) = 0.$$$$

Lean4

@[simp]
theorem charFun_zero (μ : Measure E) : charFun μ 0 = μ.real Set.univ := by simp [charFun_apply]

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

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

Разделы

Аффилиация

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