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.
Bernoulli sample frequencies
Example
Assume countable choice and dependent choice. For IID Bernoulli variables , where , let . Then in probability and The endpoint laws are included.
Facts & Assumptions
IID finite-variance weak law: Let be IID square-integrable real random variables, with and . For , and in and in probability. Also for .
Bernoulli random variables and binomial random variables as sums of independent Bernoulli trials: For , a Bernoulli random variable takes the value with probability and with probability . For , a binomial random variable is a sum of mutually independent Bernoulli variables. When , this is the constant zero random variable.
A Bernoulli variable has mean and variance ; a binomial variable has mean and variance : If is Bernoulli, then and . If is binomial, then These formulas include , , and .
Countably many independent copies of a prescribed law exist: Assume countable choice and dependent choice. Every probability measure on is the common law of a countable independent family of -valued random elements.
Verification
Given: The construction and assumptions above.
The Bernoulli law puts masses and at and . Under countable choice and dependent choice, the countable-copy result constructs a common-space IID sequence with this law. Its mean is and variance , including both endpoints.
The finite-variance IID weak law and its probability bound apply with and , giving the displayed estimate and convergence. If or , all the variables equal on the intersection of their countably many probability-one events, so every sample mean equals there and the error probability is zero, even at .
Depends on
- IID finite-variance weak law
- Bernoulli random variables and binomial random variables as sums of independent Bernoulli trials
- A Bernoulli$(p)$ variable has mean $p$ and variance $p(1-p)$; a binomial$(n,p)$ variable has mean $np$ and variance $np(1-p)$
- Countably many independent copies of a prescribed law exist
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
18 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
- Section 3.2 opening calculation, pp. 54–55 (standard reference, not scraped)