Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 661 to 666 of 2,569 results.
Cslib.MachineLearning.PACLearning.IsPACLearnerFor.mono_ε
Mathematical statement
A PAC learner with accuracy ε₁ is also a PAC learner with any weaker accuracy ε₂ ≥ ε₁: the bad event {error > opt + ε} only shrinks.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.MachineLearning.PACLearning.SetShatters.subset
Mathematical statement
Shattering is anti-monotone in the shattered set: if C shatters W and V ⊆ W, then C shatters V.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.MachineLearning.PACLearning.versionSpace_append
Mathematical statement
The version-space meet law. The version space of an appended sample is the intersection of the version spaces of the two parts: constraints accumulate by intersection.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Probability.PMF.posterior_hasSum
Mathematical statement
Posterior probabilities joint(a, b) / marginal(b) sum to 1 when b is in the support of the marginal.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Probability.PMF.posteriorDist_eq_prior_of_outputIndist
Mathematical statement
If the output distribution of a channel does not depend on the input, then conditioning on any output with positive probability leaves the prior unchanged.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Probability.PMF.uniformOfFintype_map_equiv
Mathematical statement
A uniform distribution on a finite type is invariant under any equivalence.
Source project: Lean Computer Science Library
Person-level attribution pending.