Commit 2025-05-09 13:13 bb737a65

feat: add circle averages (#24427) For a function f on the complex plane, introduce the notation circleAverage f c R as a shorthand for the average of f on the circle with center c and radius R. Averages of this form are typically used in analysis of one complex variable.

Raison d'Être

Like IntervalAverage, this notion exists as a convenience. It avoids the hassle of manually eliminating 2 * π every time an average is computed. At least for the moment, it seems that the simplifier is not built to cancel repeating factors in non-trivial formulas.

Why not use IntervalAverage?

Two reasons:

• Length: circleAverage is shorter and easier to read than the interval average of f (circleMap c R θ), taken over the interval 0..2 * π. This is an issue in computations, where splitting the circle average of a sum into a sum of circle averages quickly leads for lengthy formulas unfit for human consumption.
• Ease of use: Manipulating IntervalAverages by applying standard theorems from mathlib often leads to expressions of the form (f + g) (circleMap c R θ), f (circleMap c R θ) + g (circleMap c R θ) and (f + g) ∘ (circleMap c R) that are not equal enough for tactics like rw.