Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)
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.

McDiarmid bounded-differences inequality

Statement

Assume AC. Let n≥1, let Zi:(Ω,F,P)→(Si,Σi) be independent random elements, meaning measurable maps (Random elements and real random variables), with laws μi given by pushforward (Law or distribution of a random element). Put μ=⨂i=1nμi on the finite product sigma-algebra (The product sigma-algebra and its finite iterates). Let f:∏i=1nSi→R be product-measurable with ∫∣f∣ dμ<∞. Suppose finite deterministic constants ci≥0 satisfy ∣f(z1,…,zi,…,zn)−f(z1,…,zi′,…,zn)∣≤ci for every fixed setting of the other coordinates and every zi,zi′. The independent product-law theorem identifies the law of Z=(Z1,…,Zn) as μ. Applying change of variables for expectation first to ∣f∣ and then to f makes f(Z) integrable and gives Ef(Z)=∫f dμ. Put V=∑i=1nci2. For t>0, if V>0 then P(f(Z1,…,Zn)−Ef(Z1,…,Zn)≥t)≤exp⁡ ⁣(−2t2V), and if V=0 this probability is 0. The same bound holds for the lower tail, so the two-sided probability is at most 2e−2t2/V when V>0.

Facts & Assumptions

Given: AC, independent random elements Zi, an integrable measurable real function of them, and the deterministic coordinate oscillation bounds in the Statement.

[A1]

Assume AC, the Axiom of Choice. It is used for the conditional-expectation and conditional-Hoeffding suppliers (The Axiom of Choice).

[F1]

The product-integral construction gives integrable adapted Mi, with Mn=f(Z), M0=∫f dμ, event-integral-zero differences, and predictable endpoints of width at most ci (Doob differences inherit coordinate oscillation widths).

[F2]

Conditional expectation is the almost-sure class of integrable measurable versions satisfying all event-integral identities (Conditional expectation as an ae class).

[F3]

Under AC, an integrable adapted process is a martingale when E[Mi∣Fi−1]=Mi−1 almost surely (Martingale submartingale and supermartingale).

[F4]

If a martingale difference has predictable finite endpoints of deterministic width ci, its conditional exponential moment is at most eλ2ci2/8 (Conditional Hoeffding bound for bounded martingale differences).

[F5]

Conditional expectation preserves the unconditional expectation (Basic algebra and order properties of conditional expectation).

[F6]

A bounded measurable factor known under Fi−1 can be taken outside conditional expectation (Taking out what is known).

[F7]

For Y≥0 and r>0, P(Y≥r)≤E[Y]/r (Markov's inequality for random variables).

[F8]

Probability is subadditive on finite unions (Basic identities for a probability measure).

[F9]

The joint law of independent random elements is the product of their marginal laws; for measurable f with ∫∣f∣ dμ<∞, change of variables applied to ∣f∣ gives f(Z)∈L1 and applied to f gives Ef(Z)=∫f dμ (Independent random elements have product joint law, Change of variables for expectation).

[F11]

Every closed bounded interval [a,b] with a≤b is compact (Heine-Borel by bisection: every closed bounded interval [a,b] is compact).

[F12]

A continuous real function is bounded on a compact subset of R (A continuous real function on a compact subset of R is bounded).

Proof

1.1A1F1F2F3F9given

By [F9], the joint law of Z=(Z1,…,Zn) is μ, so the product integral in the statement is Ef(Z). By [F1], take the product-integral sequence Mi and its differences Di=Mi−Mi−1. For every A∈Fi−1, [F1] gives ∫AMi dP=∫AMi−1 dP. By [F2] and AC, Mi−1 is a version of E[Mi∣Fi−1], so [F3] makes (Mi,Fi) a martingale. The same lemma gives finite predictable endpoints Ai≤Di≤Bi with Ai≤0≤Bi and Bi−Ai≤ci.

2.1A1F1F2F4step 1.1

The event-integral identity of [F1] and [F2] give E[Di∣Fi−1]=0. Applying [F4] to these martingale differences and their endpoints gives E[eλDi∣Fi−1]≤eλ2ci2/8 for every real λ. Since the endpoints contain zero and have width at most ci, ∣Di∣≤ci almost surely.

3.1F5F6F10F11F12step 2.1algebraconstruct

Put Sk=Mk−M0=∑i=1kDi and S0=0. Step 2.1 bounds each difference by ci, hence Sk−1∈[−C,C] for C:=∑i<kci. This closed bounded interval is compact by [F11], and x↦eλx is continuous by [F10] and continuity of scalar multiplication, so [F12] makes eλSk−1 bounded. Also x↦eλx is Borel: its open-set preimages are open, and the class of Borel sets whose preimages are Borel is a sigma-algebra containing the opens, hence contains the Borel sigma-algebra (The Borel sigma-algebra of a topological space). For each Borel B, the preimage of B under eλSk−1 is Sk−1−1((x↦eλx)−1(B)), so this factor is Fk−1-measurable. By the addition formula in [F10], eλSk=eλSk−1eλDk; conditional expectation preservation [F5] and taking out the known factor [F6] give EeλSk≤eλ2ck2/8EeλSk−1. Finite induction yields EeλSn≤eλ2V/8.

4.1F7F10step 2.1step 3.1algebra

If V=0, all ci=0, so step 2.1 gives Di=0 almost surely and Sn=0. If V>0 and λ>0, then eλSn is nonnegative and Sn≥t implies eλSn≥eλt>0 by [F10]. Markov [F7] and step 3.1 give P(Sn≥t)≤eλ2V/8/eλt=e−λt+λ2V/8 by the reciprocal and addition formulas in [F10]. Choosing λ=4t/V gives the stated upper-tail bound.

5.1A1F8step 4.1algebra∎

Apply the same argument to −f for the lower-tail bound. For V>0, [F8] combines the two tails; step 4.1 handles V=0.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

100 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