haarAddCircle — Mathlib

English

Define the Haar measure on the additive circle with total mass 1; this is the unique translation-invariant probability measure on the circle.

Русский

Определяется мера Хаара на аддитивном круге с единичной массой; это единственная по сдвижению вероятность распределения на круге.

LaTeX

$$$$ \\text{haarAddCircle} : \\text{Measure}(\\text{AddCircle } T) $$$$

Lean4

/-- Haar measure on the additive circle, normalised to have total measure 1. -/
def haarAddCircle : Measure (AddCircle T) :=
  addHaarMeasure ⊤
deriving IsAddHaarMeasure

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