OAI/GroupTheory/PolycyclicRecognition/Analysis/DynkinHaarConstruction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Haar measure derived from a finite BCH chart

The global chart and its group multiplication formula suffice: the Jacobian of every left translation is one because its nonconstant part raises the lower central series. No Haar compatibility is assumed.

  1. theorem OAI.PolycyclicRecognition.dynkin_chart_map_isHaar line 24