Circle Averages

For a function f on the complex plane, this file introduces the definition Real.circleAverage f c R as a shorthand for the average of f on the circle with center c and radius R, equipped with the rotation-invariant measure of total volume one. Like IntervalAverage, this notion exists as a convenience. It avoids notationally inconvenient compositions of f with circleMap and avoids the need to manually eliminate 2 * π every time an average is computed.

Note: Like the interval average defined in Mathlib/MeasureTheory/Integral/IntervalAverage.lean, the circleAverage defined here is a purely measure-theoretic average. It should not be confused with circleIntegral, which is the path integral over the circle path. The relevant integrability property circleAverage is CircleIntegrable, as defined in Mathlib/MeasureTheory/Integral/CircleIntegral.lean.

Implementation Note: Like circleMap, circleAverages are defined for negative radii. The theorem circleAverage_congr_negRadius shows that the average is independent of the radius' sign.

Definition

noncomputable def Real.circleAverage {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℂ → E) (c : ℂ) (R : ℝ) : E

Define circleAverage f c R as the average value of f on the circle with center c and radius R. This is a real notion, which should not be confused with the complex path integral notion defined in circleIntegral (integrating with respect to dz).

theorem Real.circleAverage_def {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℂ → E} {c : ℂ} {R : ℝ} : circleAverage f c R = (2 * Real.pi)⁻¹ • ∫ (θ : ℝ) in 0..2 * Real.pi, f (circleMap c R θ)

theorem Real.circleAverage.integral_undef {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℂ → E} {c : ℂ} {R : ℝ} (hf : ¬CircleIntegrable f c R) : circleAverage f c R = 0

If 'f' is not circle integrable, then the circle average is zero by definition.

theorem Real.circleAverage_eq_intervalAverage {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℂ → E} {c : ℂ} {R : ℝ} : circleAverage f c R = ⨍ (θ : ℝ) in 0..2 * Real.pi, f (circleMap c R θ)

Expression of circleAverage in terms of interval averages.

@[simp]

theorem Real.circleAverage_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℂ → E} {c : ℂ} [CompleteSpace E] : circleAverage f c 0 = f c

Interval averages for zero radii equal values at the center point.

theorem Real.circleAverage_map_add_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℂ → E} {c : ℂ} {R : ℝ} : circleAverage (fun (z : ℂ) => f (z + c)) 0 R = circleAverage f c R

Expression of circleAverage with arbitrary center in terms of circleAverage with center zero.

theorem Real.circleAverage_eq_circleIntegral {c : ℂ} {R : ℝ} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : ℂ → F} (h : R ≠ 0) : circleAverage f c R = (2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z

Expression of the circleAverage in terms of a circleIntegral.

Congruence Lemmata

theorem Real.circleAverage_eq_integral_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℂ → E} {c : ℂ} {R : ℝ} (η : ℝ) : circleAverage f c R = (2 * Real.pi)⁻¹ • ∫ (θ : ℝ) in 0..2 * Real.pi, f (circleMap c R (θ + η))

Circle averages do not change when shifting the angle.

@[simp]

theorem Real.circleAverage_neg_radius {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℂ → E} {c : ℂ} {R : ℝ} : circleAverage f c (-R) = circleAverage f c R

Circle averages do not change when replacing the radius by its negative.

@[simp]

theorem Real.circleAverage_abs_radius {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℂ → E} {c : ℂ} {R : ℝ} : circleAverage f c |R| = circleAverage f c R

Circle averages do not change when replacing the radius by its absolute value.

theorem Real.circleAverage_congr_codiscreteWithin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f₁ f₂ : ℂ → E} {c : ℂ} {R : ℝ} (hf : f₁ =ᶠ[Filter.codiscreteWithin (Metric.sphere c |R|)] f₂) (hR : R ≠ 0) : circleAverage f₁ c R = circleAverage f₂ c R

If two functions agree outside of a discrete set in the circle, then their averages agree.

theorem Real.circleAverage_congr_sphere {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {c : ℂ} {R : ℝ} {f₁ f₂ : ℂ → E} (hf : Set.EqOn f₁ f₂ (Metric.sphere c |R|)) : circleAverage f₁ c R = circleAverage f₂ c R

If two functions agree on the circle, then their circle averages agree.

theorem Real.circleAverage_eq_circleAverage_zero_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℂ → E} {c : ℂ} {R : ℝ} : circleAverage f c R = circleAverage (fun (z : ℂ) => f (↑R * z + c)) 0 1

Express the circle average over an arbitrary circle as a circle average over the unit circle.

@[simp]

theorem Real.circleAverage_zero_one_congr_inv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℂ → E} : circleAverage (fun (x : ℂ) => f x⁻¹) 0 1 = circleAverage f 0 1

The circle average of a function f on the unit sphere equals the circle average of the function z ↦ f z⁻¹.

Continuity

theorem Real.circleMap.continuous {c : ℂ} : Continuous fun (x : ℝ × ℝ) => circleMap c x.1 x.2

The circleMap for a fixed center is continuous as a function on ℝ × ℝ.

theorem Real.ContinuousOn.circleAverage {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℂ → E} {s : Set ℝ} {c : ℂ} (hf : ContinuousOn f {z : ℂ | ‖z - c‖ ∈ s}) (hs : ∀ r ∈ s, 0 ≤ r) : ContinuousOn (Real.circleAverage f c) s

The circle average of a continuous function is itself continuous, as a function of the radius.

theorem Real.ContinuousOn.eq_of_eqOn_Ioo {f : ℝ → ℝ} {c r R : ℝ} (h₁f : ContinuousOn f (Set.Ioc r R)) (hR : r < R) (h₂f : Set.EqOn f (fun (x : ℝ) => c) (Set.Ioo r R)) : f R = c

Companion lemma to ContinuousOn.circleAverage: a function continuous on Ioc r R and constant on Ioo r R is constant.

Constant Functions

theorem Real.circleAverage_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (a : E) (c : ℂ) (R : ℝ) : circleAverage (fun (x : ℂ) => a) c R = a

The circle average of a constant function equals the constant.

theorem Real.circleAverage_const_on_circle {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℂ → E} {c : ℂ} {R : ℝ} [CompleteSpace E] {a : E} (hf : ∀ x ∈ Metric.sphere c |R|, f x = a) : circleAverage f c R = a

If f x equals a on for every point of the circle, then the circle average of f equals a.

Inequalities

theorem Real.circleAverage_mono {c : ℂ} {R : ℝ} {f₁ f₂ : ℂ → ℝ} (hf₁ : CircleIntegrable f₁ c R) (hf₂ : CircleIntegrable f₂ c R) (h : ∀ x ∈ Metric.sphere c |R|, f₁ x ≤ f₂ x) : circleAverage f₁ c R ≤ circleAverage f₂ c R

Circle averages respect the ≤ relation.

theorem Real.circleAverage_mono_on_of_le_circle {c : ℂ} {R : ℝ} {f : ℂ → ℝ} {a : ℝ} (hf : CircleIntegrable f c R) (h₂f : ∀ x ∈ Metric.sphere c |R|, f x ≤ a) : circleAverage f c R ≤ a

If f x is smaller than a on for every point of the circle, then the circle average of f is smaller than a.

theorem Real.abs_circleAverage_le_circleAverage_abs {c : ℂ} {R : ℝ} {f : ℂ → ℝ} : |circleAverage f c R| ≤ circleAverage |f| c R

Analogue of intervalIntegral.abs_integral_le_integral_abs: The absolute value of a circle average is less than or equal to the circle average of the absolute value of the function.

theorem Real.circleAverage_nonneg_of_nonneg {c : ℂ} {R : ℝ} {f : ℂ → ℝ} (h₂f : ∀ x ∈ Metric.sphere c |R|, 0 ≤ f x) : 0 ≤ circleAverage f c R

The circle average of a nonnegative function is nonnegative.

Commutativity with Linear Maps

theorem ContinuousLinearMap.circleAverage_comp_comm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {c : ℂ} {R : ℝ} [CompleteSpace E] (L : E →L[ℝ] F) {f : ℂ → E} (hf : CircleIntegrable f c R) : Real.circleAverage (⇑L ∘ f) c R = L (Real.circleAverage f c R)

Circle averages commute with continuous linear maps.

Behaviour with Respect to Arithmetic Operations

theorem Real.circleAverage_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} [NormedDivisionRing 𝕜] [Module 𝕜 E] [NormSMulClass 𝕜 E] [SMulCommClass ℝ 𝕜 E] {f : ℂ → E} {c : ℂ} {R : ℝ} {a : 𝕜} : circleAverage (a • f) c R = a • circleAverage f c R

Circle averages commute with scalar multiplication.

theorem Real.circleAverage_fun_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} [NormedDivisionRing 𝕜] [Module 𝕜 E] [NormSMulClass 𝕜 E] [SMulCommClass ℝ 𝕜 E] {f : ℂ → E} {c : ℂ} {R : ℝ} {a : 𝕜} : circleAverage (fun (z : ℂ) => a • f z) c R = a • circleAverage f c R

Circle averages commute with scalar multiplication.

theorem Real.circleAverage_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f₁ f₂ : ℂ → E} {c : ℂ} {R : ℝ} (hf₁ : CircleIntegrable f₁ c R) (hf₂ : CircleIntegrable f₂ c R) : circleAverage (f₁ + f₂) c R = circleAverage f₁ c R + circleAverage f₂ c R

Circle averages commute with addition.

theorem Real.circleAverage_fun_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {c : ℂ} {R : ℝ} {f₁ f₂ : ℂ → E} (hf₁ : CircleIntegrable f₁ c R) (hf₂ : CircleIntegrable f₂ c R) : circleAverage (fun (z : ℂ) => f₁ z + f₂ z) c R = circleAverage f₁ c R + circleAverage f₂ c R

Circle averages commute with addition.

theorem Real.circleAverage_sum {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {c : ℂ} {R : ℝ} {ι : Type u_4} {s : Finset ι} {f : ι → ℂ → E} (h : ∀ i ∈ s, CircleIntegrable (f i) c R) : circleAverage (∑ i ∈ s, f i) c R = ∑ i ∈ s, circleAverage (f i) c R

Circle averages commute with sums.

theorem Real.circleAverage_fun_sum {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {c : ℂ} {R : ℝ} {ι : Type u_4} {s : Finset ι} {f : ι → ℂ → E} (h : ∀ i ∈ s, CircleIntegrable (f i) c R) : circleAverage (fun (z : ℂ) => ∑ i ∈ s, f i z) c R = ∑ i ∈ s, circleAverage (f i) c R

Circle averages commute with sums.

theorem Real.circleAverage_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f₁ f₂ : ℂ → E} {c : ℂ} {R : ℝ} (hf₁ : CircleIntegrable f₁ c R) (hf₂ : CircleIntegrable f₂ c R) : circleAverage (f₁ - f₂) c R = circleAverage f₁ c R - circleAverage f₂ c R

Circle averages commute with subtraction.

theorem Real.circleAverage_fun_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f₁ f₂ : ℂ → E} {c : ℂ} {R : ℝ} (hf₁ : CircleIntegrable f₁ c R) (hf₂ : CircleIntegrable f₂ c R) : circleAverage (fun (z : ℂ) => f₁ z - f₂ z) c R = circleAverage f₁ c R - circleAverage f₂ c R

Circle averages commute with subtraction.