License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2020.34
URN: urn:nbn:de:0030-drops-116779
Go to the corresponding LIPIcs Volume Portal

Pauly, Arno ; Seon, Dongseong ; Ziegler, Martin

Computing Haar Measures

LIPIcs-CSL-2020-34.pdf (0.7 MB)


According to Haar’s Theorem, every compact topological group G admits a unique (regular, right and) left-invariant Borel probability measure μ_G. Let the Haar integral (of G) denote the functional ∫_G:?(G)∋ f ↦ ∫ f d μ_G integrating any continuous function f:G → ℝ with respect to μ_G. This generalizes, and recovers for the additive group G=[0;1)mod 1, the usual Riemann integral: computable (cmp. Weihrauch 2000, Theorem 6.4.1), and of computational cost characterizing complexity class #P_1 (cmp. Ko 1991, Theorem 5.32).
We establish that in fact, every computably compact computable metric group renders the Haar measure/integral computable: once using an elegant synthetic argument, exploiting uniqueness in a computably compact space of probability measures; and once presenting and analyzing an explicit, imperative algorithm based on "maximum packings" with rigorous error bounds and guaranteed convergence. Regarding computational complexity, for the groups SO(3) and SU(2), we reduce the Haar integral to and from Euclidean/Riemann integration. In particular both also characterize #P_1.

BibTeX - Entry

  author =	{Arno Pauly and Dongseong Seon and Martin Ziegler},
  title =	{{Computing Haar Measures}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{34:1--34:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Maribel Fern{\'a}ndez and Anca Muscholl},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{},
  URN =		{urn:nbn:de:0030-drops-116779},
  doi =		{10.4230/LIPIcs.CSL.2020.34},
  annote =	{Keywords: Computable analysis, topological groups, exact real arithmetic, Haar measure}

Keywords: Computable analysis, topological groups, exact real arithmetic, Haar measure
Collection: 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)
Issue Date: 2020
Date of publication: 06.01.2020
Supplementary Material: The source code of the implementation in Section 6.1 is available at

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI