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

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} [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.

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

    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.