summable_sigma_of_nonneg — Mathlib

English

If f is nonnegative on a sigma-index, then summability of f on the product corresponds to summability of its row sums and total sum.

Русский

Если f неотрицательная на суммируемом индексе, то суммируемость по произведению равна суммируемости по строкам и общей сумме.

LaTeX

$$Summable f \\\\iff (∀ x, Summable (fun y => f (x, y))) ∧ Summable (fun x => tsum fun y => f (x, y))$$

Lean4

theorem summable_sigma_of_nonneg {α} {β : α → Type*} {f : (Σ x, β x) → ℝ} (hf : ∀ x, 0 ≤ f x) :
    Summable f ↔ (∀ x, Summable fun y => f ⟨x, y⟩) ∧ Summable fun x => ∑' y, f ⟨x, y⟩ :=
  by
  lift f to (Σ x, β x) → ℝ≥0 using hf
  simpa using mod_cast NNReal.summable_sigma

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