Measures on the circle

This file defines the measure on Circle obtained from a continuous nonnegative density on the unit circle with respect to normalized arc length. Its integral is identified with Mathlib's Real.circleAverage.

Main definitions and results

• TauCeti.circleDensityMeasure: normalized arc length weighted by a density.
• TauCeti.isFiniteMeasure_circleDensityMeasure: a continuous density gives a finite measure.
• TauCeti.integral_circleDensityMeasure: integration against the weighted measure is a circle average.
• TauCeti.circleAverage_sub_zpow: the circle average of (z - c) ^ n is 1 for n = 0 and 0 otherwise, the orthogonality relation of the characters of the circle.

noncomputable def TauCeti.circleDensityMeasure (φ : ℂ → ℝ) : MeasureTheory.Measure Circle

The measure on Circle with density max φ 0 with respect to normalized arc length.

Negative values of φ are truncated to 0 by ENNReal.ofReal; for a nonnegative φ the density is φ itself.

Equations

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

theorem TauCeti.isFiniteMeasure_circleDensityMeasure {φ : ℂ → ℝ} (hφ : ContinuousOn φ (Metric.sphere 0 1)) : MeasureTheory.IsFiniteMeasure (circleDensityMeasure φ)

A measure on Circle given by a continuous density with respect to normalized arc length is finite.

theorem TauCeti.integral_circleDensityMeasure {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {φ : ℂ → ℝ} (hφ : ContinuousOn φ (Metric.sphere 0 1)) (hφ₀ : ∀ z ∈ Metric.sphere 0 1, 0 ≤ φ z) {g : ℂ → E} (hg : ContinuousOn g (Metric.sphere 0 1)) : ∫ (z : Circle), g ↑z ∂circleDensityMeasure φ = Real.circleAverage (fun (ζ : ℂ) => φ ζ • g ζ) 0 1

Integration against a continuous nonnegative density on Circle is the corresponding normalized circle average.

@[simp]

theorem TauCeti.circleAverage_sub_zpow {c : ℂ} {R : ℝ} (n : ℤ) : Real.circleAverage (fun (z : ℂ) => (z - c) ^ n) c R = if n = 0 then 1 else 0

Orthogonality of the characters of the circle. The normalized circle average of an integer power (z - c) ^ n over a circle centred at c is 1 for n = 0 and 0 otherwise.