summable_partition — Mathlib

English

A function on a partition of the index set is summable iff each piece is summable and the sum of their sums is summable.

Русский

Суммируемость функции по разбивке индексов равносильна суммируемости каждой части и сумме сумм по частям.

LaTeX

$$Summable f \\\\iff (∀ j, Summable (fun i => f i)) ∧ Summable (fun j => tsum fun i => f i)$$

Lean4

theorem summable_partition {α β : Type*} {f : β → ℝ} (hf : 0 ≤ f) {s : α → Set β} (hs : ∀ i, ∃! j, i ∈ s j) :
    Summable f ↔ (∀ j, Summable fun i : s j ↦ f i) ∧ Summable fun j ↦ ∑' i : s j, f i := by
  simpa only [← (Set.sigmaEquiv s hs).summable_iff] using summable_sigma_of_nonneg (fun _ ↦ hf _)

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