circleAverage_add — Mathlib

English

Circle averages distribute over finite sums: circleAverage (f1 + f2) c R = circleAverage f1 c R + circleAverage f2 c R.

Русский

Средние по окружности распределяются по сумме: circleAverage (f1+f2) = circleAverage f1 + circleAverage f2.

LaTeX

$$$circleAverage\ (f_1 + f_2)\ c\ R = circleAverage\ f_1\ c\ R + circleAverage\ f_2\ c\ R$$$

Lean4

/-- Circle averages commute with addition. -/
theorem circleAverage_add (hf₁ : CircleIntegrable f₁ c R) (hf₂ : CircleIntegrable f₂ c R) :
    circleAverage (f₁ + f₂) c R = circleAverage f₁ c R + circleAverage f₂ c R :=
  by
  rw [circleAverage, circleAverage, circleAverage, ← smul_add]
  congr
  apply intervalIntegral.integral_add hf₁ hf₂

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