summable_prod_of_nonneg — Mathlib

English

If f is nonnegative on a product α × β, then summability of f over the product is equivalent to the summability of its row-sums and the total sum of those row-sums.

Русский

Если f неотрицательная на произведении α × β, тогда суммируемость по произведению эквивалентна суммируемости сумм по строкам и полной сумме этих сумм.

LaTeX

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

Lean4

theorem summable_prod_of_nonneg {α β} {f : (α × β) → ℝ} (hf : 0 ≤ f) :
    Summable f ↔ (∀ x, Summable fun y ↦ f (x, y)) ∧ Summable fun x ↦ ∑' y, f (x, y) :=
  (Equiv.sigmaEquivProd _ _).summable_iff.symm.trans <| summable_sigma_of_nonneg fun _ ↦ hf _

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