Global Instances for UnitAddCircle

Mathlib's AddCircleMulti.lean uses local instances for UnitAddCircle. This file exports them globally so that UnitAddTorus (the product) can automatically resolve topological and measure-theoretic instances.

instance instMeasureSpaceUnitAddCircle_navierStokes : MeasureTheory.MeasureSpace UnitAddCircle

Haar measure on the unit circle as the default volume.

Equations

• instMeasureSpaceUnitAddCircle_navierStokes = { toMeasurableSpace := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples 1), volume := AddCircle.haarAddCircle }

instance instIsProbabilityMeasureUnitAddCircleVolume_navierStokes : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

The unit circle is a probability measure space.