circleAverage_eq_circleAverage_zero_one

English

Circle average over any circle equals the circle average over the unit circle after a linear change of variables: circleAverage f c R = circleAverage (f ∘ (R·z + c)) 0 1.

Русский

Среднее по окружности при произвольном радиусе превращается в среднее по единичной окружности после линейного изменения переменных: circleAverage f c R = circleAverage (f ∘ (R·z + c)) 0 1.

LaTeX

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

Lean4

/-- Express the circle average over an arbitrary circle as a circle average over the unit circle.
-/
theorem circleAverage_eq_circleAverage_zero_one : circleAverage f c R = (circleAverage (fun z ↦ f (R * z + c)) 0 1) :=
  by
  unfold circleAverage circleMap
  congr with θ
  ring_nf
  simp

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