Haar integrals on the additive circle as circle averages

For any positive period, normalized Haar measure on AddCircle T corresponds to normalized arc length under AddCircle.toCircle. Parametrizing a circle with this map therefore turns its circle average into a Haar integral. For period 2 * π, Complex.arg also gives the reverse transport: a Haar integral of g equals the circle average of g ∘ Complex.arg over the unit circle. These comparisons let results such as the Poisson integral formula be read as statements about integrals over the additive circle.

theorem AddCircle.integral_haarAddCircle_comp_toCircle {T : ℝ} [Fact (0 < T)] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℂ → E) (c : ℂ) (R : ℝ) : ∫ (t : AddCircle T), f (↑R * ↑t.toCircle + c) ∂haarAddCircle = Real.circleAverage f c R

Normalized Haar integration on any positive-period additive circle agrees with the circle average after parametrizing a circle by AddCircle.toCircle.

theorem AddCircle.instFactLtRealOfNatHMulPi_tauCeti : Fact (0 < 2 * Real.pi)

theorem AddCircle.toCircle_arg_of_mem_sphere {z : ℂ} (hz : z ∈ Metric.sphere 0 1) : ↑(toCircle ↑z.arg) = z

On the unit circle, AddCircle.toCircle inverts Complex.arg.

theorem AddCircle.integral_haarAddCircle_eq_circleAverage_arg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (g : AddCircle (2 * Real.pi) → E) : ∫ (θ : AddCircle (2 * Real.pi)), g θ ∂haarAddCircle = Real.circleAverage (fun (z : ℂ) => g ↑z.arg) 0 1

A Haar integral over AddCircle (2 * π) is the circle average over the unit circle of the integrand composed with Complex.arg.