circleAverage_const_on_circle — Mathlib

English

Equivalence between circleAverage on arbitrary circle and unit circle via transformation z ↦ (R z + c).

Русский

Эквивалентность между средними по произвольной окружности и по единичной окружности через преобразование z ↦ (R z + c).

LaTeX

$$$circleAverage\ f\ c\ R = circleAverage\ (f\circ(\lambda z. R\,z + c))\ 0\ 1$$$

Lean4

/-- If `f x` equals `a` on for every point of the circle, then the circle average of `f` equals `a`.
-/
theorem circleAverage_const_on_circle [CompleteSpace E] {a : E} (hf : ∀ x ∈ Metric.sphere c |R|, f x = a) :
    circleAverage f c R = a := by
  rw [circleAverage]
  conv =>
    left; arg 2; arg 1
    intro θ
    rw [hf (circleMap c R θ) (circleMap_mem_sphere' c R θ)]
  apply circleAverage_const a c R

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