Measure-theoretic results about the circle

This file is a place to collect measure-theoretic results about Circle, the unit circle in ℂ. It equips it with the Borel structure inherited from the ambient subtype, which is what makes Circle-valued functions (such as the additive characters Real.fourierChar and Real.probChar) measurable.

Unlike Circle, the additive circle ℝ / ℤ obtains its MeasurableSpace and BorelSpace instances from the general QuotientAddGroup instances (in Mathlib.MeasureTheory.MeasurableSpace.Constructions and Mathlib.MeasureTheory.Constructions.Polish.Basic respectively).

@[instance_reducible]

instance Circle.instMeasurableSpace : MeasurableSpace Circle

Equations

• One or more equations did not get rendered due to their size.

instance Circle.instBorelSpace : BorelSpace Circle

theorem Circle.measurable_coe : Measurable fun (x : Circle) => ↑x

theorem Circle.measurable_iff {X : Type u_1} [MeasurableSpace X] {f : X → Circle} : Measurable f ↔ Measurable fun (x : X) => ↑(f x)