Lemma A.2

Open

QAlgorithms.Papers.Independent.Intakethird100.P07.pointwiseSummable_absolute

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

prove2quantum

Let $X$ be a topological space and $(\phi_i:X\to\mathbb R)_{i\in I}$ a family whose finite partial sums converge at every point. Then its absolute-value family is pointwise summable:

\forall x\in X,\qquad\sum_{i\in I}|\phi_i(x)|\text{ converges in }\mathbb R.

The sums are unconditional, indexed by finite subsets of $I$ . This is an existence statement about pointwise sums, without a continuity or local uniform convergence conclusion.

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.2, PDF p. 33: the absolute-value family is pointwise summable.
There is no continuity or local uniform convergence assertion here. -/
theorem pointwiseSummable_absolute
    (X : Type u) [TopologicalSpace X] (I : Type v) (phi : I → X → ℝ)
    (hphi : ∀ x, Summable (fun i => phi i x)) :
    ∀ x, Summable (fun i => |phi i x|) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P07

end

Source

Cohomology of Local Cochains, arXiv:1110.2661v2, PDF p. 33, Lemma A.2

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 $\phi:I\to(X\to\mathbb R)$ be a family of real-valued functions. Suppose that for every $x\in X$ , the family $(\phi_i(x))_{i\in I}$ is summable, meaning that its finite partial sums converge in $\mathbb R$ . Then for every $x\in X$ , the family $(|\phi_i(x)|)_{i\in I}$ is also summable. No countability assumption on $I$ or continuity assumption on the functions is imposed; the empty index type is included, and if $X$ is empty both pointwise assertions are vacuous.

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