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.
A polynomial-tail law with finite matrix variance
Example
For let . On with its power-set sigma-algebra, let Set . Thus the two atoms each have mass .
Facts & Assumptions
Given: The countable atomic construction in the Example and the covariance and matrix-variance conventions.
Nonnegative scalar multiples and countable weighted sums of measures, Nonnegative scalar multiples and countable weighted sums of measures are measures, The Dirac set function at a point, and A Dirac set function is a probability measure: the displayed countable weighted sum of finite sums of Dirac probability measures is a measure.
Probability measures and probability spaces: a measure whose total mass is one is a probability measure.
Random elements and real random variables, A measurable function between measurable spaces, and The Borel sigma-algebra of a topological space: the identity map from the full power-set sigma-algebra is a measurable real random variable.
Expectation of a nonnegative or integrable random variable, Nonnegative simple measurable functions, The integral of a nonnegative simple function, The nonnegative integral agrees with the simple integral on simple functions, and Monotone convergence for the integral: expectation of a nonnegative random variable is its integral, finite-valued truncations are simple, and increasing limits pass through the integral.
For rational , converges iff : , , and are finite positive real numbers.
Covariance matrix of a finite-dimensional random vector and Matrix variance for covariance estimation: for and mean zero, and .
Cauchy-Schwarz for random variables: on a probability space, when is square-integrable.
Verification
By [F1], is a measure, and its total mass is by [F5]. Thus [F2] makes a probability measure. The identity map is the real random variable specified by [F3], and for each .
For and , the truncations are nonnegative simple functions increasing to . By [F4] and the finite atom masses, where convergence is [F5]. In particular is integrable by [F7], and its symmetric atom masses give .
By [F6], the covariance is , while the scalar matrix variance is . Therefore is finite and positive.
Fix . The simple truncations increase to , so [F4] gives Indeed the ratio of successive summands is , so the summands do not tend to zero and the series diverges. The law has polynomially decaying atom masses, finite matrix variance, and no finite positive exponential moment.
Depends on
- Covariance matrix of a finite-dimensional random vector
- Matrix variance for covariance estimation
- For rational $p > 0$, $\sum 1/k^p$ converges iff $p > 1$
- Nonnegative scalar multiples and countable weighted sums of measures
- Nonnegative scalar multiples and countable weighted sums of measures are measures
- The Dirac set function at a point
- A Dirac set function is a probability measure
- Probability measures and probability spaces
- Random elements and real random variables
- A measurable function between measurable spaces
- The Borel sigma-algebra of a topological space
- Expectation of a nonnegative or integrable random variable
- Nonnegative simple measurable functions
- The integral of a nonnegative simple function
- The nonnegative integral agrees with the simple integral on simple functions
- Monotone convergence for the integral
- Cauchy-Schwarz for random variables
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
56 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
- Stanislav Minsker and Xiaohan Wei, Estimation of the Covariance Structure of Heavy-Tailed Distributions, §2 (standard reference, not scraped)