Advice elimination (Ben-David & Dichterman 1998): If C is PAC-learnable with concept-dependent advice from a FINITE set A (with measurability regularity), then C is PAC-learnable without advice.
Proof strategy: run the advice-augmented learner with each a ∈ A on a training portion of the sample, producing |A| candidate hypotheses. Use a validation portion to select the candidate with lowest empirical error. Union bound over |A| advice values + Hoeffding on validation controls total failure probability. Sample complexity: O(m_orig(ε/2, δ/(2|A|)) + log(|A|/δ)/ε²).
The [Fintype A] constraint is essential: for infinite A, the theorem is false (no finite union bound). [Nonempty A] ensures the advice space is inhabited.
∀ (X : Type u) [inst : MeasurableSpace X] (C : ConceptClass X Bool) [MeasurableHypotheses X C] (A : Type u_1) [inst_2 : Fintype A] [inst_3 : Nonempty A], PACLearnableWithAdviceRegular X C A → PACLearnable X C
- Decladvice_eliminationDeclaration kindtheorem
∀ (X : Type u) [inst : MeasurableSpace X] (C : ConceptClass X Bool) [MeasurableHypotheses X C] (A : Type u_1) [inst_2 : Fintype A] [inst_3 : Nonempty A], PACLearnableWithAdviceRegular X C A → PACLearnable X C
- Declused_sample_split_measureDeclaration kindtheorem
Split D^{m₁+m₂} into D^{m₁} × D^{m₂} via splitUsedEquiv.
∀ {X : Type u} [inst : MeasurableSpace X] (D : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure D] (m₁ m₂ : ℕ) (Success : Set ((Fin m₁ → X) × (Fin m₂ → X))), MeasurableSet Success → (MeasureTheory.Measure.pi fun x => D) (⇑(splitUsedEquiv✝ m₁ m₂) ⁻¹' Success) = ((MeasureTheory.Measure.pi fun x => D).prod (MeasureTheory.Measure.pi fun x => D)) SuccessUsed by
- DecltrueErrorReal_le_of_bestAdviceDeclaration kindtheorem
∀ {X : Type u} [inst : MeasurableSpace X] {A : Type u_1} [inst_1 : Fintype A] [inst_2 : Nonempty A] (cand : A → Concept X Bool) (c : Concept X Bool) (D : MeasureTheory.Measure X) {m : ℕ} (Sval : Fin m → X × Bool) (η τ : ℝ), 0 ≤ η → (∀ (a : A), |TrueErrorReal X (cand a) c D - EmpiricalError X Bool (cand a) Sval (zeroOneLoss Bool)| ≤ η) → ∀ (aStar : A), TrueErrorReal X (cand aStar) c D ≤ τ → TrueErrorReal X (cand (bestAdvice cand Sval)) c D ≤ τ + 2 * ηUsed by
- Declprob_ge_one_sub_complDeclaration kindtheorem
For a probability measure, μ(S) ≥ 1 - μ(Sᶜ), and hence μ(S) ≥ 1 - δ if μ(Sᶜ) ≤ δ.
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (S : Set Ω) (δ : ENNReal), μ Sᶜ ≤ δ → μ S ≥ 1 - δUsed by
- Declnat_pair_sample_marginalDeclaration kindtheorem
Sampling Nat.pair m₁ m₂ coordinates and taking the first m₁+m₂ gives the same measure as sampling m₁+m₂ coordinates directly. The extra junk coordinates integrate out via pi_cylinder_set_eq.
∀ {X : Type u} [inst : MeasurableSpace X] (D : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure D] [MeasureTheory.SigmaFinite D] (m₁ m₂ : ℕ) (Success : Set (Fin (m₁ + m₂) → X)), MeasurableSet Success → (MeasureTheory.Measure.pi fun x => D) (usedPrefix✝ m₁ m₂ ⁻¹' Success) = (MeasureTheory.Measure.pi fun x => D) SuccessUsed by
- Declpi_cylinder_set_eqDeclaration kindtheorem
Cylinder set measure on product: if an event depends only on the first coordinates (those satisfying predicate p), then its measure under D^ι equals D^{p}(event). Uses piEquivPiSubtypeProd: D^ι ≃ D^{p} × D^{¬p}, and (D^{p} × D^{¬p})(A × univ) = D^{p}(A) · D^{¬p}(univ) = D^{p}(A).
∀ {ι : Type u_1} [inst : Fintype ι] [DecidableEq ι] {X : Type u} [inst_2 : MeasurableSpace X] (D : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure D] [MeasureTheory.SigmaFinite D] (p : ι → Prop) [inst_5 : DecidablePred p] (S : Set ({ i // p i } → X)), MeasurableSet S → (MeasureTheory.Measure.pi fun x => D) {xs | (fun i => xs ↑i) ∈ S} = (MeasureTheory.Measure.pi fun x => D) SUsed by
- DecllearnWithAdvice_measurable_fixedDeclaration kindtheorem
∀ {X : Type u} [inst : MeasurableSpace X] {A : Type u_1} (LA : LearnerWithAdvice X Bool A), AdviceEvalMeasurable LA → ∀ (a : A) {m : ℕ} (S : Fin m → X × Bool), Measurable (LA.learnWithAdvice a S)Used by
- Declfinite_validation_family_boundDeclaration kindtheorem
∀ {X : Type u} [inst : MeasurableSpace X] {A : Type u_1} [inst_1 : Fintype A] (D : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure D] (c : Concept X Bool), Measurable c → ∀ (cand : A → Concept X Bool), (∀ (a : A), Measurable (cand a)) → ∀ (m : ℕ), 0 < m → ∀ (η : ℝ), 0 < η → η ≤ 1 → (MeasureTheory.Measure.pi fun x => D) {xs | ∃ a, |TrueErrorReal X (cand a) c D - EmpiricalError X Bool (cand a) (fun i => (xs i, c (xs i))) (zeroOneLoss Bool)| ≥ η} ≤ ENNReal.ofReal (↑(Fintype.card A) * 2 * Real.exp (-2 * ↑m * η ^ 2))Used by
- Declhoeffding_one_sided_upperDeclaration kindtheorem
Upper-tail Hoeffding: for iid Bernoulli(p) draws, the empirical average overshoots the mean by ≥ t with probability ≤ exp(-2mt²).
This is the mirror of
hoeffding_one_sided(which bounds the lower tail). The proof uses the same sub-Gaussian machinery with Z_i = indicator(x_i) - p (instead of p - indicator(x_i)).∀ {X : Type u} [inst : MeasurableSpace X] (D : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure D] (h c : Concept X Bool) (m : ℕ), 0 < m → ∀ (t : ℝ), 0 < t → t ≤ 1 → MeasurableSet {x | h x ≠ c x} → (MeasureTheory.Measure.pi fun x => D) {xs | EmpiricalError X Bool h (fun i => (xs i, c (xs i))) (zeroOneLoss Bool) ≥ TrueErrorReal X h c D + t} ≤ ENNReal.ofReal (Real.exp (-2 * ↑m * t ^ 2)) - Declhoeffding_one_sidedDeclaration kindtheorem
One-sided Hoeffding: for iid Bernoulli(p) draws, the empirical average undershoots the mean by ≥ t with probability ≤ exp(-2mt²).
Proof strategy (3 steps):
1. MGF bound (Hoeffding's lemma): For X ∈ [0,1] with E[X] = p, E[exp(s(X-p))] ≤ exp(s²/8).
- Adapt from
cosh_le_exp_sq_halfinfrastructure in Rademacher.lean. - Key: convexity of exp on [0,1] gives E[exp(sX)] ≤ p·exp(s) + (1-p)·exp(0), then the s²/8 bound follows from ln(1 + x) ≤ x and Taylor expansion.
have mgf_bound : ∀ (s : ℝ), ∫ x, Real.exp (s * (indicator x - p)) ∂D ≤ Real.exp (s^2 / 8) := by ...
2. Product independence: E[exp(s·∑(X_i-p))] = ∏ E[exp(s(X_i-p))] ≤ exp(ms²/8).
- Uses
MeasureTheory.Measure.piindependence structure. - Needs:
Measure.piintegral factorization for product of functions. - MEASURABILITY:
fun xs => Real.exp (s * ∑ i, f (xs i))is measurable (composition of measurable functions).have product_bound : ∀ (s : ℝ), ∫ xs, Real.exp (s * ∑ i, (indicator (xs i) - p)) ∂Measure.pi (fun _ => D) ≤ Real.exp (m * s^2 / 8) := by ...
3. Exponential Markov + optimize: P[∑(X_i-p) ≤ -mt] = P[exp(-s·∑(X_i-p)) ≥ exp(smt)] ≤ exp(-smt + ms²/8). Optimize over s: set s = 4t to get ≤ exp(-2mt²).
- Uses Markov's inequality in ENNReal form.
- CAST ISSUE: Markov gives ENNReal bound, need to convert exp(-2mt²) between ENNReal.ofReal and the measure value.
have markov_step : ∀ (s : ℝ) (hs : 0 < s), Measure.pi (fun _ => D) {xs | ∑ i, (indicator (xs i) - p) ≤ -(m : ℝ) * t} ≤ ENNReal.ofReal (Real.exp (-(s * m * t) + m * s^2 / 8)) := by ... have optimize : Real.exp (-(4*t * m * t) + m * (4*t)^2 / 8) = Real.exp (-2 * m * t^2) := by ring_nf
CAST ISSUES to watch:
m : ℕneeds cast toℝin the exponent:(m : ℝ)EmpiricalErrorreturnsℝ,TrueErrorRealreturnsℝ, good — no ENNReal gap- The measure value is
ENNReal, the boundexp(-2mt²)isℝ≥0∞viaENNReal.ofReal
References: SSBD Lemma B.3, Hoeffding (1963)
∀ {X : Type u} [inst : MeasurableSpace X] (D : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure D] (h c : Concept X Bool) (m : ℕ), 0 < m → ∀ (t : ℝ), 0 < t → t ≤ 1 → MeasurableSet {x | h x ≠ c x} → (MeasureTheory.Measure.pi fun x => D) {xs | EmpiricalError X Bool h (fun i => (xs i, c (xs i))) (zeroOneLoss Bool) ≤ TrueErrorReal X h c D - t} ≤ ENNReal.ofReal (Real.exp (-2 * ↑m * t ^ 2)) - Adapt from
- DeclbestAdvice.congr_simpDeclaration kindtheorem
∀ {X : Type u} [inst : MeasurableSpace X] {A : Type u_1} [inst_1 : Fintype A] [inst_2 : Nonempty A] (cand cand_1 : A → Concept X Bool), cand = cand_1 → ∀ {m : ℕ} (Sval Sval_1 : Fin m → X × Bool), Sval = Sval_1 → bestAdvice cand Sval = bestAdvice cand_1 Sval_1Used by
- DeclMeasurableHypotheses.mem_measurableDeclaration kindtheorem
∀ {X : Type u} {inst : MeasurableSpace X} {C : ConceptClass X Bool} [self : MeasurableHypotheses X C], ∀ h ∈ C, Measurable hUsed by
- Hypothesisa
PACLearnableWithAdviceRegular X C A
- DefinitionAdviceEvalMeasurabledef
Joint measurability of a sample-dependent advice learner's evaluation map.
{X : Type u} → [MeasurableSpace X] → {A : Type u_1} → LearnerWithAdvice X Bool A → Prop - 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)
- DefinitionEmpiricalErrordef
Empirical error: average loss on a finite sample.
(X : Type u) → (Y : Type v) → Concept X Y → {m : ℕ} → (Fin m → X × Y) → LossFunction Y → ℝ - 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)
- DefinitionLearnerWithAdvicestructure
A learner augmented with advice.
Type u → Type v → Type u_1 → Type (max (max u u_1) v)
- DefinitionLearnerWithAdvice.learnWithAdvicedef
Advice-augmented learning: advice → sample → hypothesis
{X : Type u} → {Y : Type v} → {A : Type u_1} → LearnerWithAdvice X Y A → A → {m : ℕ} → (Fin m → X × Y) → Concept X Y - 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
- DefinitionPACLearnableWithAdviceRegulardef
PAC learnability with finite advice, plus measurability for holdout validation.
(X : Type u) → [MeasurableSpace X] → ConceptClass X Bool → (A : Type u_1) → [Fintype A] → [Nonempty A] → Prop
- DefinitionTrueErrordef
True error (0-1 loss, realizable case): D-probability of disagreement. This is what PACLearnable's success event measures.
(X : Type u) → [inst : MeasurableSpace X] → Concept X Bool → Concept X Bool → MeasureTheory.Measure X → ENNReal
- DefinitionTrueErrorRealdef
True error in ℝ: for use in bounds involving subtraction/absolute value. COUNTER-1 of TrueError. The toReal bridge loses information when the measure is ⊤.
(X : Type u) → [inst : MeasurableSpace X] → Concept X Bool → Concept X Bool → MeasureTheory.Measure X → ℝ
- DefinitionbestAdvicedef
Choose the advice value with minimum validation empirical error.
{X : Type u} → [MeasurableSpace X] → {A : Type u_1} → [Fintype A] → [Nonempty A] → (A → Concept X Bool) → {m : ℕ} → (Fin m → X × Bool) → A - DefinitionsplitUsedEquivdef
Split Fin (m₁ + m₂) → X into (Fin m₁ → X) × (Fin m₂ → X) measurably.
{X : Type u} → [inst : MeasurableSpace X] → (m₁ m₂ : ℕ) → (Fin (m₁ + m₂) → X) ≃ᵐ (Fin m₁ → X) × (Fin m₂ → X) - DefinitionusedPrefixdef
Extract the first m₁ + m₂ coordinates from a sample of size Nat.pair m₁ m₂.
{X : Type u} → [MeasurableSpace X] → (m₁ m₂ : ℕ) → (Fin (Nat.pair m₁ m₂) → X) → Fin (m₁ + m₂) → X - DefinitionzeroOneLossdef
The 0-1 loss for classification.
(Y : Type v) → [DecidableEq Y] → LossFunction Y
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
- d4155a9f1007
- Verified
- 2026-09-24T00:00:00Z