Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-07-31
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Uniform Dirichlet test: uniformly bounded partial sums times a uniformly decreasing null family give a uniformly convergent function series

Statement

Let XX be a set and let uk,vk:X→Ru_k,v_k:X\to\mathbb{R}. Put An(x):=∑k<nuk(x)A_n(x):=\sum_{k<n}u_k(x). Suppose:

  • there is M≥0M\ge0 such that ∣An(x)∣≤M|A_n(x)|\le M for every nn and xx;
  • vk(x)≥0v_k(x)\ge0 and vk+1(x)≤vk(x)v_{k+1}(x)\le v_k(x) for every kk and xx;
  • vk→0v_k\to0 uniformly on XX.

Then the function series ∑ukvk\sum u_kv_k converges uniformly on XX.

Facts & Assumptions

Given: Functions uk,vk:X→Ru_k,v_k:X\to\mathbb{R} satisfying the three hypotheses in the Statement, with partial sums An(x)=∑k<nuk(x)A_n(x)=\sum_{k<n}u_k(x).

[L1]

Abel summation by parts expresses a finite sum ∑j<rajbj\sum_{j<r}a_jb_j as Arbr−1−∑j<r−1Aj+1(bj+1−bj)A_rb_{r-1}-\sum_{j<r-1}A_{j+1}(b_{j+1}-b_j), where Ar=∑j<rajA_r=\sum_{j<r}a_j (Abel summation by parts: with An=∑k<nakA_n = \sum_{k<n} a_k one has ∑k<nakbk=Anbn−1−∑k<n−1Ak+1 (bk+1−bk)\sum_{k<n} a_k b_k = A_n b_{n-1} - \sum_{k < n-1} A_{k+1}\,(b_{k+1} - b_k) for every n≥1n \ge 1).

[L2]

Finite sums split and telescope, preserve inequalities, and obey the triangle inequality after repeated use of ∣s+t∣≤∣s∣+∣t∣|s+t|\le|s|+|t| (Finite sums and finite products, by recursion, Laws of finite sums and finite products, The triangle inequality, Basic properties of the absolute value).

[L3]

A function series converges uniformly exactly when its tails are uniformly small (A series of real-valued functions converges uniformly if and only if its tails are uniformly small).

Proof

technique · direct
1.1

Let ε>0\varepsilon>0. Uniform convergence vk→0v_k\to0 gives NN such that 0≤vk(x)<ε/(2M+1)0\le v_k(x)<\varepsilon/(2M+1) for every k≥Nk\ge N and every x∈Xx\in X.

givenchoose
1.2

Fix n>m≥Nn>m\ge N and x∈Xx\in X, put p:=m+1p:=m+1, q:=nq:=n, and for p≤r≤qp\le r\le q put Br(x):=∑k=pruk(x)=Ar+1(x)−Ap(x)B_r(x):=\sum_{k=p}^{r}u_k(x)=A_{r+1}(x)-A_p(x).

L2construct
2.1

For every p≤r≤qp\le r\le q, the bound on the AjA_j gives ∣Br(x)∣≤∣Ar+1(x)∣+∣Ap(x)∣≤2M|B_r(x)|\le |A_{r+1}(x)|+|A_p(x)|\le2M.

step 1.2L2
2.2

Applying [L1] to the shifted finite list from pp through qq gives ∑k=pquk(x)vk(x)=Bq(x)vq(x)+∑k=pq−1Bk(x)(vk(x)−vk+1(x))\sum_{k=p}^{q}u_k(x)v_k(x)=B_q(x)v_q(x)+\sum_{k=p}^{q-1}B_k(x)\bigl(v_k(x)-v_{k+1}(x)\bigr).

step 1.2L1L2
3.1

Since vk(x)−vk+1(x)≥0v_k(x)-v_{k+1}(x)\ge0, steps 2.1 and 2.2 with telescoping give ∣∑k=pquk(x)vk(x)∣≤2Mvq(x)+2M∑k=pq−1(vk(x)−vk+1(x))=2Mvp(x)<ε\left|\sum_{k=p}^{q}u_k(x)v_k(x)\right|\le2Mv_q(x)+2M\sum_{k=p}^{q-1}(v_k(x)-v_{k+1}(x))=2Mv_p(x)<\varepsilon.

step 1.1step 2.1step 2.2L2algebra
4.1

The estimate in step 3.1 holds for every n>m≥Nn>m\ge N and x∈Xx\in X, so [L3] proves uniform convergence of ∑ukvk\sum u_kv_k.

step 3.1L3∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 41 results over 11 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources