Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)
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.

Product martingale from independent mean one factors

Example

Assume AC. For given independent real integrable (Yk)k1 with EYk=1, the products M0=1 and Mn=k=1nYk form a martingale for F0={,Ω} and Fn=σ(Y1,,Yn). Factors may be signed.

Facts & Assumptions

Given: The hypotheses and conventions in the example.

[F3]

Finite products of integrable functions of independent variables are integrable, and expectations factor. Expectations factor over finite products of independent random variables.

[F4]

The sigma-algebra of a finite past is independent of the next variable sigma-algebra. Disjoint groups of an independent sigma-algebra family remain independent.

[F5]

An integrable variable independent of a sigma-algebra has constant conditional mean equal to its expectation. Conditioning a known variable and an independent variable.

[F6]

A finite measurable factor may be taken out when its product with the integrable input is integrable. Taking out what is known.

[F7]

AC supplies the inherited conditional-expectation existence and any stated choice of versions. The Axiom of Choice.

Verification

technique · direct
1.1

The generated finite-history sigma-algebras form a filtration; finite products are adapted. Apply factorization to the Borel functions tt to get EMn=k=1nEYk< for n1; at n=0 it equals one. Group independence separates σ(Yn+1) from the finite past, so E[Yn+1Fn]=EYn+1=1 (also for the trivial past at zero).

givenF1F2F3F4F5
2.1

The variable Mn is finite and Fn-measurable. Both Yn+1 and MnYn+1=Mn+1 are integrable by step 1.1. The unbounded taking-out clause therefore gives E[Mn+1Fn]=MnE[Yn+1Fn]=Mn. This proves the martingale assertion Martingale submartingale and supermartingale. AC is inherited from CE; neither positivity nor identical distribution of factors was used. If one adjoins the deterministic factor Y0=1, the displayed filtration is exactly the natural filtration of the resulting zero-based factor process Natural filtration of a process, not necessarily that of the products.

F6F7step 1.1
3.1

For example take Ω={1,3}2 with four equal masses, let Y1,Y2 be its coordinates and Yk=1 for k3. Each first factor has mean (1+3)/2=1 and absolute mean 2; coordinate rectangle counting proves independence. The four values of M2 are 1,3,3,9, so EM2=1 and EM2=4=22. Conditional on Y1=1 the product averages (13)/2=1, and conditional on Y1=3 it averages (3+9)/2=3.

step 1.1step 2.1

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

32 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