circleAverage_sum — Mathlib

English

For a finite index set ι, circleAverage of the sum over i of f_i equals the sum over i of circleAverage f_i.

Русский

Для конечного множества индексов ι среднее по окружности от суммы функций равно сумме средних.

LaTeX

$$$circleAverage\ (\sum_{i\in s} f_i)\ c\ R = \sum_{i\in s} circleAverage\ (f_i)\ c\ R$$$

Lean4

/-- Circle averages commute with sums. -/
theorem circleAverage_sum {ι : Type*} {s : Finset ι} {f : ι → ℂ → E} (h : ∀ i ∈ s, CircleIntegrable (f i) c R) :
    circleAverage (∑ i ∈ s, f i) c R = ∑ i ∈ s, circleAverage (f i) c R :=
  by
  unfold circleAverage
  simp [← Finset.smul_sum, intervalIntegral.integral_finset_sum h]

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