circleAverage_fun_smul — Mathlib

English

Circle average on arbitrary circle equals circle average on unit circle after reparameterization, cf. 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

/-- Circle averages commute with scalar multiplication. -/
theorem circleAverage_fun_smul : circleAverage (fun z ↦ a • f z) c R = a • circleAverage f c R :=
  circleAverage_smul

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