Densities on the additive circle

Reading an additive-circle point in the chart [a, a + T) sends circle volume to restricted Lebesgue measure. For a law with density relative to normalized Haar measure, the real chart density is the lifted density divided by the period T.

These identities allow cdfs and quantiles of circular laws to be computed in a fixed angle chart, with an explicit choice at the seam. Covering ℝ by translates of one chart also shows that a set of the circle is null exactly when its preimage in ℝ is null (AddCircle.volume_preimage_coe_eq_zero_iff).

In the other direction, reducing a real law with density f modulo T gives the circle law whose density relative to circle volume is the periodization QuotientAddGroup.automorphize f, which at a real point x is ∑ k : ℤ, f (x + k • T). This is how wrapped laws on the circle obtain their densities.

Reading the circle in the symmetric chart (-T/2, T/2], on which the distance to 0 is |x|, also bounds the integral of a radial function h ↦ g ‖h‖ by twice the integral of g over the half line (AddCircle.lintegral_comp_norm_le).

theorem AddCircle.map_coe_equivIco_volume {T : ℝ} [hT : Fact (0 < T)] (a : ℝ) : MeasureTheory.Measure.map (fun (θ : AddCircle T) => ↑((equivIco T a) θ)) MeasureTheory.volume = MeasureTheory.volume.restrict (Set.Ico a (a + T))

Reading a circle point in [a, a + T) sends circle volume to Lebesgue measure restricted to that interval.

theorem AddCircle.volume_preimage_coe_eq_zero_iff {T : ℝ} [hT : Fact (0 < T)] {s : Set (AddCircle T)} : MeasureTheory.volume (QuotientAddGroup.mk ⁻¹' s) = 0 ↔ MeasureTheory.volume s = 0

A set of the additive circle is null exactly when its preimage in ℝ is null.

theorem AddCircle.map_coe_equivIco_withDensity_haarAddCircle {T : ℝ} [hT : Fact (0 < T)] (a : ℝ) {f : AddCircle T → ENNReal} : MeasureTheory.Measure.map (fun (θ : AddCircle T) => ↑((equivIco T a) θ)) (haarAddCircle.withDensity f) = (MeasureTheory.volume.restrict (Set.Ico a (a + T))).withDensity fun (x : ℝ) => (ENNReal.ofReal T)⁻¹ * f ↑x

The real density in [a, a + T) of a Haar-weighted circle law is its lifted Haar density divided by T.

theorem AddCircle.automorphize_coe {T : ℝ} [hT : Fact (0 < T)] {M : Type u_1} [TopologicalSpace M] [AddCommMonoid M] (f : ℝ → M) (x : ℝ) : QuotientAddGroup.automorphize f ↑x = ∑' (k : ℤ), f (x + k • T)

The periodization of a function on ℝ, evaluated at a real point, is the sum of the function over the translates of that point by multiples of the period.

theorem AddCircle.map_coe_withDensity {T : ℝ} [hT : Fact (0 < T)] {f : ℝ → ENNReal} (hf : Measurable f) : MeasureTheory.Measure.map QuotientAddGroup.mk (MeasureTheory.volume.withDensity f) = MeasureTheory.volume.withDensity (QuotientAddGroup.automorphize f)

Reducing a real law with density f modulo T gives the circle law whose density relative to circle volume is the periodization of f.

The proof is the unfolding argument of QuotientAddGroup.integral_eq_integral_automorphize, carried out for lower integrals of ℝ≥0∞-valued functions so that no integrability hypothesis is needed.

theorem AddCircle.lintegral_comp_norm_le {T : ℝ} [hT : Fact (0 < T)] {g : ℝ → ENNReal} (hg : Measurable g) : ∫⁻ (h : AddCircle T), g ‖h‖ ≤ 2 * ∫⁻ (t : ℝ) in Set.Ioi 0, g t

A radial function on the circle integrates to at most twice its integral over the half line: ∫⁻ h, g ‖h‖ ≤ 2 ∫⁻ t in (0, ∞), g t.