English
A function f on the sigma-type Σ x, β x is summable iff each fiber is summable and the sum over x of the fiber sums is summable.
Русский
Функция f на сигма-типе Σ x, β x суммируема тогда и только тогда, когда каждое сечение суммируема и сумма по x от сумм по каждому сечению суммируема.
LaTeX
$$$\\\\mathrm{Summable}(f) \\\\iff \\\\Big( \\forall x, \\\\mathrm{Summable}(\\\\lambda y, f \\\\langle x,y \\\\rangle) \\\\Big) \\\\wedge \\\\mathrm{Summable} \\\\big(\\\\lambda x, \\\\sum' y, f \\\\langle x,y \\\\rangle\\\\big)$$$
Lean4
theorem summable_sigma {β : α → Type*} {f : (Σ x, β x) → ℝ≥0} :
Summable f ↔ (∀ x, Summable fun y => f ⟨x, y⟩) ∧ Summable fun x => ∑' y, f ⟨x, y⟩ :=
by
constructor
· simp only [← NNReal.summable_coe, NNReal.coe_tsum]
exact fun h => ⟨h.sigma_factor, h.sigma⟩
· rintro ⟨h₁, h₂⟩
simpa only [← ENNReal.tsum_coe_ne_top_iff_summable, ENNReal.tsum_sigma', ENNReal.coe_tsum (h₁ _)] using h₂
