The Theorems This Library States
These are the declarations written with the theorem keyword, as opposed to lemma. The distinction is the author's own: by the usual convention a theorem is a result worth stating for its own sake, while a lemma is a step towards one. This page takes that convention at face value.
So this list is only as good as the library's discipline about the two keywords. Where a project uses them interchangeably, read this as "all results" rather than as a statement of intent.
10 of 1382 declarations are stated as theorems, ranked within each chapter by how much machinery they rest on.
Against each one is what you have made of it. A declaration is accepted when you have read it and judged that it says what its name claims — and covered when, in addition, every declaration its statement rests on is accepted too. The gap between those two is the point: accepting a theorem whose definitions you have not read accepts a sentence, not a theorem.
Whether something is proved is a separate question. A sorry is flagged below but never blocks acceptance, because accepting is a judgement about what a statement means; Sorries and assumptions reports the rest.
For Mathlib
-
ProbabilityTheory.HasCondDistrib.hasLaw_of_const'Alias of the forward direction of
ProbabilityTheory.hasCondDistrib_const_iff.**Alias** of the forward direction of `ProbabilityTheory.hasCondDistrib_const_iff`. --- Conditioning on a constant is the same as having law `κ b`.
Conditioning on a constant is the same as having law
κ b. -
ProbabilityTheory.HasLaw.hasCondDistrib_constAlias of the reverse direction of
ProbabilityTheory.hasCondDistrib_const_iff.**Alias** of the reverse direction of `ProbabilityTheory.hasCondDistrib_const_iff`. --- Conditioning on a constant is the same as having law `κ b`.
Conditioning on a constant is the same as having law
κ b. -
Finset.measurable_inf'Dual version of
Finset.measurable_sup'.
Online
-
Bandits.TS.integral_regret_leIf Thompson sampling has the correct prior over environments and every environment has
Kactions, each of which has a corresponding reward betweenlanduthat is sub-Gaussian with variance proxyσ2after its mean is subtracted, then the Bayesian regret at timenis at most(2 * K + 1) * (u - l) + 8 * √(σ2 * K * n * Real.log n). -
Bandits.UCB.regret_le_of_gt_two'Regret bound for the UCB algorithm with exploration constant
c > 2 * σ2, forσ2-subgaussian rewards, with an explicit constant. -
Bandits.ETC.regret_leRegret bound for the ETC algorithm.
Sequential Learning
-
Learning.randomSampling.action_tendsto_anyThe minimum distance from sampled actions to any point tends to zero.
-
Learning.IsAlgEnvSeq.identDistrib_trajectoryThe law of the sequence of rounds generated by an algorithm-environment pair is unique: it does not depend on the probability space used.
-
Learning.Environment.ext -
Learning.Algorithm.ext
Verdicts remember what they were about. Each verdict is recorded against the declaration's meaning at the moment you set it — a structural hash of the elaborated term, not of how it prints. So a later build of a revised library can tell you which of your acceptances are of something that has since changed, and it needs neither the old build nor a --baseline to do it: the exported file carries its own reference points. Those acceptances are listed above, and they are excluded from every count on this page rather than quietly inflating it.
What this is not. Nothing here is checked or authenticated. The exported file is plain JSON that anyone can edit, and an accepted declaration is one that a human said says what its name claims — no more. It is a work aid for the reader who made it, and it should never be offered to anyone else as evidence that a library was audited.
Where it is kept. In this browser, under this project's name. Clearing your browser data deletes it, and a second reader on another machine shares none of it — so export the file, which is the artifact that actually travels.