Theorems · Theorem · measure theory

Real.circleAverage_congr_codiscreteWithin

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

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

Defined in

Mathlib.MeasureTheory.Integral.CircleAverage

Cited by

4 results in Mathlib

Foundations

Depth 257 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace