Source-pinned research

Research proof index

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 136 research declarations. Search 10,000 more complete Mathlib declarations.

All topics

136 results

Clear filters
Project-declaredLean 4.33.0-rc1

Error map eq hypothesis Error

Cslib.MachineLearning.PACLearning.error_map_eq_hypothesisError

Plain-language statement

Under a realizable distribution P.map (x ↦ (x, c(x))), the general 0-1 error coincides with the binary hypothesisError P h c, where h and c are viewed as subsets of α via the characteristic function decide (· ∈ ·).

computer sciencecomputabilityprogram semantics

Source project: Lean Computer Science Library

Person-level attribution pending.

View proof record
Project-declaredLean 4.33.0-rc1

Is PACLearner For antitone C

Cslib.MachineLearning.PACLearning.IsPACLearnerFor.antitone_C

Plain-language statement

The deterministic PAC learner predicate is antitone in the concept class: a learner for a larger class C' is also a learner for any subclass C ⊆ C', since the agnostic benchmark optimalError _ C ≥ optimalError _ C' makes the error requirement easier.

computer sciencecomputabilityprogram semantics

Source project: Lean Computer Science Library

Person-level attribution pending.

View proof record
Project-declaredLean 4.33.0-rc1

Is PACLearner For mono ε

Cslib.MachineLearning.PACLearning.IsPACLearnerFor.mono_ε

Plain-language statement

A PAC learner with accuracy ε₁ is also a PAC learner with any weaker accuracy ε₂ ≥ ε₁: the bad event {error > opt + ε} only shrinks.

computer sciencecomputabilityprogram semantics

Source project: Lean Computer Science Library

Person-level attribution pending.

View proof record
Project-declaredLean 4.33.0-rc1

Set Shatters subset

Cslib.MachineLearning.PACLearning.SetShatters.subset

Plain-language statement

Shattering is anti-monotone in the shattered set: if C shatters W and V ⊆ W, then C shatters V.

computer sciencecomputabilityprogram semantics

Source project: Lean Computer Science Library

Person-level attribution pending.

View proof record
Project-declaredLean 4.33.0-rc1

Version Space append

Cslib.MachineLearning.PACLearning.versionSpace_append

Plain-language 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.

computer sciencecomputabilityprogram semantics

Source project: Lean Computer Science Library

Person-level attribution pending.

View proof record
Project-declaredLean 4.33.0-rc1

Posterior has Sum

Cslib.Probability.PMF.posterior_hasSum

Plain-language statement

Posterior probabilities joint(a, b) / marginal(b) sum to 1 when b is in the support of the marginal.

computer sciencecomputabilityprogram semantics

Source project: Lean Computer Science Library

Person-level attribution pending.

View proof record