circleAverage_fun_add — Mathlib

English

Shifting the center by c adds uniformly: circleAverage(f(z+c)) with center 0 equals circleAverage(f) with center c and radius R.

Русский

Смещение центра на c равно переписанию функции через z ↦ z+c и сравнения со средним на центре 0.

LaTeX

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

Lean4

/-- Expression of `circleAverage´ with arbitrary center in terms of `circleAverage` with center zero.
-/
theorem circleAverage_fun_add : circleAverage (fun z ↦ f (z + c)) 0 R = circleAverage f c R :=
  by
  unfold circleAverage circleMap
  congr
  ext θ
  simp only [zero_add]
  congr 1
  ring

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