Statistics
The Lean Pool projects whose card's first MSC2020 code is in class 62, Statistics: 2 articles, one per card.
TheoremFinite Čencov-Petz Uniqueness#
Formalizes the finite/discrete Čencov-Petz uniqueness theorem, showing that any continuous metric family on finite probability simplexes that is monotone under Markov morphisms is a scalar multiple of the Fisher information metric.
Quoted from the card LeanPool/projects/cencov-petz.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 5 main results, each with its informal statement quoted from the card. The scan finds 5 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
LeanPool.CencovPetz.MonotoneMetricFamily.eq_smul_fisher_of_continuous(theorem; a main declaration), declared in LeanPool/CencovPetz/CencovFinite.lean, line 46: “Proves that every continuous monotone metric family on a finite probability simplex is a scalar multiple of the Fisher information metric.” Its source, as the card gives it: “N. N. Chentsov, Statistical Decision Rules and Optimal Inference, AMS Translations of Mathematical Monographs 53, 1982.”LeanPool.CencovPetz.MonotoneMetricFamily.eq_smul_fisher_of_isRational(theorem), declared in LeanPool/CencovPetz/CencovSplitPoint.lean, line 225: “Establishes the scalar Fisher-form identity at rational simplex points using split representations.”LeanPool.CencovPetz.MonotoneMetricFamily.eq_smul_fisher_of_isSplitRepresentable(theorem), declared in LeanPool/CencovPetz/CencovSplitPoint.lean, line 48: “Proves the scalar Fisher-form identity for simplex points represented as pushforwards of uniform distributions under splitting maps.”LeanPool.CencovPetz.MonotoneMetricFamily.uniformScalar_eq_uniformScalar_two(theorem), declared in LeanPool/CencovPetz/UniformScalarConstant.lean, line 220: “Shows that the uniform-point scalar is independent of simplex dimension once the dimension is at least two.”LeanPool.CencovPetz.TangentFin.Bilin.B_eq_smul_fisherBilin_uniform(lemma), declared in LeanPool/CencovPetz/UniformScalarMultiple.lean, line 366: “Proves that the permutation-invariant bilinear form at a uniform finite simplex point is a scalar multiple of the Fisher bilinear form.”
Project
- Authors: Adam Benenson.
- Source: Statistical Decision Rules and Optimal Inference by N. N. Chentsov, https://bookstore.ams.org/mmono-53.
- Project repository: abenenson/cencov-petz.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 62B10, 53C21.
- In Lean Pool: LeanPool/CencovPetz, from the card LeanPool/projects/cencov-petz.yaml.
Sources
TheoremRL Theory in Lean#
Develops probability, Markov-chain, and stochastic-matrix infrastructure for reinforcement-learning theory.
Quoted from the card LeanPool/projects/rl-theory-in-lean.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists one main result, with its informal statement quoted from the card. The scan finds its declaration in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
StochasticMatrix.stationary_distribution_exists(theorem; a main declaration), declared in LeanPool/RlTheoryInLean/Data/Matrix/Stochastic.lean, line 669: “Proves existence of a stationary distribution for a stochastic matrix.”
Project
- Authors: Shangtong Zhang.
- Source: arXiv:2511.03618.
- Project repository: ShangtongZhang/rl-theory-in-lean.
- Provenance: mix, which in Lean Pool's terms means people and AI “both contributed substantially” to its Lean proofs.
- License: MIT, under which the project was published; Lean Pool redistributes it under Apache-2.0, keeping its copyright line: “Copyright (c) 2025 Shangtong Zhang”.
- MSC2020: 62L20, 60J10.
- In Lean Pool: LeanPool/RlTheoryInLean, from the card LeanPool/projects/rl-theory-in-lean.yaml.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.