Learn · Probability and statistics
Axeyum for probability and statistics
Axeyum now has a finite, rational-valued probability development with expectation, variance, covariance, concentration, and a weak law of large numbers.
a103b3db3 Measured Source Axeyum fact ledger and implementation documentation After reading this guide, you should be able to
Learning objectives
- Identify the parts of Axeyum that are relevant to probability and statistics.
- Distinguish implemented results from the current research frontier.
- Open a lesson or artifact that provides the underlying definitions and evidence.
Current state
What can be proved without a measure-theory library?
The formal library defines finite rational-valued random variables and distributions. It proves nonnegative expectation, variance identities, covariance laws, Cauchy-Schwarz for covariance, Chebyshev's inequality for sample means, and a weak law of large numbers under pairwise uncorrelated assumptions.
This constructive finite-probability layer computes sums and bounds over explicit finite carriers, and its kernel facts have empty axiom footprints. A measure-theoretic layer is the next stage of the development.
Why it matters
What the current work makes possible
- The weak law is connected to its algebraic and inequality dependencies in the ledger.
- Finite distributions and rational-valued variables can be evaluated directly.
- The development provides a concrete base for testing statistical certificates from other Axeyum components.
Results to inspect
Open the evidence
What comes next
Extend the present base
The next finite layer includes independence libraries, common named distributions, moment bounds, tail inequalities, and statistical estimators.
Measure-theoretic probability will follow the analysis and topology work needed for sigma-algebras, measures, measurable functions, and the Lebesgue integral.
Where to begin