Documentation

Mathlib.MeasureTheory.Integral.CircleAverage

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 elemininate 2 * π every time an average is computed.

Note: Like the interval average defined in Mathlib.MeasureTheory.Integral.IntervalAverage, 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.

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 #

source
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).

Equations
Instances For
    source
    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 θ)
    source
    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.

    source
    @[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.

    source
    theorem Real.circleAverage_fun_add {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.

    Congruence Lemmata #

    source
    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.

    source
    @[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.

    source
    @[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.

    source
    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.

    Behaviour with Respect to Arithmetic Operations #

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

    Circle averages commute with scalar multiplication.

    source
    theorem Real.circleAverage_fun_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 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.

    source
    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.

    source
    theorem Real.circleAverage_sum {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {c : ℂ} {R : ℝ} {ι : Type u_3} {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.