Universal learnable → PAC learnable. Proof sketch: UniversalLearnable gives learner L with rate → 0 and Pr[error ≤ rate(m)] ≥ 2/3. Two components: 1. Event containment: rate(m) < ε ⟹ {error ≤ rate(m)} ⊆ {error ≤ ε} (monotonicity). 2. Confidence boosting: 2/3 → 1-δ via median-of-means (Γ₆₇, sorry'd in boost_two_thirds_to_pac). Routes through boost_two_thirds_to_pac which encapsulates the Chernoff-based boosting.
∀ (X : Type u) [inst : MeasurableSpace X] (C : ConceptClass X Bool) [MeasurableHypotheses X C], (∀ (L : BatchLearner X Bool), LearnEvalMeasurable L) → UniversalLearnable X C → PACLearnable X C
- Decluniversal_imp_pacDeclaration kindtheorem
∀ (X : Type u) [inst : MeasurableSpace X] (C : ConceptClass X Bool) [MeasurableHypotheses X C], (∀ (L : BatchLearner X Bool), LearnEvalMeasurable L) → UniversalLearnable X C → PACLearnable X C
- Declboost_two_thirds_to_pacDeclaration kindtheorem
Boosting lemma: given a learner with success probability ≥ 2/3 under D^m, construct a boosted learner with success probability ≥ 1-δ for any δ > 0. Standard technique: run L independently k times on independent samples of size m₀, take majority vote.
Construction:
- kmin = ⌈9/δ⌉ + 2 (enough blocks for Chebyshev concentration)
- m₀ from hrate(ε/kmin) so that rate(m₀) < ε/kmin
- n = max m₀ (kmin - 1). Then k = n + 1 ≥ kmin.
- Total samples: (n + 1) * n, with Nat.sqrt((n+1)*n) = n.
- At sample size m = (n+1)*n, L' recovers k = n+1 blocks of size n.
- Event containment: when > k/2 blocks have D-error ≤ rate(n) < ε/kmin, majority D-error ≤ k · rate(n) < k/kmin · ε ≤ ε via union bound.
Γ₆₇: sorry — the full measure-theoretic proof requires: (a) block_extract : (Fin (kn) → X) → Fin k → (Fin n → X) (b) iIndepFun for block extractions under product measure D^(kn) (c) chebyshev_majority_bound for i.i.d. Bernoulli(≥2/3) events (d) block extraction marginal = D^n (e) majority vote D-error analysis via union bound
None of this infrastructure currently exists in the codebase. The sorry is A4-compliant (the conclusion PACLearnable X C is non-trivially-true: it requires genuine concentration + majority analysis) and A5-compliant (the proof strategy is structurally complete, only infrastructure is missing).
∀ (X : Type u) [inst : MeasurableSpace X] (C : ConceptClass X Bool) [MeasurableHypotheses X C] (L : BatchLearner X Bool) [MeasurableBatchLearner X L] (rate : ℕ → ℝ), (∀ ε > 0, ∃ m₀, ∀ m ≥ m₀, rate m < ε) → (∀ (D : MeasureTheory.Measure X), MeasureTheory.IsProbabilityMeasure D → ∀ c ∈ C, ∀ (m : ℕ), (MeasureTheory.Measure.pi fun x => D) {xs | D {x | L.learn (fun i => (xs i, c (xs i))) x ≠ c x} ≤ ENNReal.ofReal (rate m)} ≥ ENNReal.ofReal (2 / 3)) → PACLearnable X CBatchLearnerBatchLearner.learnConceptClassFLT.ConceptLearnEvalMeasurableMeasurableBatchLearnerMeasurableHypothesesPACLearnableblock_extractboosted_majoritygoodBlockEventUses
Used by
- DecliIndepSet_goodBlockEventsDeclaration kindtheorem
T5: The goodBlockEvents are independent under the product measure.
∀ {X : Type u} [inst : MeasurableSpace X] (L : BatchLearner X Bool) [MeasurableBatchLearner X L] (D : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure D] (c : Concept X Bool), Measurable c → ∀ (rate : ℕ → ℝ) (k n : ℕ), ProbabilityTheory.iIndepSet (goodBlockEvent✝ L D c rate k n) (MeasureTheory.Measure.pi fun x => D)Used by
- DecliIndepFun_block_extractDeclaration kindtheorem
Block extractions are independent under the product measure. Key infrastructure for boosting (D4) and probability amplification.
∀ {X : Type u_1} [inst : MeasurableSpace X] (k m : ℕ) (D : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure D], ProbabilityTheory.iIndepFun (fun j ω => block_extract k m ω j) (MeasureTheory.Measure.pi fun x => D)Used by
- DeclgoodBlockEvent_prob_ge_two_thirdsDeclaration kindtheorem
T4: Each block's good event has probability ≥ 2/3, transported from the base learner guarantee.
∀ {X : Type u} [inst : MeasurableSpace X] (C : ConceptClass X Bool) (L : BatchLearner X Bool) [MeasurableBatchLearner X L] (rate : ℕ → ℝ), (∀ (D : MeasureTheory.Measure X), MeasureTheory.IsProbabilityMeasure D → ∀ c ∈ C, ∀ (m : ℕ), (MeasureTheory.Measure.pi fun x => D) {xs | D {x | L.learn (fun i => (xs i, c (xs i))) x ≠ c x} ≤ ENNReal.ofReal (rate m)} ≥ ENNReal.ofReal (2 / 3)) → ∀ (D : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure D], ∀ c ∈ C, Measurable c → ∀ (k n : ℕ) (j : Fin k), (MeasureTheory.Measure.pi fun x => D) (goodBlockEvent✝ L D c rate k n j) ≥ ENNReal.ofReal (2 / 3)BatchLearnerBatchLearner.learnConceptClassFLT.ConceptLearnEvalMeasurableMeasurableBatchLearnerblock_extractgoodBlockEventUses
Used by
- DeclmeasurableSet_goodBlock_ADeclaration kindtheorem
T0: Shared helper — measurability of the "good training set" event for a single block.
∀ {X : Type u} [inst : MeasurableSpace X] (L : BatchLearner X Bool) [MeasurableBatchLearner X L] (D : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure D] (c : Concept X Bool), Measurable c → ∀ (rate : ℕ → ℝ) (n : ℕ), MeasurableSet {xs | D {x | L.learn (fun i => (xs i, c (xs i))) x ≠ c x} ≤ ENNReal.ofReal (rate n)} - Declmap_block_extract_eq_piDeclaration kindtheorem
T3: Block extraction pushforward of product measure equals product measure.
∀ {X : Type u} [inst : MeasurableSpace X] (k n : ℕ) (D : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure D] (j : Fin k), MeasureTheory.Measure.map (fun ω => block_extract k n ω j) (MeasureTheory.Measure.pi fun x => D) = MeasureTheory.Measure.pi fun x => D - DeclgoodBlockEvent_measurableDeclaration kindtheorem
T2: goodBlockEvent is measurable for each block index j.
∀ {X : Type u} [inst : MeasurableSpace X] (L : BatchLearner X Bool) [MeasurableBatchLearner X L] (D : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure D] (c : Concept X Bool), Measurable c → ∀ (rate : ℕ → ℝ) (k n : ℕ) (j : Fin k), MeasurableSet (goodBlockEvent✝ L D c rate k n j)BatchLearnerBatchLearner.learnFLT.ConceptLearnEvalMeasurableMeasurableBatchLearnerblock_extractgoodBlockEventUsed by
- Declblock_extract_measurableDeclaration kindtheorem
Block extraction is measurable: extracting block j from a pi-type is measurable.
∀ {X : Type u_1} [inst : MeasurableSpace X] (k m : ℕ) (j : Fin k), Measurable fun ω => block_extract k m ω j - Declchebyshev_seven_twelfths_boundDeclaration kindtheorem
T6: Chebyshev concentration for 7/12 threshold — when k ≥ 36/δ independent events each have probability ≥ 2/3, the fraction exceeding 7/12 is ≥ 1-δ.
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {k : ℕ} {δ : ℝ}, 0 < δ → 36 / δ ≤ ↑k → ∀ (events : Fin k → Set Ω), (∀ (j : Fin k), MeasurableSet (events j)) → ProbabilityTheory.iIndepSet (fun j => events j) μ → (∀ (j : Fin k), μ (events j) ≥ ENNReal.ofReal (2 / 3)) → μ {ω | 7 * k ≤ 12 * {j | ω ∈ events j}.card} ≥ ENNReal.ofReal (1 - δ)Used by
- Declboosted_sample_error_le_of_good_blocksDeclaration kindtheorem
T8: If ≥ 7/12 of blocks are good, the boosted hypothesis has D-error ≤ 7·max(rate(n),0).
∀ {X : Type u} [inst : MeasurableSpace X] (D : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure D] (c : Concept X Bool), Measurable c → ∀ (L : BatchLearner X Bool) [MeasurableBatchLearner X L] (rate : ℕ → ℝ) (k n : ℕ) (ω : Fin (k * n) → X), 0 < k → 7 * k ≤ 12 * {j | ω ∈ goodBlockEvent✝ L D c rate k n j}.card → D {x | (boosted_majority✝ k fun j => L.learn (fun i => (block_extract k n ω j i, c (block_extract k n ω j i))) x) ≠ c x} ≤ ENNReal.ofReal (7 * max (rate n) 0)BatchLearnerBatchLearner.learnFLT.ConceptLearnEvalMeasurableMeasurableBatchLearnerblock_extractboosted_majoritygoodBlockEventUses
Used by
- Declmajority_error_le_seven_rate_of_good_fractionDeclaration kindtheorem
T7: If ≥ 7/12 of the hypotheses have D-error ≤ ρ, majority vote has D-error ≤ 7ρ.
∀ {X : Type u} [inst : MeasurableSpace X] (D : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure D] {k : ℕ}, 0 < k → ∀ (c : Concept X Bool), Measurable c → ∀ (hs : Fin k → Concept X Bool), (∀ (j : Fin k), Measurable (hs j)) → ∀ (good : Finset (Fin k)), 7 * k ≤ 12 * good.card → ∀ (ρ : ℝ), 0 ≤ ρ → (∀ j ∈ good, D {x | hs j x ≠ c x} ≤ ENNReal.ofReal ρ) → D {x | (boosted_majority✝ k fun j => hs j x) ≠ c x} ≤ ENNReal.ofReal (7 * ρ) - Decllearn_measurable_fixedDeclaration kindtheorem
T1: A learner with joint measurability gives measurable hypotheses for fixed training data.
∀ {X : Type u} [inst : MeasurableSpace X] (L : BatchLearner X Bool) [MeasurableBatchLearner X L] {m : ℕ} (S : Fin m → X × Bool), Measurable (L.learn S) - DeclMeasurableBatchLearner.eval_measurableDeclaration kindtheorem
Joint measurability of the evaluation map
∀ {X : Type u} {inst : MeasurableSpace X} {L : BatchLearner X Bool} [self : MeasurableBatchLearner X L] (m : ℕ), Measurable fun p => L.learn p.1 p.2 - DeclMeasurableHypotheses.mem_measurableDeclaration kindtheorem
∀ {X : Type u} {inst : MeasurableSpace X} {C : ConceptClass X Bool} [self : MeasurableHypotheses X C], ∀ h ∈ C, Measurable h - HypothesishL_meas
∀ (L : BatchLearner X Bool), LearnEvalMeasurable L
- Hypothesishul
UniversalLearnable X C
- DefinitionBatchLearnerstructure
A batch learner (PAC paradigm): takes a finite sample, returns a hypothesis.
Type u → Type v → Type (max u v)
- DefinitionBatchLearner.learndef
The learning algorithm: given a sample, produce a hypothesis
{X : Type u} → {Y : Type v} → BatchLearner X Y → {m : ℕ} → (Fin m → X × Y) → Concept X Y - DefinitionConceptClassdef
A concept class is a set of concepts. Used by every paradigm, complexity measure, and criterion.
Primary definition: Set of functions. Used for PAC/agnostic PAC where concept classes are sets over which VC dimension, Rademacher complexity, covering numbers, etc. are measured. Alternative definitions below for contexts requiring decidability, enumerability, or measurability.
Type u → Type v → Type (max v u)
- DefinitionFLT.Conceptdef
A concept is a function from domain to label. This is the atomic unit that concept classes collect and learners try to approximate.
Type u → Type v → Type (max u v)
- DefinitionLearnEvalMeasurabledef
Joint measurability of a batch learner's evaluation map.
{X : Type u} → [MeasurableSpace X] → BatchLearner X Bool → Prop - DefinitionMeasurableBatchLearnerstructure
A batch learner whose evaluation map is jointly measurable.
The condition: for each sample size m, the map (S, x) ↦ L.learn S x from (Fin m → X × Bool) × X to Bool is Measurable.
This is the minimal regularity that makes the PAC success event {S | D{x | L.learn(S)(x) ≠ c(x)} ≤ ε} a MeasurableSet (via measurable_measure_prod_mk_left).
Equivalent to
LearnEvalMeasurable(Separation.lean) andAdviceEvalMeasurable(Extended.lean) for the non-advice case.(X : Type u) → [MeasurableSpace X] → BatchLearner X Bool → Prop
- DefinitionMeasurableHypothesesstructure
Every concept in C is a measurable function. Krapp-Wirth precondition: Γ(h) ∈ Σ_Z for all h ∈ H.
(X : Type u) → [MeasurableSpace X] → ConceptClass X Bool → Prop
- DefinitionPACLearnabledef
PAC (Probably Approximately Correct) learning. The central definition of computational learning theory.
Sample space: Fin m → X with i.i.d. product measure D^m. Labels: derived deterministically from target concept c (realizable case). Error: D-probability of disagreement between learner output and c.
(X : Type u) → [MeasurableSpace X] → ConceptClass X Bool → Prop
- DefinitionUniversalLearnabledef
Universal learning: distribution-free convergence rates. Strictly stronger than PAC.
Sample space: Fin m → X with i.i.d. product measure D^m (matching PACLearnable). Labels: derived deterministically from target concept c (realizable case). The rate function converges to 0, and for every m, with probability ≥ 2/3 over D^m, the learner's error is at most rate(m).
Γ₄₈ fix: changed from existential Dm to Measure.pi (CNA₁₁ definition repair).
(X : Type u) → [MeasurableSpace X] → ConceptClass X Bool → Prop
- Definitionblock_extractdef
Extract block j from a flat array of k*m elements, using finProdFinEquiv.
{α : Type u_1} → (k m : ℕ) → (Fin (k * m) → α) → Fin k → Fin m → α - Definitionboosted_majoritydef
Majority vote: returns true iff strictly more than half the votes are true.
(k : ℕ) → (Fin k → Bool) → Bool
- DefinitiongoodBlockEventdef
The event that block j produces a hypothesis with D-error ≤ rate(n).
{X : Type u} → [inst : MeasurableSpace X] → BatchLearner X Bool → MeasureTheory.Measure X → Concept X Bool → (ℕ → ℝ) → (k n : ℕ) → Fin k → Set (Fin (k * n) → X)
Verification
- Replay
- accepted
- Axioms
- Classical.choiceQuot.soundpropext
- Statement identity
- not-applicable
- Substrate
- Lean 4 kernel v4.31.0
- Dictionary pin
- design-lab@5802df4 · initial
- Frozen export
- ba68a04fbf8b
- Verified
- 2026-09-24T00:00:00Z