circleAverage_def — Mathlib

English

The circleAverage is defined as the average of f over the circle of center c and radius R, using the parameterization θ ↦ circleMap(c,R,θ).

Русский

circleAverage определяется как усреднение f по окружности с центром c и радиусом R через параметризацию θ ↦ circleMap(c,R,θ).

LaTeX

$$$circleAverage\ f\ c\ R = \frac{1}{2\pi}\int_{0}^{2\pi} f\big(circleMap\ c\ R\ \theta\big)\,d\theta$$$

Lean4

theorem circleAverage_def : circleAverage f c R = (2 * π)⁻¹ • ∫ θ in 0..2 * π, f (circleMap c R θ) :=
  rfl

Похожие утверждения