instIsProbabilityMeasureRealHaarAddCircle

Mathlib.Analysis.Fourier.AddCircle

URI: https://scilib.ai/kg/mathlib#AddCircle.instIsProbabilityMeasureRealHaarAddCircle

English

The Haar measure on the additive circle is a probability measure; hence the total mass is 1.

Русский

Мера Хаара на аддитивном круге является вероятностной; суммарная масса равна 1.

LaTeX

$$$$ \\text{IsProbabilityMeasure}(\\text{haarAddCircle}) $$$$

Lean4

instance : IsProbabilityMeasure (@haarAddCircle T _) :=
  IsProbabilityMeasure.mk addHaarMeasure_self

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

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

Разделы

Аффилиация

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