circleAverage_eq_intervalAverage — Mathlib

English

The circle average can be expressed as an interval average over θ ∈ [0, 2π], i.e., circleAverage f c R equals the average of θ ↦ f(circleMap(c,R,θ)) on that interval.

Русский

Среднее по окружности может быть выражено как среднее по интервалу θ ∈ [0, 2π], т.е. circleAverage f c R равно усреднению функции θ ↦ f(circleMap(c,R,θ)) на этом интервале.

LaTeX

$$$circleAverage\ f\ c\ R = \langle\!\langle\theta\in[0,2\pi]\rangle\!\rangle f(circleMap\ c\ R\ \theta)$$$

Lean4

/-- Expression of `circleAverage´ in terms of interval averages. -/
theorem circleAverage_eq_intervalAverage : circleAverage f c R = ⨍ θ in 0..2 * π, f (circleMap c R θ) := by
  simp [circleAverage, interval_average_eq]

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