r-irbe Measure Theory & Probability Mathematics
Measure-theoretic and probabilistic foundations for stochastic models, convergence guarantees, mixing time analysis, ergodic properties, and uncertainty quantification.
Routing
- USE FOR: Measure theory, probability theory, stochastic processes, ergodic theory, and concentration inequalities. Use for mathematical reasoning about probability spaces, random variables, convergence, mixing, and probabilistic arguments. Covers both theoretical foundations and applied probabilistic methodology.
- DO NOT USE FOR: Lean proofs in this domain (use @lean-math-stochastic); time-series analysis (use @math-time-series); topology/analysis (use @math-topology-analysis).
- TRIGGERS: measure theory, probability, stochastic process, ergodic theory, concentration inequality, Radon-Nikodym.
Workflow
- Classify the question: measure space, σ-algebra, integration, conditional, martingale, ergodic, or concentration.
- Pick the matching section; identify the Mathlib namespace (
MeasureTheory,ProbabilityTheory). - Produce the mathematical answer; cite the relevant Mathlib lemma and verify it exists at the current pin (per the
verification disciplinememory). - Hand off: to
@lean-math-stochasticfor the Lean proof, to@lean-researchfor pin-verification, to@lean-zettelkasten.
Recovery & STOP
- STOP if the question is purely time-series — delegate to
@math-time-series. - STOP if topology/analysis dominates — delegate to
@math-topology-analysis. - STOP if a Mathlib symbol cited cannot be verified at the current pin — escalate to
@lean-research.
Handoffs
- Predecessors:
agent:gateway,skill:lean-research. - Successors:
skill:lean-math-stochastic,skill:lean-research,skill:lean-zettelkasten.
Detailed reference
Full content for math-measure-probability lives in
references/math-measure-probability-handbook.md.
Load that file when the skill is convened; the SKILL.md only carries
the dispatch contract and the parts index.
| Section | Topic |
|---|---|
| Part 1 | Measure Theory Foundations |
| Part 2 | Probability Theory |
| Part 3 | Concentration Inequalities |
| Part 4 | Stochastic Processes |
| Part 5 | Ergodic Theory |
| Part 6 | Bayesian Methods |
| Part 7 | Extreme Value Theory |
| Part 8 | Project-specific Probabilistic Models |
| Part 9 | Formalization Connections |
See also
../../references/math-measure-probability-handbook.md— Full handbook (extracted from this skill)../lean-math-stochastic/SKILL.md— Successor../lean-research/SKILL.md— Successor../lean-zettelkasten/SKILL.md— Successor