Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passaudited 2026-08-28
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 typewriter sequence converges in measure and in L^1 but nowhere pointwise

Example

On [0,1] with Lebesgue measure, define f0:=0,f2k+j:=χIk,jfor k≥0, 0≤j<2k, where Ik,j=[j2−k,(j+1)2−k) for j<2k−1 and Ik,2k−1=[1−2−k,1]. Then:

  1. fn→0 in measure.
  2. fn→0 in L1([0,1]).
  3. For every x∈[0,1], the sequence (fn(x)) does not converge.

So the typewriter sequence separates convergence in measure and in L1 from almost-everywhere convergence.

Facts & Assumptions

Given: Lebesgue measure on [0,1] and the typewriter sequence (fn) of the Example, including its initial value f0=0.

[L1]

Convergence in measure means that for every real ε>0, μ({∣fn−f∣>ε})→0. (Convergence in measure)

[L2]

Convergence in L1(μ) means ∫∣fn−f∣ dμ→0. (Convergence in L^1(mu))

[L3]

Almost-everywhere convergence means pointwise convergence off a measurable null set. (Convergence almost everywhere relative to a measure)

Verification

technique · direct
1.1givenL2algebra

If 2k≤n<2k+1, then fn is the indicator of a dyadic interval of length 2−k, so ∫01∣fn∣ dλ=2−k.

1.2given

Fix x∈[0,1]. In each generation k≥1 there is exactly one interval Ik,jk containing x, so f2k+jk(x)=1. The same generation also contains intervals missing x, hence infinitely many indices n with fn(x)=0. So (fn(x)) takes the values 0 and 1 infinitely often and therefore does not converge.

2.1step 1.1L2

Since 2k≤n<2k+1 forces k→∞ as n→∞, step 1.1 gives ∫01∣fn∣ dλ→0. Therefore fn→0 in L1([0,1]) by [L2].

2.2step 1.1L1

Fix ε∈(0,1). When 2k≤n<2k+1, the set {∣fn−0∣>ε} is exactly the support interval of fn, so it has measure 2−k. Thus these bad-set measures tend to 0, and [L1] gives fn→0 in measure.

3.1step 1.2step 2.1step 2.2L3∎

Step 2.2 proves convergence in measure, step 2.1 proves convergence in L1, and step 1.2 shows that [L3] fails at every point.

Depends on

Used by

Dependency tree · two levels

6 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