Lemma A.1

Open

QAlgorithms.Papers.Independent.Intakethird100.P07.pointwiseSummable_subfamily

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $X$ be a topological space, $I$ any index set, and $V$ a complete Hausdorff abelian topological group, equipped with its compatible group uniformity. Let $\phi_i:X\to V$ be a pointwise unconditionally summable family: at each $x$ the net of finite partial sums converges. Then

\forall J\subseteq I\;\forall x\in X,\qquad\sum_{j\in J}\phi_j(x)\text{ converges in }V.

In particular every subfamily is pointwise summable, including the empty subfamily, whose sum is zero. Continuity of the individual functions or of the sums is not asserted.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P07

Formal statement

noncomputable section

universe u v

namespace QAlgorithms.Papers.Independent.Intakethird100.P07

open CategoryTheory Topology TopologicalSpace

/-- Lemma A.1, PDF pp. 32–33: pointwise unconditional summability is
inherited by every subfamily in a complete Hausdorff abelian group. -/
theorem pointwiseSummable_subfamily
    (X : Type u) [TopologicalSpace X] (I : Type v)
    (V : Type u) [AddCommGroup V] [UniformSpace V] [IsUniformAddGroup V]
    [CompleteSpace V] [T2Space V] (phi : I → X → V)
    (hphi : ∀ x, Summable (fun i => phi i x)) :
    ∀ (J : Set I) (x : X), Summable (fun j : J => phi j.val x) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P07

end

Source

Cohomology of Local Cochains, arXiv:1110.2661v2, PDF p. 32, Lemma A.1

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $X$ be any topological space, let $I$ be any index type, and let $V$ be an additive commutative group equipped with a uniform structure making it a uniform additive group, complete and Hausdorff. Let $\phi:I\to(X\to V)$ be any family of functions such that, for every $x\in X$ , the family $(\phi_i(x))_{i\in I}$ is summable, meaning that its finite partial sums converge in $V$ . Then for every subset $J\subseteq I$ and every $x\in X$ , the restricted family $(\phi_j(x))_{j\in J}$ is summable. Neither countability of $I$ nor continuity of the functions $\phi_i$ is assumed; $I$ and $J$ may be empty, in which case the corresponding empty family is summable with sum $0$ .

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph