circleAverage_comp_comm — Mathlib

English

If f(x) ≤ a for all x on the circle, then circleAverage f c R ≤ a.

Русский

Если f(x) ≤ a для всех точек окружности, то circleAverage f c R ≤ a.

LaTeX

$$$\forall x\in\operatorname{sphere}(c,|R|): f(x) \le a \Rightarrow circleAverage\ f\ c\ R \le a$$$

Lean4

/-- Circle averages commute with continuous linear maps. -/
theorem _root_.ContinuousLinearMap.circleAverage_comp_comm [CompleteSpace E] (L : E →L[ℝ] F) {f : ℂ → E}
    (hf : CircleIntegrable f c R) : circleAverage (L ∘ f) c R = L (circleAverage f c R) :=
  by
  unfold circleAverage
  rw [map_smul]
  congr
  exact L.intervalIntegral_comp_comm hf

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