finsum — Mathlib

English

The finsum of CircleIntegrable functions is CircleIntegrable.

Русский

Обобщенная сумма CircleIntegrable функций является CircleIntegrable.

LaTeX

$$$\text{CircleIntegrable.finsum}(\{ f_i \}) \Rightarrow \text{CircleIntegrable}(\sum_i^\text{finite} f_i,c,R).$$$

Lean4

/-- `finsum`s of circle integrable functions are circle integrable. -/
protected theorem finsum {ι : Type*} {f : ι → ℂ → E} (h : ∀ i, CircleIntegrable (f i) c R) :
    CircleIntegrable (∑ᶠ i, f i) c R :=
  by
  by_cases h₁ : (Function.support f).Finite
  · rw [finsum_eq_sum f h₁]
    exact CircleIntegrable.sum h₁.toFinset (fun i _ ↦ h i)
  · rw [finsum_of_infinite_support h₁]
    apply circleIntegrable_const

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