sum — Mathlib

English

Finite sums of CircleIntegrable functions are CircleIntegrable.

Русский

Конечные суммы CircleIntegrable функций также CircleIntegrable.

LaTeX

$$$\text{CircleIntegrable.finsum }(\text{f}) \;\text{что } \text{∀ i, CircleIntegrable } f_i \Rightarrow \text{CircleIntegrable}(\sum_i f_i).$$$

Lean4

/-- Sums of circle integrable functions are circle integrable. -/
protected theorem sum {ι : Type*} (s : Finset ι) {f : ι → ℂ → E} (h : ∀ i ∈ s, CircleIntegrable (f i) c R) :
    CircleIntegrable (∑ i ∈ s, f i) c R :=
  by
  rw [CircleIntegrable,
    (by aesop : (fun θ ↦ (∑ i ∈ s, f i) (circleMap c R θ)) = ∑ i ∈ s, fun θ ↦ f i (circleMap c R θ))] at *
  exact IntervalIntegrable.sum s h

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