circleAverage_const — Mathlib

English

The circle average on the unit circle is unchanged by replacing the integration map by (R·z + c) with R=1, c=0, i.e., 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

/-- The circle average of a constant function equals the constant.
-/
theorem circleAverage_const [CompleteSpace E] (a : E) (c : ℂ) (R : ℝ) : circleAverage (fun _ ↦ a) c R = a :=
  by
  simp only [circleAverage, intervalIntegral.integral_const, ← smul_assoc, sub_zero, smul_eq_mul]
  ring_nf
  simp

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