Probability theory and stochastic processes
The Lean Pool projects whose card's first MSC2020 code is in class 60, Probability theory and stochastic processes: 15 articles, one per card.
LemmaAumann's Agreement Theorem#
Formalizes Aumann's agreement theorem for information partitions and a common-prior setting, together with a p-belief variant bounding posterior disagreement by 2 * (1 - p).
Quoted from the card LeanPool/projects/agree-to-disagree.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 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.
AgreeToDisagree.agreeToDisagree(lemma; a main declaration), declared in LeanPool/AgreeToDisagree/AgreeToDisagree.lean, line 226: “If it is common knowledge at a state that two agents assign fixed posterior probabilities to an event, and the common-knowledge cell has equal posterior under their priors, then the two posterior probabilities are equal.”AgreeToDisagree.agreeToDisagree'(lemma), declared in LeanPool/AgreeToDisagree/AgreeToDisagree.lean, line 240: “Generalizes the agreement theorem to a family of agents indexed by an arbitrary type.”AgreeToDisagree.agreeToDisagree_beliefs(lemma; a main declaration), declared in LeanPool/AgreeToDisagree/AgreeToDisagreeBeliefs.lean, line 308: “Proves that common p-belief of fixed posteriors bounds the difference between any two agents' real-valued posteriors by 2 * (1 - p).”
Project
- Authors: Ruiz Chen, Ben Eltschig, Ken Ono, Jujian Zhang.
- Source: We Can't Agree to Disagree, Formally: Aumann's Theorem and Assumption Accounting in Lean, https://papers.ssrn.com/sol3/papers.cfm?abstract_id=6837298.
- Project repository: AxiomMath/AgreeToDisagree.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: MIT, under which the project was published; Lean Pool redistributes it under Apache-2.0.
- MSC2020: 60A10, 91A40.
- In Lean Pool: LeanPool/AgreeToDisagree, from the card LeanPool/projects/agree-to-disagree.yaml.
Sources
TheoremBennett--Bernstein, Freedman, and Hoeffding concentration inequalities#
Develops variance-sensitive sub-gamma moment-generating-function estimates, Bennett and Bernstein bounds, a Freedman--Bernstein upper tail for finite adapted sums, conditional and independent-variable Hoeffding inequalities.
Quoted from the card LeanPool/projects/concentration-inequalities.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 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.
Contrib.Bennett.hasSubgammaMGF_of_bounded_above(theorem), declared in LeanPool/ConcentrationInequalities/BennettBernstein.lean, line 485: “A centered real random variable bounded above by a positive constant, with bounded second moment, satisfies a Bennett--Bernstein sub-gamma moment-generating-function estimate.”Contrib.Freedman.subgamma_bernstein_tail(theorem; a main declaration), declared in LeanPool/ConcentrationInequalities/FreedmanBernstein.lean, line 352: “A finite adapted sum of conditionally sub-gamma increments satisfies the corresponding variance-sensitive Freedman--Bernstein upper-tail bound.”Contrib.ConditionalHoeffding.hasCondSubgaussianMGF_of_mem_Icc(theorem), declared in LeanPool/ConcentrationInequalities/ConditionalHoeffding.lean, line 41: “A bounded random variable with zero conditional expectation satisfies a conditional Hoeffding sub-Gaussian moment-generating-function estimate.”Contrib.Hoeffding.hoeffding_upper(theorem), declared in LeanPool/ConcentrationInequalities/HoeffdingUpper.lean, line 63: “A sum of finitely many independent random variables valued in the unit interval exceeds its mean by t with probability at most exp(-2 t squared divided by the number of terms).”
Project
- Authors: Juan Pablo Traverso Gianini, Aristotle.
- Source: Reusable concentration-inequality components accompanying Linear-Error Clique Partitions of Split Graphs via Structured Triangle Packing by Juan Pablo Traverso Gianini, https://github.com/jtraverso/erdos-81-chordal-clique-partitions/blob/b3423f3e8c8db7c2d1b279673293ef3079faf903/preprints/PAPER_III/05_formalization/lean_v1.4_freeze/Contrib/FreedmanBernstein.lean.
- Project repository: jtraverso/erdos-81-chordal-clique-partitions.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 60E15, 60G42.
- In Lean Pool: LeanPool/ConcentrationInequalities, from the card LeanPool/projects/concentration-inequalities.yaml.
Sources
TheoremBurkholder Martingale Transform Inequality#
Formalizes Burkholder's sharp Lp inequality for real-valued martingale transforms: if
fis a discrete martingale andwa predictable multiplier bounded by1, then the Lp norm of the transformw ⋆ₘ fis at most(pStar p - 1)times the Lp norm off, wherepStar pis the maximum ofpand its conjugate exponent. The proof builds the Burkholder special function as a majorant of the relevant payoff in each exponent regime (1 < p < 2,p = 2,p > 2).
Quoted from the card LeanPool/projects/burkholder.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 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.
MeasureTheory.Lp_Burkholder_inequality_martingaleTransform(theorem; a main declaration), declared in LeanPool/Burkholder/MartingaleTransforms.lean, line 1382: “The sharp Lp Burkholder inequality: for a discrete martingalefand a predictable multiplierwwith|w n| ≤ 1, the Lp norm of the martingale transform(w ⋆ₘ f) nis bounded by(pStar p - 1)times the Lp norm off n.”MeasureTheory.martingaleTransform_martingale(theorem), declared in LeanPool/Burkholder/MartingaleTransforms.lean, line 210: “The martingale transform of a martingale by a strongly predictable bounded multiplier is itself a martingale.”Majorants.exists_majorant_p_g_1(theorem), declared in LeanPool/Burkholder/Majorants.lean, line 47: “For every exponentp > 1there exists a Burkholder majorant, the special function dominating the payoff and driving the inequality.”
Project
- Authors: Daniel Smania.
- Source: Boundary value problems and sharp inequalities for martingale transforms by Donald L. Burkholder, doi:10.1214/aop/1176993220.
- Project repository: SmaniaD/Burkholder.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 60G42.
- In Lean Pool: LeanPool/Burkholder, from the card LeanPool/projects/burkholder.yaml.
Sources
TheoremThe Cramer-Wold theorem#
Formalizes the finite-dimensional Cramer-Wold theorem for measures on Euclidean spaces, with Banach-space continuous-dual generalizations, Hilbert-space inner-product versions, and random-variable law corollaries for identical distributions and
HasLaw.
Quoted from the card LeanPool/projects/cramer-wold.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 6 main results, each with its informal statement quoted from the card. The scan finds 6 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.CramerWold.euclideanSpace_measure_eq_of_forall_inner_map_eq(theorem; a main declaration), declared in LeanPool/CramerWold.lean, line 153: “Proves the classical finite-dimensional Cramer-Wold theorem for finite Borel measures onEuclideanSpace ℝ (Fin n), showing equality when all scalar projections have equal pushforward measures.”LeanPool.CramerWold.measure_eq_of_forall_dual_map_eq(theorem), declared in LeanPool/CramerWold.lean, line 51: “Generalizes the extensionality criterion to finite Borel measures on complete second-countable real normed spaces, using all continuous-linear real projections.”LeanPool.CramerWold.measure_eq_of_forall_inner_map_eq(theorem), declared in LeanPool/CramerWold.lean, line 102: “Specializes Cramer-Wold extensionality to real Hilbert spaces, using scalar projections of the formx ↦ ⟪t, x⟫_ℝ.”LeanPool.CramerWold.identDistrib_of_forall_dual_comp_identDistrib(theorem), declared in LeanPool/CramerWold.lean, line 209: “Proves that two finite-measure random variables are identically distributed when every continuous-linear real projection of them is identically distributed.”LeanPool.CramerWold.identDistrib_of_forall_inner_comp_identDistrib(theorem), declared in LeanPool/CramerWold.lean, line 262: “Gives the Hilbert-space random-variable version using all scalar inner-product projections.”LeanPool.CramerWold.hasLaw_of_forall_dual_comp_hasLaw(theorem), declared in LeanPool/CramerWold.lean, line 314: “Proves that a random variable has a target law when every continuous-linear real projection has the corresponding projected target law.”
Project
- Authors: Lazar Milikic.
- Source: Some theorems on distribution functions by Harald Cramer, Herman Wold, doi:10.1112/jlms/s1-11.4.290.
- Project repository: Lemmy00/lean-pool.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 60B11, 60E10, 28A33.
- In Lean Pool: LeanPool/CramerWold, from the card LeanPool/projects/cramer-wold.yaml.
Sources
TheoremFeige's sharp unit-slack inequality#
For small-universe probability spaces, proves the sharp fixed-dimensional unit-slack lower bound for sums of independent nonnegative random variables: if each coordinate has mean at most one, then the probability that the sum lies below its mean plus one is at least (n/(n+1))^n, and this constant is optimal. The supporting library formalizes the Vlassis--Thomas exact distribution-free calibration theorem, Grünbaum's centroid-halfspace inequality and sharp simplex example, and the normalized-exponential bridge joining them.
Quoted from the card LeanPool/projects/feige.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 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.
Feige.sharp_unit_slack_feige_complete(theorem; a main declaration), declared in LeanPool/Feige/MainTheorem.lean, line 26: “For every positive dimension n and every small-universe probability space, the sharp fixed-dimensional lower bound for the strict event that a sum of independent nonnegative random variables is below its expectation plus one is (n/(n+1))^n, and an explicit finite family proves optimality.”VlassisThomas.exactCalibration(theorem), declared in LeanPool/Feige/VlassisThomas/Main.lean, line 30: “On every small-universe probability space, the Dirichlet statistic used in the proof is super-uniform for every independent family of measurable, integrable, nonnegative random variables whose coordinate means are at most one.”Grunbaum.grunbaum_centroid_halfspace(theorem), declared in LeanPool/Feige/Grunbaum/Main.lean, line 187: “Every closed halfspace containing the centroid of a positive-volume convex body in finite-dimensional Euclidean space contains at least the sharp Grünbaum fraction of the body's volume.”
Project
- Authors: Zhengqing Zhou.
- Source: Sharp Small-Deviation Inequalities for Sums of Independent Nonnegative Random Variables by Weibo Fu, Yanjun Han, Guanyang Wang, Jun Yan, Peng Zhang, Zhengqing Zhou, arXiv:2607.23980.
- Project repository: pengzhang91/Feige, at commit 98ab466e.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 60E15, 52A20.
- In Lean Pool: LeanPool/Feige, from the card LeanPool/projects/feige.yaml.
Sources
TheoremGaussian Moments Conjecture counterexamples#
Proves explicit complex polynomial counterexamples to the Gaussian Moments Conjecture in every dimension at least three, using genuine expectations under finite products of standard real Gaussian measures. Retains reusable polynomial integrability, Stein identities, complex contractions, coefficient formulas, injective-coordinate marginals, and related moment results.
Quoted from the card LeanPool/projects/gaussian-moments-counterexamples.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 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.
GaussianMomentsCounterexamples.not_GMC_of_three_le(theorem; a main declaration), declared in LeanPool/GaussianMomentsCounterexamples/Counterexamples.lean, line 93: “For every n at least three, the Gaussian Moments Conjecture fails: some complex polynomial has all positive pure Gaussian moments zero, while a polynomial multiplier prevents eventual mixed-moment vanishing.”GaussianMomentsCounterexamples.master_three(theorem), declared in LeanPool/GaussianMomentsCounterexamples/Counterexamples.lean, line 32: “For every complex univariate polynomial A and positive m, the expectation of A(Q3) times P3 to power m equals m! times the degree-m coefficient of A(X) times (1+X) to power m-1. The explicit P3 has degree four and five terms in its natural complex coordinates.”GaussianMomentsCounterexamples.master_four(theorem), declared in LeanPool/GaussianMomentsCounterexamples/Counterexamples.lean, line 40: “The analogous arbitrary-A coefficient identity for the explicit four-variable polynomial P4, of degree three and six terms in its natural complex coordinates, gives an independent counterexample.”
Project
- Authors: Christopher D. Long.
- Source: arXiv:2607.18186.
- The card's note on its source: “Imports the completed Gaussian core and related moment infrastructure. The July manuscript predates the September Lean proof release. Five and six term counts refer to the natural complex coordinates; total degrees four and three also hold in the original real coordinates. The separate Jacobian-map and route-arithmetic files are excluded. No general inversion, Jacobian-reduction route, or resolution of the two-dimensional conjecture is claimed. Upstream MIT notice is retained in the project entry module. Upstream Lean authorship is inferred from the public codex/lean-formalization branch; its exact proof-authoring model and extent of human editing are unreported. This port and optimization are Codex-authored.”
- Project repository: long-mathematics/gaussian-moments-counterexamples, at commit c31bb63a.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: MIT, under which the project was published; Lean Pool redistributes it under Apache-2.0.
- MSC2020: 60E05, 13F20.
- In Lean Pool: LeanPool/GaussianMomentsCounterexamples, from the card LeanPool/projects/gaussian-moments-counterexamples.yaml.
Sources
TheoremThe Hanson-Wright inequality for sub-Gaussian quadratic forms#
Proves the finite-dimensional Hanson-Wright concentration inequality for quadratic forms of independent mean-zero sub-Gaussian real random variables whose maximum least global-MGF sub-Gaussian scale is positive, for matrices with positive Frobenius and operator norms. The bound uses the fixed universal coefficient 1 / (256 * exp(1)^2). This is the MGF normalization of the usual result; no formal identification with an Orlicz psi-2 norm is claimed. The development derives the required moment-generating-function certificate instead of assuming it, and contributes reusable scalar Bernstein, Chernoff, cumulant, sub-Gaussian-process, and finite-maximum infrastructure.
Quoted from the card LeanPool/projects/hanson-wright.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 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.HansonWright.hanson_wright_inequality_hdp(theorem; a main declaration), declared in LeanPool/HansonWright/Probability/Concentration/HansonWright.lean, line 3923: “For independent mean-zero real random variables with finite least global-MGF sub-Gaussian scales and positive maximum coordinate MGF scale, and a matrix with positive Frobenius and operator norms, the centered quadratic form satisfies the Hanson-Wright two-regime exponential tail bound with the fixed universal coefficient 1 / (256 * exp(1)^2).”LeanPool.HansonWright.hasHansonWrightMGF_of_subgaussian(theorem), declared in LeanPool/HansonWright/Probability/Concentration/HansonWright.lean, line 3669: “Given positive K and operator norm and C at least 64 * exp(1)^2, independent coordinates with global-MGF sub-Gaussian parameter K^2 satisfy the local quadratic cumulant-generating-function estimate needed for Hanson-Wright.”LeanPool.bernstein_inequality(theorem), declared in LeanPool/HansonWright/Probability/Concentration/Bernstein.lean, line 581: “A finite family of independent, centered, uniformly bounded real random variables satisfies the classical scalar Bernstein tail inequality.”
Project
- Authors: Yuanhe Zhang, Jason D. Lee, Fanghui Liu.
- Source: High-Dimensional Probability (second edition) by Roman Vershynin, doi:10.1017/9781009490672, https://www.math.uci.edu/~rvershyn/papers/HDP-book/HDP-book.html.
- Project repository: Lean-MoDS/StatsMLlib, at commit 37286c3d.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: Apache-2.0.
- MSC2020: 60E15, 60B20, 62H12.
- In Lean Pool: LeanPool/HansonWright, from the card LeanPool/projects/hanson-wright.yaml.
Sources
TheoremInflation termination for classical pair-source networks#
For finite binary pair-source networks without isolated vertices, classifies when the inflation hierarchy characterizes compatibility with finite latent alphabets: precisely forests of double stars, where order two suffices. Also proves triangle nontermination for arbitrary measurable latent probability spaces, quantitative obstructions, finite and measurable Finner inequalities, and graph witnesses.
Quoted from the card LeanPool/projects/inflation-termination.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 2 main results, each with its informal statement quoted from the card. The scan finds 2 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.
TriangleInflation.Graph.classification_NW(theorem; a main declaration), declared in LeanPool/InflationTermination/PalomarSolutions/TriangleInflationClassification.lean, line 45: “For finite binary pair-source graphs without isolated vertices, some finite order of the Navascués–Wolfe hierarchy characterizes compatibility with finite latent alphabets exactly for double-star forests; order two suffices there.”TriangleInflation.no_finite_characterizing_orderM(theorem), declared in LeanPool/InflationTermination/TriangleInflation/FinnerMeasure.lean, line 635: “At every positive inflation order, a triangle law passes both the AI and NW tests but has no compatible model over any measurable latent probability spaces.”
Project
- Authors: William Blair.
- Project repository: williamjblair/inflation-termination, at commit 2aa1f05c.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: MIT, under which the project was published; Lean Pool redistributes it under Apache-2.0.
- MSC2020: 60A05, 05C05.
- In Lean Pool: LeanPool/InflationTermination, from the card LeanPool/projects/inflation-termination.yaml.
Sources
TheoremMalliavin calculus and the Clark–Ocone representation#
Constructs the Malliavin derivative, Gaussian integration by parts, closability, Wiener chaos, Brownian Itô integration and martingale representation. The Clark–Ocone endpoint uses a generating pre-Brownian process with continuous linear coordinates on a separable real Gaussian Banach space, its natural filtration, and pairs in the closed Malliavin graph; the conditional-expectation sections agree almost everywhere at positive times.
Quoted from the card LeanPool/projects/lean-malliavin.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.
PalomarClarkOcone.generated_clark_ocone(theorem; a main declaration), declared in LeanPool/Malliavin/ClarkOconeSolution.lean, line 317: “For a generating pre-Brownian process on a separable real Gaussian Banach space whose coordinates are pointwise represented by continuous linear functionals, constructs a time realization of the Malliavin derivative and an Itô isometry for the natural filtration, with martingale representation for every terminal L² variable. For pairs in the closed Malliavin graph, the Clark–Ocone formula identifies the derivative's predictable projection with its conditional-expectation sections for almost every positive time.”
Project
- Authors: Ezzeri Esa.
- Project repository: savarin/lean-malliavin, at commit a1a6ccc6.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 60H07, 60H05.
- In Lean Pool: LeanPool/Malliavin, from the card LeanPool/projects/lean-malliavin.yaml.
Sources
TheoremMarkovProcess#
A Lean formalization of continuous-path Markov processes associated with conservative Feller transition semigroups on nonempty locally compact Polish spaces. A uniform Kolmogorov displacement-moment bound yields a unique measurable kernel from each starting point to continuous-path space, with the prescribed finite-dimensional distributions. The library also develops strong Markov properties, generators and resolvents, stopping and killing, and Brownian motion as an example.
Quoted from the card LeanPool/projects/markovprocess.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.
MarkovProcess.existsUnique_continuousProcess(theorem; a main declaration), declared in LeanPool/MarkovProcess/MarkovProcess/Main.lean, line 410: “A conservative Feller transition semigroup on a nonempty locally compact Polish space satisfying the Kolmogorov moment criterion determines a unique continuous-path Markov kernel with its prescribed finite-dimensional distributions.”
Project
- Authors: Scott Armstrong.
- Project repository: scottnarmstrong/markovprocess, at commit dbade0d1.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 60J25, 60J35, 60G17.
- In Lean Pool: LeanPool/MarkovProcess, from the card LeanPool/projects/markovprocess.yaml.
Sources
TheoremOptimal fully dynamic matching on the line#
Constructs a measurable hierarchical policy for fully dynamic matching of uniformly arriving demand and replenishment on the unit interval. Proves logarithmic-over-inventory bounds for long-run root-mean-square distance from every initial inventory and for initialized finite-horizon expected average cost.
Quoted from the card LeanPool/projects/fd1d-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.
FD1D.V5.Palomar.optimalDynamicMatchingUpperBound(theorem; a main declaration), declared in LeanPool/FullyDynamicMatching/FD1D/V5/PaperStatements.lean, line 136: “For every inventory size m at least two, an online policy has long-run RMS cost at most (72000/log 2) log(m+1)/m from every initial inventory, and the same expected-average-cost bound after initialization for horizons at least 2m².”
Project
- Authors: Yash Kanoria.
- Project repository: ykanoria/fd1d-lean, at commit 26a5b4e2.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 60J20, 90B15.
- In Lean Pool: LeanPool/FullyDynamicMatching, from the card LeanPool/projects/fd1d-lean.yaml.
Sources
ClassQuasi-Borel Spaces#
Formalizes quasi-Borel spaces and quasi-Borel pre-domains, a category for higher-order probability theory.
Quoted from the card LeanPool/projects/quasi-borel-spaces.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 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.
QuasiBorelSpace(class; a main declaration), declared in LeanPool/QuasiBorelSpaces/Defs.lean, line 31: “Defines a quasi-Borel space as a type with a set of random variables closed under constants, measurable precomposition, and gluing.”QuasiBorelSpace.IsHom(inductive), declared in LeanPool/QuasiBorelSpaces/Defs.lean, line 64: “Defines morphisms of quasi-Borel spaces as maps that preserve random variables under precomposition.”OmegaQuasiBorelSpace(class; a main declaration), declared in LeanPool/QuasiBorelSpaces/OmegaQuasiBorelSpace.lean, line 45: “Combines the quasi-Borel and ω-complete partial order structures with the compatibility axiom of Vakar-Kammar-Staton.”QuasiBorelSpace.ProbabilityMeasure(structure; a main declaration), declared in LeanPool/QuasiBorelSpaces/ProbabilityMeasure.lean, line 39: “Defines the probability-measure monad on quasi-Borel spaces by quotienting pre-probability measures by integral equivalence.”
Project
- Authors: Anthony Vandikas, Kiarash Sotoudeh.
- Source: doi:10.1109/LICS.2017.8005137, arXiv:1701.02547.
- Project repository: YellPika/quasi-borel-spaces.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: MIT, under which the project was published; Lean Pool redistributes it under Apache-2.0, keeping its copyright line: “Copyright (c) 2025 Anthony Vandikas, Kiarash Sotoudeh”.
- MSC2020: 60A05, 18C50, 68Q55.
- In Lean Pool: LeanPool/QuasiBorelSpaces, from the card LeanPool/projects/quasi-borel-spaces.yaml.
Sources
TheoremRare subtree patterns in conditioned Bienaymé trees#
Proves marked Poisson approximation, root declumping, maximal complete non-fringe r-ary height and maximum leaf-height for critical Bienaymé trees conditioned on their size, under the stated stable-domain, marking, cutoff and non-clustering hypotheses. Periodic offspring laws are included through admissible-size limits. Single-point phase refinements are formulated along phase-separated admissible subsequences. The dependency closure preserves tree coding, Chen–Stein bounds, regular variation, stable densities and lattice local limit estimates, with concrete offspring examples and direct consequences.
Quoted from the card LeanPool/projects/rare-subtree-patterns.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 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.
PoissonDeclumping.poissonApproximation(theorem; a main declaration), declared in LeanPool/RareSubtreePatterns/MainTheorems.lean, line 44: “Under the critical stable-domain assumption, microscopicity and non-clustering with a common sublinear divergent cutoff give Poisson approximation for bounded expected marked counts, and a law of large numbers when the expected count diverges, along admissible tree sizes.”PoissonDeclumping.poissonApproximation2(theorem; a main declaration), declared in LeanPool/RareSubtreePatterns/MainTheorems.lean, line 48: “For a root-degree set B with positive finite weight c_B, structural microscopicity of the original marks and non-clustering of the root-declumped marks yield Poisson approximation with the c_B-adjusted parameter when expected counts are bounded, and divergence in probability when they grow, along admissible tree sizes.”PoissonDeclumping.maxString(theorem; a main declaration), declared in LeanPool/RareSubtreePatterns/MainTheorems.lean, line 52: “For critical offspring laws in a stable domain, the maximum non-fringe complete r-ary height has a lattice-Gumbel law for unary strings and two-point localization for r at least two, with the stated offspring probabilities and single-point refinements along phase-separated admissible subsequences.”PoissonDeclumping.maxLeafHeight(theorem; a main declaration), declared in LeanPool/RareSubtreePatterns/MainTheorems.lean, line 56: “The maximum leaf-height has the stated lattice-Gumbel behavior when the unary offspring probability is positive, and the two-point behavior when it is zero, with single-point refinements along phase-separated admissible subsequences and the stated nondegeneracy and stable-domain conditions.”
Project
- Authors: Igor Kortchemski.
- Source: arXiv:2607.22291v1.
- Project repository: igor-kortchemski/rare-subtree-patterns, at commit fc5ef722.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 60J80, 60G50, 05C05, 05C80.
- In Lean Pool: LeanPool/RareSubtreePatterns, from the card LeanPool/projects/rare-subtree-patterns.yaml.
Sources
TheoremSuperdiffusion and anomalous regularization in self-similar random flows#
Proves quenched displacement-moment estimates, quantitative generator renormalization and anomalous large-scale elliptic regularity for random incompressible flows satisfying the ABK shell-law assumptions. The shell carrier has continuous second derivatives, a stronger qualitative regularity assumption than the paper's local C^{1,1} assumption. The model hypotheses are explicit; the Gaussian example is not constructed. Preserves the production dependency closure, including sensitivity, diffusivity recursion, concentration and divergence-form process theory. Reuses the pooled homogenization and Markov-process libraries. A public companion theorem proves finiteness of the first and second displacement observables used in the superdiffusivity statement. Additional proofs establish measurable dependence of the transition law and quenched displacement expectations on the environment.
Quoted from the card LeanPool/projects/superdiffusion.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 6 main results, each with its informal statement quoted from the card. The scan finds 6 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.
Algsuperdiff.superdiffusivity_with_finite_moments(theorem; a main declaration), declared in LeanPool/Superdiffusion/Algsuperdiff/SuperdiffusivityFiniteMoments.lean, line 30: “For dimensions at least two, one positive small-coupling threshold simultaneously gives the full quantitative superdiffusivity bounds and almost-sure integrability of both displacement observables at every positive time.”Algsuperdiff.superdiffusivity(theorem), declared in LeanPool/Superdiffusion/Algsuperdiff/MainTheorems.lean, line 104: “For each dimension and positive nondegeneracy constant, sufficiently small coupling gives annealed moment bounds for the quenched second displacement moment about the intrinsic superdiffusive scale and for the squared quenched mean displacement, uniformly at all positive times and throughout the stated coupling-dependent moment range.”Algsuperdiff.generator_renormalization(theorem), declared in LeanPool/Superdiffusion/Algsuperdiff/MainTheorems.lean, line 156: “At every triadic scale, the effective diffusivity tracks the predicted superdiffusive profile. One measurable random error with quantitative moment bounds controls both the essential uniform difference and the energy difference between random and homogenized Dirichlet solutions for all admissible forcing and boundary data.”Algsuperdiff.anomalous_regularity(theorem), declared in LeanPool/Superdiffusion/Algsuperdiff/MainTheorems.lean, line 235: “At every scale and admissible Hölder exponent, a random minimal scale with an exponential tail yields large-scale excess-decay estimates for Dirichlet solutions, uniformly in molecular diffusivity, with the boundary-data term absent in the interior subcube.”Algsuperdiff.Section5.Provider.exists_ae_integrable_streamProcess_displacement(theorem), declared in LeanPool/Superdiffusion/Algsuperdiff/Section5/Provider/DisplacementIntegrability.lean, line 64: “For dimensions at least two and sufficiently small coupling, at every positive time the first and second displacement observables of the constructed process are integrable for almost every environment.”Algsuperdiff.Section5.Measurability.measurable_streamProcess_displacement_expectations(theorem), declared in LeanPool/Superdiffusion/Algsuperdiff/Section5/Measurability/DisplacementExpectations.lean, line 115: “The first and second quenched displacement expectations of the constructed process are measurable functions of the environment.”
Project
- Authors: Scott Armstrong, Tuomo Kuusi.
- Source: arXiv:2601.22142.
- Project repository: scottnarmstrong/Superdiffusion, at commit 7f204763.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 60K37, 35B27, 60J60.
- In Lean Pool: LeanPool/Superdiffusion, from the card LeanPool/projects/superdiffusion.yaml.
Sources
LemmaWigner Semicircle Distribution#
Defines the real Wigner semicircle distribution, its normalized density, affine transformations, and finite-moment integrability.
Quoted from the card LeanPool/projects/semicirclelaw.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 7 main results, each with its informal statement quoted from the card. The scan finds 7 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.SemicircleLaw.semicirclePDFReal(def), declared in LeanPool/SemicircleLaw/SemicircleDistribution.lean, line 55: “Defines the real-valued density of the semicircle distribution with mean μ and variance v.”LeanPool.SemicircleLaw.semicirclePDF(def), declared in LeanPool/SemicircleLaw/SemicircleDistribution.lean, line 212: “Defines the ℝ≥0∞-valued density of the semicircle distribution.”LeanPool.SemicircleLaw.integral_semicirclePDFReal_eq_one(lemma; a main declaration), declared in LeanPool/SemicircleLaw/SemicircleDistribution.lean, line 181: “Proves that the real-valued semicircle density integrates to one for nonzero variance.”LeanPool.SemicircleLaw.semicircleReal(def), declared in LeanPool/SemicircleLaw/SemicircleDistribution.lean, line 245: “Defines the semicircle measure on ℝ, equal to a Dirac mass when the variance is zero.”LeanPool.SemicircleLaw.semicircleReal_map_add_const(lemma), declared in LeanPool/SemicircleLaw/SemicircleDistribution.lean, line 393: “Shows that translating a semicircle measure translates its mean parameter.”LeanPool.SemicircleLaw.semicircleReal_map_const_mul(lemma), declared in LeanPool/SemicircleLaw/SemicircleDistribution.lean, line 413: “Shows that scaling by a nonzero constant scales the mean and variance parameters.”LeanPool.SemicircleLaw.memLp_id_semicircleReal(lemma), declared in LeanPool/SemicircleLaw/SemicircleDistribution.lean, line 548: “Shows that the identity has all finite Lp moments under a semicircle distribution.”
Project
- Authors: FredRaj3.
- Source: https://www.math.ucsd.edu/~tkemp/247A.Notes.pdf.
- Project repository: FredRaj3/SemicircleLaw.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: MIT, under which the project was published; Lean Pool redistributes it under Apache-2.0, keeping its copyright line: “Copyright (c) 2025 FredRaj3”.
- MSC2020: 60B20, 60E05.
- In Lean Pool: LeanPool/SemicircleLaw, from the card LeanPool/projects/semicirclelaw.yaml.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.