Alphabeta Math
CounterexampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedaudited 2026-09-10
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.

Weak law does not imply strong law

Statement refuted

A weak sample-mean law need not be a centered strong law. Assuming AC, there are integrable real (Xn) with Sn/n→0 in probability but (Sn−ESn)/n not tending to zero almost surely.

Facts & Assumptions

[F1]

The recursion theorem: Let (N,0,σ) be a Peano system (def-peano-system), in particular the natural numbers N (def-natural-numbers). For any set A, any element a∈A, and any function f:A→A, there is a unique function g:N→A such that g(0)=a and g(σ(n))=f(g(n)) for all n∈N.

[F2]

A box in Rn with parameters ai≤bi is Lebesgue measurable of measure ∏i<n(bi−ai), whichever of its faces are included: Let n≥1, assume the Axiom of Countable Choice (def-countable-choice), and let ai≤bi be reals for i<n. Write

R∘:={ x∈Rn:ai<xi<bi for every i<n },R‾:=[a,b]={ x∈Rn:ai≤xi≤bi for every i<n }

(def-multidimensional-rectangle-and-volume). Then R∘ is open and R‾ is closed, so both are Borel and Lebesgue measurable, and every set R with R∘⊆R⊆R‾ is Lebesgue measurable with

λn(R)  =  ∏i<n(bi−ai).

In particular this covers the four one-dimensional face conventions in each coordinate — the open box, the closed box [a,b], the half-open box B(a,b)=∏i<n(ai,bi] of def-half-open-box, and every mixture of them, in any combination of coordinates — and it gives measure 0 to all of them whenever ai=bi for some i<n. For a half-open box with infinite parameters the value is already λn(B)=vol⁡(B) (thm-lebesgue-measure-is-a-complete-measure).

[F3]

Countably many independent copies of a prescribed law exist: Assume countable choice and dependent choice. Every probability measure ν on (S,Σ) is the common law of a countable independent family of S-valued random elements.

[F4]

Measurable coordinatewise functions preserve independence: Let (Xi)i∈I be an independent family of random elements Xi:(Ω,F,P)→(Si,Σi). For each i, let gi:(Si,Σi)→(Ti,Ti) be measurable. Then the family (gi∘Xi)i∈I is independent.

[F5]

Second Borel-Cantelli lemma under pairwise independence: Let (An)n∈N be pairwise independent events with ∑n=0∞P(An)=+∞. Then P(An i.o.)=1.

Counterexample

Given: The objects, hypotheses and definitions in the statement. Its conclusions are to be established below.

1.1F1F2F3F4

AC restricted to a countable family gives CC; choosing a successor for each point of an entire relation and using F1 gives DC. On ((0,1),B,λ) the identity U has P(U≤t)=t for 0<t<1 by F2. F3 supplies IID copies Un. Let Bn=1{Un≤1/(n+1)}, which are independent by F4.

1.2givenalgebra

Set B0=0 and Xn=nBn−(n−1)Bn−1. These finite-valued variables are integrable; telescoping gives Sn=nBn. Thus P(∣Sn/n∣>ε)≤1/(n+1)→0 for every ε>0, and ESn/n=1/(n+1)→0.

2.1F5step 1.2∎

The sum of 1/(n+1) diverges: each block 2j≤n+1<2j+1 contributes at least 1/2. The complementary probabilities n/(n+1) also have divergent sum. Apply F5 to the independent events Bn=1 and separately to Bn=0. Both occur infinitely often on a common conull event. Hence the centered averages Bn−1/(n+1) have limsup 1 and liminf 0 there, refuting the centered strong law while step 1.2 establishes the weak law.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

50 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