Formalized Haar Measure

DOI10.4230/lipics.itp.2021.18arXiv2102.07636OpenAlexW3173599188MaRDI QIDQ6099605

Floris van Doorn

Publication date: 20 June 2023

Full work available at URL: https://arxiv.org/abs/2102.07636

zbMATH Keywords

Haar measuremeasure theoryBochner integralinteractive theorem provingformalized mathematicsLean

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (3)

Measure construction by extension in dependent type theory with application to integration ⋮ A formalization of the change of variables formula for integrals in mathlib ⋮ A Coq formalization of Lebesgue induction principle and Tonelli's theorem

This page was built for publication: Formalized Haar Measure