Alphabeta Math
CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29
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.

Continuous fn→0 pointwise on [0,1] with ∫01fn=1 for every n

Statement refuted

False claim: if (fn) is a sequence of Riemann integrable functions on [0,1] converging pointwise to f, and f is integrable, then ∫01fn→∫01f.

For n∈N write cn:=ι(n+1)≥1 (The canonical natural ι(n)=n⋅1F of a field, Canonical naturals are positive and strictly increasing) and define the tent fn:[0,1]→R by

fn(x)  :=  {4cn2 x0≤x≤12cn,4cn2(1cn−x)12cn≤x≤1cn,01cn≤x≤1.

Each fn is continuous on [0,1], hence integrable, with

∫01fn  =  1for every n,

while fn(x)→0 for every x∈[0,1]. So the pointwise limit is the zero function, whose integral is 0, and the integrals do not converge to it.

The heights are unbounded: fn attains the value 2cn at x=1/(2cn), and 2cn→∞. That is what the example refutes and what it does not: it refutes the interchange for pointwise convergence, and it says nothing whatever about sequences that are uniformly bounded, for which no theorem is stated on this page in any direction.

Facts & Assumptions

Given: For n∈N, cn=ι(n+1) and the function fn above; a point x∈[0,1] and a real ε>0.

[L6]

For n≥1 the map x↦xn has derivative ι(n)x n−1; sums and scalar multiples of differentiable functions are differentiable with the corresponding derivatives; and ∫pqc=c(q−p) for a constant (For a natural n≥1 the function x↦xn is differentiable everywhere with derivative ι(n) x n−1; for n=0 it is the constant 1, with derivative 0; for a natural n≥1 the function x↦x−n is differentiable at every x≠0 with derivative −ι(n) x−n−1; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, Sums, scalar multiples, products and quotients: (f+g)′(c)=f′(c)+g′(c), (αf)′(c)=αf′(c), (fg)′(c)=f′(c)g(c)+f(c)g′(c), and (f/g)′(c)=(f′(c)g(c)−f(c)g′(c))/g(c)2 when g(c)≠0, If m≤f≤M on [a,b] then m(b−a)≤L(f,P)≤∫ab‾f≤∫ab‾f≤U(f,P)≤M(b−a) for every partition P; in particular every constant function is integrable, with ∫abc=c(b−a), The derivative f′(c)=lim⁡x→cf(x)−f(c)x−c of f:A→R at a point c∈A that is a limit point of A, and differentiability on a set, Integer powers am).

[L7]

A sequence of reals converges to L when for every real ε>0 there is N with ∣an−L∣<ε for all n≥N (Limits and Cauchy sequences of reals, Sequences of reals: bounded, eventually, frequently, tails, subsequences).

Counterexample

technique · direct
1.1

cn≥1 by [L1], so 0<1/(2cn)<1/cn≤1 and the three pieces of the definition subdivide [0,1].

givenL1
2.1

The three formulas agree at the shared endpoints: at x=1/(2cn) both give 4cn2/(2cn)=2cn, and at x=1/cn the second gives 0, which is the third. So fn is a well-defined function and is continuous on [0,1] by [L2], hence integrable by [L3].

step 1.1L2L3
2.2

On [1/cn,1] the function fn is constantly 0, so ∫1/cn1fn=0 by [L6]; when 1/cn=1 this piece is degenerate and the integral is 0 by [L4].

step 1.1L4L6
2.3

Pointwise convergence to 0. At x=0 every fn(0)=0. For x>0, [L1] gives N with 1/ι(N+1)<x, and for n≥N one has cn=ι(n+1)≥ι(N+1), hence 1/cn≤1/ι(N+1)<x, so x lies in the third piece and fn(x)=0.

step 1.1givenL1L8
3.1

On [0,1/(2cn)] the function H(x):=2cn2x2 has H′(x)=4cn2x=fn(x) by [L6], so ∫01/(2cn)fn=H(1/(2cn))−H(0)=2cn2/(4cn2)=1/2 by [L5].

step 2.1L5L6
3.2

On [1/(2cn),1/cn] the function H2(x):=4cn2(x/cn−x2/2) has H2′(x)=4cn2(1/cn−x)=fn(x) by [L6], and H2(1/cn)=4cn2(1/cn2−1/(2cn2))=2 while H2(1/(2cn))=4cn2(1/(2cn2)−1/(8cn2))=3/2; so ∫1/(2cn)1/cnfn=2−3/2=1/2 by [L5].

step 2.1L5L6
3.3

Hence ∣fn(x)−0∣=0<ε for all n≥N, so fn(x)→0 for every x∈[0,1] by [L7].

step 2.3L7
4.1

By [L4] applied twice, ∫01fn=1/2+1/2+0=1 for every n.

step 3.1step 3.2step 2.2L4
5.1

The pointwise limit is the zero function, which is integrable with integral 0 by [L6], while ∫01fn=1 for every n by step 4.1; so the integrals do not converge to the integral of the limit and the claim is false.

step 4.1step 3.3L6L7∎

Remarks

  • What this refutes, stated exactly. It refutes the interchange of a limit with an integral under pointwise convergence alone, even when every fn is continuous and the limit function is as regular as possible. It does not refute, and does not address, any statement about uniformly convergent sequences or about uniformly bounded ones; no such statement is proved on this page, and none is contradicted here.

  • Unboundedness of the heights is essential to the construction and is stated as a feature, not hidden. sup⁡[0,1]fn=2cn grows without bound, and the mass 1 escapes into a spike of shrinking width. A reader who wants a theorem in this direction should note that the hypothesis to look for is a bound on the whole sequence, and that whichever theorem supplies it is not on this page.

  • The integral of the limit exists here. The failure is not that the limit function is non-integrable — it is the zero function — but that the numbers ∫01fn simply do not converge to ∫010. A separate failure, in which the pointwise limit of integrable functions is not integrable at all, is recorded as a false statement on the companion page of The Riemann Integral.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

78 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