LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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.

The nonlinear geometric iteration: an explicit threshold forces convergence to zero

Statement

Let $δ > 0$ , $C \geq 1$ , $B \geq 1$ , and let $(Y_{j})_{j \geq 0}$ be a sequence of nonnegative real numbers with $Y_{j + 1} \leq C B^{j} Y_{j}^{1 + δ} (j \geq 0) .$ Put $λ : = (2 B)^{- 1 / δ} \in (0, 1)$ . If $Y_{0} \leq C^{- 1 / δ} (2 B)^{- 1 / δ^{2}}$ , then $Y_{j} \leq Y_{0} λ^{j} (j \geq 0),$ so in particular $Y_{j} \to 0$ and $\sum_{j \geq 0} Y_{j} < + \infty$ . Equivalently: the explicit smallness condition $C Y_{0}^{δ} \leq (2 B)^{- 1 / δ}$ on the initial datum forces geometric decay of the whole sequence with ratio $λ$ .

Facts & Assumptions

Given: real numbers $δ > 0$ , $C \geq 1$ , $B \geq 1$ , and a sequence $(Y_{j})_{j \geq 0}$ of nonnegative reals with $Y_{j + 1} \leq C B^{j} Y_{j}^{1 + δ}$ for all $j \geq 0$ ; put $λ = (2 B)^{- 1 / δ}$ .

[F1]

Real powers with positive base: $λ^{δ} = 1 / (2 B)$ , so $B λ^{δ} = 1 / 2$ ; moreover $0 < λ < 1$ because $2 B \geq 2$ , and for $a > 0$ and real $u, v$ one has $a^{u + v} = a^{u} a^{v}$ , $(a^{u})^{v} = a^{u v}$ and $a^{0} = 1$ (Real powers for positive bases, with the zero-base positive-exponent convention). Also $t \mapsto t^{1 + δ}$ is nondecreasing on $[0, + \infty)$ because $1 + δ > 0$ .

[L1]

For $0 < λ < 1$ the sequence of integer powers $(λ^{j})_{j \geq 0}$ is null (For $∣ r ∣ < 1$ the sequence $r^{k}$ is null, and for $∣ r ∣ > 1$ the sequence $∣ r ∣^{k}$ diverges to $+ \infty$ ).

Proof

technique · direct induction with the ansatz $Y_j\le Y_0\lambda^j$, using that the induction requirement is largest at $j=0$

1.1givenF1algebra

The hypothesis is equivalent to $C Y_{0}^{δ} \leq λ$ : raising $Y_{0} \leq C^{- 1 / δ} (2 B)^{- 1 / δ^{2}}$ to the power $δ > 0$ gives $Y_{0}^{δ} \leq C^{- 1} (2 B)^{- 1 / δ} = C^{- 1} λ$ , and conversely this inequality implies the original one by raising to the power $1 / δ > 0$ and using the power identities of [F1]. Together with [F1] the data therefore satisfy $0 < λ < 1$ , $B λ^{δ} = 1 / 2$ and $C Y_{0}^{δ} \leq λ$ .

2.1step 1.1F1givenalgebra

Induction claim: $Y_{j} \leq Y_{0} λ^{j}$ for every $j \geq 0$ . The case $j = 0$ is $Y_{0} \leq Y_{0}$ . Assume the claim for some $j \geq 0$ . Then the recursion, the nonnegativity of $Y_{j}$ and the induction hypothesis give $Y_{j + 1} \leq C B^{j} Y_{j}^{1 + δ} \leq C B^{j} (Y_{0} λ^{j})^{1 + δ} = C B^{j} Y_{0}^{1 + δ} λ^{j (1 + δ)}$ , so it suffices to show $C B^{j} Y_{0}^{δ} λ^{j δ - 1} \leq 1$ , equivalently $Y_{0} λ^{j + 1} \geq C B^{j} Y_{0}^{1 + δ} λ^{j (1 + δ)}$ . By step 1.1 and [F1], $C B^{j} Y_{0}^{δ} λ^{j δ - 1} = (C Y_{0}^{δ} / λ) (B λ^{δ})^{j} = (C Y_{0}^{δ} / λ) 2^{- j} \leq C Y_{0}^{δ} / λ \leq 1$ . Hence $Y_{j + 1} \leq Y_{0} λ^{j + 1}$ , and induction proves the claim for all $j$ .

3.1step 2.1L1F1algebra∎

By step 2.1, $0 \leq Y_{j} \leq Y_{0} λ^{j}$ with $0 < λ < 1$ , so $Y_{j} \to 0$ by [L1]. Moreover the finite geometric sum identity $(1 - λ) \sum_{j = 0}^{N} λ^{j} = 1 - λ^{N + 1}$ , proved by induction on $N$ , gives $\sum_{j = 0}^{N} Y_{j} \leq Y_{0} \sum_{j = 0}^{N} λ^{j} \leq Y_{0} / (1 - λ)$ for every $N$ , because $λ^{N + 1} \geq 0$ ; the partial sums of the nonnegative series $\sum_{j \geq 0} Y_{j}$ are therefore increasing and bounded above by $Y_{0} / (1 - λ)$ , so the series converges and $\sum_{j \geq 0} Y_{j} \leq Y_{0} / (1 - λ) < + \infty$ . Only the displayed power identities and the null geometric sequence are used, so no choice principle is used.

Depends on

Used by

Dependency tree · two levels

23 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Bozhidar Velichkov, Elliptic PDEs: Teorema di De Giorgi (Universita di Pisa; complete 7-page note, in Italian) (standard reference, not scraped)
Leon Simon, Lectures on Partial Differential Equations (Stanford University; complete author scan, 118 sheets reproducing the 223 printed pages of the manuscript, two logical pages per sheet) (standard reference, not scraped)