formalproofsmdplib0.1.0

Formalization of MDP Theory

Formalizing Markov Decision Processes in Lean

CI Documentation

Verified Lean algorithms for tabular MDPs, with two goals:

  1. Algorithms that solve robust and risk-averse MDPs of moderate size.
  2. Proofs of correctness and of fundamental MDP properties, usable on their own for structural results such as the optimality of a policy class.

The API documentation and the companion paper are published by CI on every push to main.

Library Contents

Sample spaces are finite ([FinEnum Ω]), so there are no measurability side conditions. Two types appear:

  • W: probabilities, and values that are averaged with them (expectation, CVaR). Any linear ordered field — ℚ makes every definition computable (see MDPLibTest.lean), ℝ gives the standard theory.
  • V: values that are only compared (events, ℙ, CDF, quantiles, VaR). Any linear order, e.g. W, ℕ, ℤ.

They are separate so that order-only results apply to any ordered values, and so that @[to_dual (dont_translate := W)] can derive mirror-image results by reversing the order on values without reversing it on probabilities.

Mathlib's measure-theoretic probability is not used: it is noncomputable, fixed to ℝ/ℝ≥0∞, and has no quantiles or VaR. Its scalar-generic convexity API (Finset.centerMass, StdSimplex) is reused instead.

Probability foundations

MDPLib/Probability/Defs.lean, MDPLib/Probability/Prelude.lean

ResultLean name
Finite distribution on Ω (nonneg weights summing to one), Dirac distributionFindist, Findist.Δ, Findist.dirac
A distribution forces its sample space to be nonemptyFindist.nonempty
Random variables as bare functions Ω → V; events as Ω → Bool with Mathlib's Boolean algebra (⊔, ⊓)FinRV, FinRV.sup_eq_or, FinRV.inf_eq_and
Comparison events X ≤ᵣ t, X <ᵣ t, X ≥ᵣ t, X >ᵣ t, X =ᵣ y and the indicator 𝕀FinRV.leq, FinRV.lt, FinRV.geq, FinRV.gt, FinRV.eq, FinRV.indicator
Probability ℙ[B // P], conditional probability ℙ[B | C // P]Findist.probability, Findist.probabilityCond
Expectation 𝔼[X // P], conditional expectation 𝔼[X | B // P] and the conditional-expectation random variable 𝔼[X |ᵣ L // P]Findist.expect, Findist.expectCond, Findist.expectCondRV
Probability as the expectation of an indicatorFindist.probability_eq_expect_indicator
Decomposition of a random variable along a discrete label X = ∑ᵢ X · 𝕀[L = i]FinRV.eq_sum_mul_indicatorEq, Findist.expect_eq_sum_mul_indicatorEq
Convexity bounds for two-point mixtures; Jensen's inequality for |·| on the uniform distributionIsProb.self_le_combo_of_le, IsProb.combo_le_self_of_ge, Matrix.abs_dotProduct_le_dotProduct_abs_uniform

Expectation as a convex combination

MDPLib/Probability/Convexity.lean

ResultLean name
𝔼[X // P] is Mathlib's Finset.centerMass at weights summing to oneFindist.expect_eq_centerMass
minQuark X ≤ 𝔼[X] ≤ maxQuark XFindist.expect_ge_minQuark, Findist.expect_le_maxQuark
Jensen's inequality for an arbitrary convex / concave functionFindist.expect_convexOn_le, Findist.expect_concaveOn_ge

Bridge to Mathlib's standard simplex

MDPLib/Probability/StdSimplex.lean

ResultLean name
A Findist as a point of Convexity.StdSimplex (noncomputable; proof-layer only)Findist.toStdSimplex
Mathlib's indexed convex combination is this library's expectationFindist.toStdSimplex_iConvexComb
Findist.dirac is StdSimplex.single; the bridge is injectiveFindist.toStdSimplex_dirac, Findist.toStdSimplex_injective

Probability: basic properties

MDPLib/Probability/Basic.lean

ResultLean name
ℙ takes values in [0,1]Findist.probability_nonneg, Findist.probability_le_one, Findist.isProb_probability
Linearity, homogeneity and monotonicity of expectationFindist.expect_sum, Findist.expect_smul, Findist.expect_mono
Complement rules ℙ[B] + ℙ[¬B] = 1, and the ≤/> and </≥ pairsFindist.probability_add_probability_not, Findist.probability_le_gt_one, Findist.probability_lt_ge_one
Monotonicity of ℙ[X ≤ t] in both X and t (and the antitone versions)Findist.probability_le_mono, Findist.probability_lt_mono, Findist.probability_ge_anti, Findist.probability_gt_anti
Behaviour of events and probabilities under monotone / strictly monotone / antitone transformations of XFinRV.leq_eq_comp_leq_of_strictMono, StrictMono.probability_le, StrictMono.probability_ge, …
Cash (translation) invariance and negation duality of the comparison eventsFindist.probability_leq_add_const, Findist.probability_leq_eq_neg_geq_neg
CDF cdf P X t = ℙ[X ≤ t]; it is nondecreasing in t and antitone in XFindist.cdf, Findist.cdf_mono, Findist.cdf_anti_of_le
Law of the unconscious statisticianFindist.expect_comp_eq_sum
Tower property (law of total expectation)Findist.expect_expectCondRV
Law of total probabilityFindist.probability_eq_sum
Expectation equals the sum over the (finite) image of XFindist.expect_eq_sum_probability_mul, FinRV.sum_image_univ_eq_sum_fin
Duplicate-free list of the values of a random variable, with index/value inversesFinRV.imageList, FinRV.imageIdxOf, FinRV.getElem_imageIdxOf, FinRV.imageList_nodup
Invariance of probability and expectation under a permutation of the sample spaceFindist.comp, Findist.probability_comp_perm, Findist.expect_comp_perm
A ≤ event can be replaced by a strict < event at a larger thresholdFindist.exists_probability_leq_eq_probability_lt, Findist.exists_probability_leq_eq_probability_lt_of_lt_maxQuark

Quantiles

MDPLib/Probability/Quantile.lean

ResultLean name
Quantile set {q | ℙ[X ≤ q] ≥ α ∧ ℙ[X ≥ q] ≥ 1-α} and its one-sided (lower) relaxationStatistic.quantile, Statistic.quantileLower, Statistic.IsQuantile, Statistic.IsQuantileLower
Equivalent characterizations of membership, including the strict form ℙ[X < q] ≤ αStatistic.mem_quantile_iff, Statistic.mem_quantileLower_iff_probability_lt, Statistic.mem_quantile_of_probability_lt
Every quantile is a lower quantileStatistic.quantile_subset_quantileLower
Reflection: q is an α-quantile of X iff -q is a (1-α)-quantile of -XStatistic.mem_quantile_neg_iff
Quantiles under monotone maps; equivalence for strictly monotone mapsStatistic.mem_quantile_comp_of_monotone, Statistic.mem_quantile_comp_iff_of_strictMono, Statistic.mem_quantileLower_comp_iff_of_strictMono
Lower quantiles of X ≤ Y are cofinal — the basis for monotonicity of VaRStatistic.isCofinalFor_quantileLower_of_le
Cash invariance of the lower-quantile set: QuantileLower(X + c) = QuantileLower(X) + cStatistic.quantileLower_add_const_eq_image
The image f '' quantile(X) is cofinal/coinitial in quantile(f∘X) for monotone f (proof incomplete)Statistic.isCofinalFor_quantile_comp_image_of_monotone, Statistic.isCoinitialFor_quantile_comp_image_of_monotone

Value at Risk

MDPLib/Risk/VaR.lean

ResultLean name
Risk level 0 ≤ α < 1Risk.IsRiskLevel, Risk.RiskLevel
Non-constructive VaR: the greatest lower quantile (equivalently, the greatest quantile)Risk.IsVaR, Risk.IsVaRQuantile
Characterization IsVaR v ↔ ℙ[X < v] ≤ α < ℙ[X ≤ v]Risk.isVaR_iff
Computable VaR VaR[X // P, α] as a max over the finite candidate set, which is nonemptyRisk.finVaR, Risk.finVaRSet, Risk.finVaRSet_nonempty
VaR is monotone: X ≤ Y implies VaR[X] ≤ VaR[Y]Risk.IsVaR.le_of_le
Correctness of the computable VaR: IsVaR P X α (VaR[X // P, α])Risk.isVaR_finVaR
The two definitions (greatest quantile / greatest lower quantile) agreeRisk.isVaRQuantile_iff_isVaR
The quantile set is nonemptyRisk.quantile_nonempty
Translation (cash) invariance for the Risk.IsVaR predicateRisk.IsVaR.add_const
… and for the computable VaR: VaR[X + c] = VaR[X] + cRisk.finVaR_add_const
Strictly monotone transformations for the Risk.IsVaR predicateRisk.IsVaR.comp_of_strictMono
… and for the computable VaR: VaR[f∘X] = f(VaR[X])Risk.finVaR_comp_of_strictMono
Positive homogeneity: VaR[c·X] = c·VaR[X] for c > 0Risk.finVaR_const_mul

Main.lean checks VaR on the distributions in test_var.json using standalone code (computeVaR), not the verified Risk.finVaR.

MDPs and histories

MDPLib/MDP/Histories.lean

ResultLean name
Tabular MDP with finite states, actions, transitions and rewardsMDP
Histories s₀ a₀ s₁ …, their length, last state, prefixes, and the length-indexed subtypeHist, Hist.length, Hist.last, Hist.prefix, MDP.HistOfLength
The count S · (S·A)^t and the explicit index maps Fin (numHist t) ↔ HistOfLength tMDP.numHist, MDP.idxToHist, MDP.histToIdx
… that those maps are mutually inverse, i.e. that the count is the cardinality (proof incomplete)leftInverse_idxToHist_histToIdx, rightInverse_idxToHist_histToIdx, exists_init_of_length_eq_zero, exists_foll_of_length_eq_succ
Embeddings Hist × A × S ↪ Hist and S ↪ HisttupleToHistEmbedding, stateToHistEmbedding
The horizon-t history sets are exactly the histories of length t; Fintype (M.HistOfLength t)mem_historiesHorizon, length_eq_of_mem_historiesHorizon, MDP.historiesHorizonT

The ℋ h t family is defined; its length lemma length_of_mem_histories is still unproven. MDPLib/Risk/CVaR.lean is a stub with notes for CVaR.

Building and testing

lake build MDPLib            # the library
lake -R build MDPLib:docs    # the API documentation
lake build mdplib            # the binary file
lake build MDPLibTest        # computability tests
./test.sh                    # computability + regression tests, interpreted and compiled (Linux)

CI runs the library build, test.sh, the docs and the paper on every pull request.

Lean Resources

Most useful

Others