Alphabeta MathHow 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.
Variance and covariance identities for random variables
Statement
Let be square-integrable real random variables on one probability space. Then Moreover, covariance is symmetric and bilinear on finite linear combinations. On finite full-power-set probability spaces these formulas reduce to the published finite identities.
Facts & Assumptions
Given: Square-integrable real random variables .
Variance and covariance are the expectations of the centered square and centered product (Moments, variance, and covariance on a probability space).
Expectation is linear on integrable random variables (Linearity, monotonicity, and the modulus bound for expectation).
Finite probability spaces agree with the full-power-set probability-space formalism (Finite probability spaces are exactly finite full-power-set probability spaces).
In the finite model expectation is the weighted sum, and variance and covariance use the same centered-square and centered-product definitions (Expectation of a real random variable on a finite probability space, Variance, standard deviation, and covariance on a finite probability space).
Proof
Since the probability measure has total mass one, makes integrable. Likewise makes integrable. Finite linear combinations of square-integrable variables remain square-integrable by , applied repeatedly. All expectations below are therefore finite.
Expanding and applying [L2] gives Likewise,
The covariance formula in step 2.1 is symmetric in and , so . If and are finite linear combinations of square-integrable real random variables, step 1.1 makes them square-integrable. Expanding and using [L2] gives
On a finite full-power-set probability space, [L3] identifies the measure with its singleton weights. The integral of a finite-valued random variable is the sum of its values times those weights, so [L4] identifies the two expectations and the centered definitions. Thus the formulas in step 2.1 and step 3.1 agree with the finite identities.
Depends on
- Moments, variance, and covariance on a probability space
- Linearity, monotonicity, and the modulus bound for expectation
- Finite probability spaces are exactly finite full-power-set probability spaces
- Expectation of a real random variable on a finite probability space
- Variance, standard deviation, and covariance on a finite probability space
Used by
- Brownian paths have infinite total variation Corollary
- Independence forces covariance to vanish Corollary
- Kolmogorov two-series sufficiency Corollary
- Variance adds for every finite pairwise-independent family Corollary
- Almost sure frequency of heads Example
- An AR(1) covariance forecast and general-RHS Toeplitz solve Example
- Common random numbers can remove finite-difference noise Example
- Gaussian reparameterization gives two gradient estimators Example
- Nonidentical strong law under summable normalized variances Example
- One-step and multistep forecasts for a causal AR(1) Example
- Same state dynamics with distinct observation kernels Example
- 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) Lemma
- Absolutely summable linear filters preserve weak stationarity Lemma
- Bounded centered convergent series have summable variances Lemma
- Covariance kernels of square-integrable fields are positive semidefinite Lemma
- Independent-copy symmetrization of random series Lemma
- Oppositely monotone functions of independent coordinates have nonpositive covariance Lemma
- Summability of truncated normalized variances Lemma
- Coupled finite differences have a covariance-controlled variance Proposition
- A dominated pathwise simulation gradient is unbiased Theorem
- Chebyshev weak law for uncorrelated arrays Theorem
- Classical bounded-sample mean baseline Theorem
- Coefficient and factorial-effect variances under equal replication Theorem
- Covariance is symmetric and bilinear in finite linear combinations Theorem
- Directional Jacobian and Hessian differences retain Taylor and evaluation-noise errors Theorem
- Durbin–Levinson solves the successive prediction equations Theorem
- Etemadi strong law for pairwise independent iid variables Theorem
- Finite-fourth-moment root-n consistency of sample-centered covariance Theorem
- Finite-history forecast equations and error variance Theorem
- Kolmogorov convergence criterion Theorem
- Kolmogorov maximal inequality Theorem
- Kriging systems and mean-square optimality Theorem
- Normal equations for best affine L² prediction Theorem
- Order-two intrinsic variograms are conditionally negative definite Theorem
- Ordinary importance sampling has finite variance and a CLT under a weighted second moment Theorem
- Pairwise-independent Borel-Cantelli frequency law Theorem
- Sample-mean variance and positive semidefinite sample ACVF Theorem
- Strong law under summable normalized variances Theorem
- The likelihood-ratio score gradient is unbiased on fixed support Theorem
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
- Jean-Francois Le Gall, Integration, Probabilities and Stochastic Processes, Section 8.2.1 (standard reference, not scraped)