Mathesis

Dhruv GuptaZetetic-Dhruvperson2026-09-24T00:00:00Z

Declfundamental_vc_compression_with_info

∀ (X : Type u) (C : ConceptClass X Bool), VCDim X C < ⊤ ↔ ∃ k cs, CompressionSchemeWithInfo.size cs = k

TopicCompression

ThesisStepDefinition

Declfundamental_vc_compression_with_infoDeclaration kindtheorem
```
∀ (X : Type u) (C : ConceptClass X Bool), VCDim X C < ⊤ ↔ ∃ k cs, CompressionSchemeWithInfo.size cs = k
```
CompressionSchemeWithInfo CompressionSchemeWithInfo.size CompressionSchemeWithInfo0 ConceptClass VCDim
Uses
- compression_with_info_imp_vcdim_finite
- vcdim_finite_imp_compression_with_info
Declvcdim_finite_imp_compression_with_infoDeclaration kindtheorem
The forward direction of the Moran-Yehudayoff theorem: finite VC dimension implies existence of a compression scheme with finite side information.
The construction: 1. Build a proper finite-support learner L from VC + Sauer-Shelah 2. For sample S: extract c, Y = pointSupport S, HY = hypothesis envelope 3. Apply approximate minimax on the agreement game → distribution p on HY 4. Apply VC ε-approximation on agreement tests → T representative hypotheses 5. Kernel = union of witness subsets for T hypotheses 6. Side info = incidence: which hypothesis's witness contains each kernel point 7. Reconstruct by majority vote over T hypotheses
```
∀ (X : Type u) (C : ConceptClass X Bool), VCDim X C < ⊤ → ∃ k cs, CompressionSchemeWithInfo.size cs = k
```
CompressionSchemeWithInfo.Info CompressionSchemeWithInfo.info_finite CompressionSchemeWithInfo.size CompressionSchemeWithInfo0 ConceptClass FLT.Concept ProperFiniteSupportLearner ProperFiniteSupportLearner.sampleBound VCDim
Uses
- moran_yehudayoff_forward_construction
- vcdim_finite_imp_proper_finite_support_learner
Used by
- fundamental_vc_compression_with_info
Declvcdim_finite_imp_proper_finite_support_learnerDeclaration kindtheorem
Finite VC dimension implies existence of a proper finite-support learner. The construction uses ERM + finite_support_vc_approx on the disagreement family.
```
∀ (X : Type u) (C : ConceptClass X Bool), Set.Nonempty C → VCDim X C < ⊤ → ∃ _L, True
```
ConceptClass FLT.Concept FinitePMF Finset.boolVCDim ProperFiniteSupportLearner VCDim boolTestExpectation disagreementFamily empiricalPMF labeledSampleOfFinset supportError
Uses
Used by
- vcdim_finite_imp_compression_with_info
DeclsupportError_eq_boolTestExpectationDeclaration kindtheorem
supportError expressed in terms of boolTestExpectation of a disagreement test.
```
∀ {X : Type u} (Y : Finset X) (q : FinitePMF ↥Y) (h c : X → Bool),
  supportError Y q h c = boolTestExpectation q fun y => decide (h ↑y ≠ c ↑y)
```
FinitePMF FinitePMF.prob boolTestExpectation supportError
Used by
- vcdim_finite_imp_proper_finite_support_learner
DecldisagreementFamily_boolVCDim_leDeclaration kindtheorem
VC dimension of the disagreement family is bounded by VCDim(C). Restriction to Y and xor with c do not increase shattering dimension.
```
∀ {X : Type u} [inst : DecidableEq X] (C : ConceptClass X Bool) (c : X → Bool) (Y : Finset X) {d : ℕ},
  VCDim X C ≤ ↑d → (disagreementFamily✝ C c Y).boolVCDim ≤ d
```
ConceptClass FLT.Concept Finset.boolVCDim Shatters VCDim boolFamilyToFinsetFamily disagreementFamily
Used by
- vcdim_finite_imp_proper_finite_support_learner
Declmoran_yehudayoff_forward_constructionDeclaration kindtheorem
The Moran-Yehudayoff forward construction. Uses finalizeIncidenceScheme to package the majority-vote scheme with universe-correct Info type.
The agent must provide: compressCore, blockHyp, rowHyp, hsmall, hsub, hagree, hmajor. These are the MY wiring.
```
∀ (X : Type u) (C : ConceptClass X Bool),
  Set.Nonempty C →
    ∀ (L : ProperFiniteSupportLearner X C), VCDim X C < ⊤ → ∀ (_K : ℕ), ∃ k cs, CompressionSchemeWithInfo.size cs = k
```
CompressionSchemeWithInfo.size CompressionSchemeWithInfo0 ConceptClass FLT.Concept FinitePMF FinitePMF.prob Finset.boolVCDim IncidenceInfo ProperFiniteSupportLearner ProperFiniteSupportLearner.learn ProperFiniteSupportLearner.sampleBound VCDim agreeTest agreeTests boolGamePayoff boolTestExpectation boundedSubsamples decodeWitnessLabel decodeWitnessXCoords empiricalPMF encodeWitnessInfo hypothesisEnvelope labeledSampleOfFinset pointSupport uniformPMF
Uses
Used by
- vcdim_finite_imp_compression_with_info

Declroundtrip_blockHyp_eq_repDeclaration kindtheorem

Generic roundtrip theorem for the hround sorry.

If:

encodeWitnessInfo is used in compressCore,
decodeWitnessXCoords and decodeWitnessLabel are used in blockHyp, and
the kernel contains the witness pairs with the correct labels,

then the decoded block hypothesis is exactly the representative hypothesis.

∀ {X : Type u} [inst : DecidableEq X] (learn : {m : ℕ} → (Fin m → X × Bool) → X → Bool) (kernel : Finset (X × Bool))
  (c : X → Bool) (K : ℕ) (W : Finset X) (h : X → Bool),
  kernel.card ≤ K →
    (∀ x ∈ W, (x, c x) ∈ kernel) →
      (∀ p ∈ kernel, p.2 = c p.1) →
        learn (labeledSampleOfFinset c W) = h →
          ∀ (x : X),
            have info := encodeWitnessInfo kernel c K W;
            have blockXCoords := decodeWitnessXCoords kernel info;
            have blockLabel := decodeWitnessLabel kernel;
            learn (labeledSampleOfFinset blockLabel blockXCoords) x = h x

decodeWitnessLabel decodeWitnessXCoords encodeWitnessInfo labeledSampleOfFinset

Uses

decodeWitnessLabel_eq_on_encoded
decodeWitnessXCoords_encode_eq
labeledSampleOfFinset_eq_of_eq_on_support

Used by

moran_yehudayoff_forward_construction

DecllabeledSampleOfFinset_eq_of_eq_on_supportDeclaration kindtheorem
If two label functions agree on all points of Z, then the labeled samples they induce on Z.equivFin are equal.
```
∀ {X : Type u} [DecidableEq X] {ℓ₁ ℓ₂ : X → Bool} {Z : Finset X},
  (∀ x ∈ Z, ℓ₁ x = ℓ₂ x) → labeledSampleOfFinset ℓ₁ Z = labeledSampleOfFinset ℓ₂ Z
```
labeledSampleOfFinset
Used by
- roundtrip_blockHyp_eq_rep
DecldecodeWitnessXCoords_encode_eqDeclaration kindtheorem
If every (x, c x) with x ∈ W lies in kernel, and kernel.card ≤ K, then decoding the encoded witness positions gives back exactly W.
```
∀ {X : Type u} [inst : DecidableEq X] (kernel : Finset (X × Bool)) (c : X → Bool) {K : ℕ} (W : Finset X),
  kernel.card ≤ K → (∀ x ∈ W, (x, c x) ∈ kernel) → decodeWitnessXCoords kernel (encodeWitnessInfo kernel c K W) = W
```
decodeWitnessXCoords encodeWitnessInfo
Used by
- roundtrip_blockHyp_eq_rep
DecldecodeWitnessLabel_eq_on_encodedDeclaration kindtheorem
On the encoded witness support, the decoded label function agrees with the true label function c, provided every pair in the kernel has the correct second coordinate.
```
∀ {X : Type u} [inst : DecidableEq X] (kernel : Finset (X × Bool)) (c : X → Bool) (W : Finset X),
  (∀ x ∈ W, (x, c x) ∈ kernel) → (∀ p ∈ kernel, p.2 = c p.1) → ∀ x ∈ W, decodeWitnessLabel kernel x = c x
```
decodeWitnessLabel
Used by
- roundtrip_blockHyp_eq_rep
Declmwu_approx_minimaxDeclaration kindtheorem
Genuine approximate minimax via MWU regret extraction. If every column mixture admits a pure row with expected payoff ≥ v, then there is a row mixture with payoff ≥ v - ε against every column.
```
∀ {R : Type u_1} {C : Type u_2} [inst : Fintype R] [inst_1 : Fintype C] [Nonempty R] [Nonempty C] [DecidableEq R]
  [DecidableEq C] (M : R → C → Bool) (v ε : ℝ),
  0 < ε →
    (∀ (q : FinitePMF C), ∃ r, v ≤ ∑ c, q.prob c * if M r c = true then 1 else 0) →
      ∃ p, ∀ (c : C), v - ε ≤ boolGamePayoff M p c
```
FinitePMF FinitePMF.prob MWUConfig.potential MWUConfig.weights boolGamePayoff empiricalPMF mwuConfig mwuHitCount mwuRows uniformPMF
Uses
Used by
- moran_yehudayoff_forward_construction
Declweight_le_potentialDeclaration kindtheorem
A single weight is bounded by the potential.
```
∀ {C : Type u_1} [inst : Fintype C] (cfg : MWUConfig C) (c : C), cfg.weights c ≤ cfg.potential
```
MWUConfig MWUConfig.potential MWUConfig.weights
Uses
- MWUConfig.weights_pos
Used by
- mwu_approx_minimax

Declmwu_weight_eq_pow_hitCountDeclaration kindtheorem

Exact individual-weight tracking: the weight of column c after T rounds is (1-η) to the number of rounds in which c was hit.

∀ {R : Type u_1} {C : Type u_2} [inst : Fintype R] [inst_1 : Fintype C] [inst_2 : Nonempty C] (M : R → C → Bool) (η : ℝ)
  (hη1 : η < 1) (v : ℝ) (hrow : ∀ (q : FinitePMF C), ∃ r, v ≤ ∑ c, q.prob c * if M r c = true then 1 else 0) (T : ℕ)
  (c : C), (mwuConfig M η hη1 v hrow T).weights c = (1 - η) ^ mwuHitCount✝ M η hη1 v hrow T c

FinitePMF FinitePMF.prob MWUConfig MWUConfig.toPMF MWUConfig.weights mwuConfig mwuHitCount mwuRun mwuUpdateWeights

Uses

MWUConfig.mk.congr_simp
MWUConfig.weights_pos

Used by

mwu_approx_minimax

DeclMWUConfig.mk.congr_simpDeclaration kindtheorem

∀ {C : Type u_1} [inst : Fintype C] (weights weights_1 : C → ℝ) (e_weights : weights = weights_1)
  (weights_pos : ∀ (c : C), 0 < weights c),
  { weights := weights, weights_pos := weights_pos } = { weights := weights_1, weights_pos := ⋯ }

MWUConfig

Used by

mwu_weight_eq_pow_hitCount

Declmwu_potential_T_boundDeclaration kindtheorem
Potential bound after T steps: Φ_T ≤ |C| · (1 - ηv)^T.
This is the core MWU guarantee. Combined with individual weight lower bounds (w_T(c) = (1-η)^{losses(c)}), it yields the regret bound.
```
∀ {R : Type u_1} {C : Type u_2} [inst : Fintype R] [inst_1 : Fintype C] [inst_2 : Nonempty C] (M : R → C → Bool)
  (η : ℝ),
  0 ≤ η →
    ∀ (hη1 : η < 1) (v : ℝ) (hrow : ∀ (q : FinitePMF C), ∃ r, v ≤ ∑ c, q.prob c * if M r c = true then 1 else 0)
      (T : ℕ), (mwuConfig M η hη1 v hrow T).potential ≤ ↑(Fintype.card C) * (1 - η * v) ^ T
```
FinitePMF FinitePMF.prob MWUConfig MWUConfig.potential MWUConfig.toPMF mwuConfig mwuRun mwuUpdateWeights
Uses
Used by
- mwu_approx_minimax

Declpotential_one_step_boundDeclaration kindtheorem

Potential bound after one step: Φ' ≤ Φ · (1 - η·v).

∀ {R : Type u_1} {C : Type u_2} [Fintype R] [inst : Fintype C] [inst_1 : Nonempty C] (M : R → C → Bool) (η : ℝ),
  0 ≤ η →
    ∀ (hη1 : η < 1) (v : ℝ) (hrow : ∀ (q : FinitePMF C), ∃ r, v ≤ ∑ c, q.prob c * if M r c = true then 1 else 0)
      (cfg : MWUConfig C), (mwuUpdateWeights M η hη1 cfg ⋯.choose).potential ≤ cfg.potential * (1 - η * v)

FinitePMF FinitePMF.prob MWUConfig MWUConfig.potential MWUConfig.toPMF MWUConfig.weights mwuUpdateWeights

Uses

best_response_payoff_weights

Used by

mwu_potential_T_bound

Declbest_response_payoff_weightsDeclaration kindtheorem

Best response payoff ≥ v · Φ in terms of weights.

∀ {R : Type u_1} {C : Type u_2} [Fintype R] [inst : Fintype C] [inst_1 : Nonempty C] (M : R → C → Bool) (v : ℝ)
  (hrow : ∀ (q : FinitePMF C), ∃ r, v ≤ ∑ c, q.prob c * if M r c = true then 1 else 0) (cfg : MWUConfig C),
  v * cfg.potential ≤ ∑ c, cfg.weights c * if M ⋯.choose c = true then 1 else 0

FinitePMF FinitePMF.prob MWUConfig MWUConfig.potential MWUConfig.toPMF MWUConfig.weights

Uses

MWUConfig.potential_pos

Used by

potential_one_step_bound

DeclMWUConfig.potential_posDeclaration kindtheorem
```
∀ {C : Type u_1} [inst : Fintype C] [Nonempty C] (cfg : MWUConfig C), 0 < cfg.potential
```
MWUConfig MWUConfig.potential MWUConfig.weights
Uses
- MWUConfig.weights_pos
Used by
- best_response_payoff_weights
DeclMWUConfig.weights_posDeclaration kindtheorem
```
∀ {C : Type u_1} [inst : Fintype C] (self : MWUConfig C) (c : C), 0 < self.weights c
```
MWUConfig MWUConfig.weights
Used by

DeclmwuUpdateWeights.congr_simpDeclaration kindtheorem

∀ {C : Type u_1} [inst : Fintype C] {R : Type u_2} (M M_1 : R → C → Bool),
  M = M_1 →
    ∀ (η η_1 : ℝ) (e_η : η = η_1) (hη1 : η < 1) (cfg cfg_1 : MWUConfig C),
      cfg = cfg_1 → ∀ (r r_1 : R), r = r_1 → mwuUpdateWeights M η hη1 cfg r = mwuUpdateWeights M_1 η_1 ⋯ cfg_1 r_1

MWUConfig mwuUpdateWeights

Used by

mwu_potential_T_bound

DeclmwuInit_potentialDeclaration kindtheorem
```
∀ (C : Type u_1) [inst : Fintype C], (mwuInit C).potential = ↑(Fintype.card C)
```
MWUConfig.potential MWUConfig.weights mwuInit
Used by
- mwu_potential_T_bound
Declminimax_value_le_oneDeclaration kindtheorem
The minimax value of a Boolean game is at most 1.
```
∀ {R : Type u_1} {C : Type u_2} [Fintype R] [inst : Fintype C] [Nonempty C] (M : R → C → Bool) (v : ℝ),
  (∀ (q : FinitePMF C), ∃ r, v ≤ ∑ c, q.prob c * if M r c = true then 1 else 0) → v ≤ 1
```
FinitePMF FinitePMF.prob uniformPMF
Uses
- FinitePMF.prob_nonneg
- FinitePMF.prob_sum_one
Used by
- mwu_approx_minimax
- mwu_potential_T_bound

DeclhitRate_from_potentialDeclaration kindtheorem

Arithmetic core: from the potential bound and sufficiently small η / large T, deduce a per-column hit-rate lower bound. Uses Real.log — exactly 4 Mathlib lemmas.

∀ {N H T : ℕ} {η v ε : ℝ},
  0 < ↑N →
    0 < η →
      η < 1 →
        v ≤ 1 →
          0 < T → (1 - η) ^ H ≤ ↑N * (1 - η * v) ^ T → η ≤ ε / 4 → Real.log ↑N / (η * ↑T) ≤ ε / 4 → v - ε ≤ ↑H / ↑T

Used by

mwu_approx_minimax

DeclboolGamePayoff_nonnegDeclaration kindtheorem
```
∀ {R : Type u_1} {C : Type u_2} [inst : Fintype R] (M : R → C → Bool) (p : FinitePMF R) (c : C),
  0 ≤ boolGamePayoff M p c
```
FinitePMF FinitePMF.prob boolGamePayoff
Uses
- FinitePMF.prob_nonneg
Used by
- mwu_approx_minimax

DeclboolGamePayoff_empirical_eq_hitCountDeclaration kindtheorem

Empirical payoff of the MWU row sequence equals the normalized hit count.

∀ {R : Type u_1} {C : Type u_2} [inst : Fintype R] [inst_1 : Fintype C] [inst_2 : Nonempty C] [inst_3 : DecidableEq R]
  (M : R → C → Bool) (η : ℝ) (hη1 : η < 1) (v : ℝ)
  (hrow : ∀ (q : FinitePMF C), ∃ r, v ≤ ∑ c, q.prob c * if M r c = true then 1 else 0) {T : ℕ} (hT : 0 < T) (c : C),
  boolGamePayoff M (empiricalPMF hT (mwuRows M η hη1 v hrow T)) c = ↑(mwuHitCount✝ M η hη1 v hrow T c) / ↑T

FinitePMF FinitePMF.prob boolGamePayoff empiricalPMF mwuHitCount mwuRows

Uses

boolGamePayoff_empirical_eq_avg
mwuHitCount_eq_sum_indicator

Used by

mwu_approx_minimax

DeclmwuHitCount_eq_sum_indicatorDeclaration kindtheorem

The recursive hit counter agrees with the sum of Boolean indicators over the emitted row sequence.

∀ {R : Type u_1} {C : Type u_2} [inst : Fintype R] [inst_1 : Fintype C] [inst_2 : Nonempty C] (M : R → C → Bool) (η : ℝ)
  (hη1 : η < 1) (v : ℝ) (hrow : ∀ (q : FinitePMF C), ∃ r, v ≤ ∑ c, q.prob c * if M r c = true then 1 else 0) (T : ℕ)
  (c : C), ↑(mwuHitCount✝ M η hη1 v hrow T c) = ∑ t, if M (mwuRows M η hη1 v hrow T t) c = true then 1 else 0

FinitePMF FinitePMF.prob MWUConfig MWUConfig.toPMF mwuConfig mwuHitCount mwuRows mwuRun

Used by

boolGamePayoff_empirical_eq_hitCount

DeclboolGamePayoff_empirical_eq_avgDeclaration kindtheorem

Specialized empirical-payoff identity for ApproxMinimax (avoids cyclic import with FiniteVCApprox).

∀ {R : Type u_1} {C : Type u_2} [inst : Fintype R] [inst_1 : DecidableEq R] {T : ℕ} (hT : 0 < T) (rs : Fin T → R)
  (M : R → C → Bool) (c : C), boolGamePayoff M (empiricalPMF hT rs) c = (∑ t, if M (rs t) c = true then 1 else 0) / ↑T

FinitePMF.prob boolGamePayoff empiricalPMF

Used by

boolGamePayoff_empirical_eq_hitCount

DeclhypothesisEnvelope_subDeclaration kindtheorem
Every hypothesis in the envelope is in C.
```
∀ {X : Type u} {C : ConceptClass X Bool} (L : ProperFiniteSupportLearner X C) (c : X → Bool) (Y : Finset X),
  ∀ h ∈ hypothesisEnvelope L c Y, h ∈ C
```
ConceptClass FLT.Concept ProperFiniteSupportLearner ProperFiniteSupportLearner.learn ProperFiniteSupportLearner.sampleBound boundedSubsamples hypothesisEnvelope labeledSampleOfFinset
Uses
- ProperFiniteSupportLearner.output_mem
Used by
- moran_yehudayoff_forward_construction
DeclProperFiniteSupportLearner.output_memDeclaration kindtheorem
```
∀ {X : Type u} {C : ConceptClass X Bool} (self : ProperFiniteSupportLearner X C) {m : ℕ} (S : Fin m → X × Bool),
  self.learn S ∈ C
```
ConceptClass FLT.Concept ProperFiniteSupportLearner ProperFiniteSupportLearner.learn
Used by
- hypothesisEnvelope_sub
Declgood_on_support_gives_row_responseDeclaration kindtheorem
For each C-realizable sample, the proper learner provides a row-response for the minimax game on the hypothesis envelope.
```
∀ {X : Type u} {C : ConceptClass X Bool} (L : ProperFiniteSupportLearner X C),
  ∀ c ∈ C,
    ∀ (Y : Finset X) [Nonempty ↥Y] (HY : Finset (X → Bool)),
      HY = hypothesisEnvelope L c Y →
        ∀ (q : FinitePMF ↥Y), ∃ h, 2 / 3 ≤ ∑ y, q.prob y * if decide (↑h ↑y = c ↑y) = true then 1 else 0
```
ConceptClass FLT.Concept FinitePMF FinitePMF.prob ProperFiniteSupportLearner ProperFiniteSupportLearner.learn ProperFiniteSupportLearner.sampleBound boundedSubsamples hypothesisEnvelope labeledSampleOfFinset supportError
Uses
- ProperFiniteSupportLearner.good_on_support
- supportAgreement_eq_one_sub_supportError
Used by
- moran_yehudayoff_forward_construction
DeclsupportAgreement_eq_one_sub_supportErrorDeclaration kindtheorem
Weighted agreement = 1 - supportError.
```
∀ {X : Type u} (Y : Finset X) (q : FinitePMF ↥Y) (h c : X → Bool),
  (∑ y, q.prob y * if h ↑y = c ↑y then 1 else 0) = 1 - supportError Y q h c
```
FinitePMF FinitePMF.prob supportError
Uses
- FinitePMF.prob_sum_one
Used by
- good_on_support_gives_row_response
DeclProperFiniteSupportLearner.good_on_supportDeclaration kindtheorem
```
∀ {X : Type u} {C : ConceptClass X Bool} (self : ProperFiniteSupportLearner X C),
  ∀ c ∈ C,
    ∀ (Y : Finset X) (q : FinitePMF ↥Y),
      ∃ Z ⊆ Y, Z.card ≤ self.sampleBound ∧ supportError Y q (self.learn (labeledSampleOfFinset c Z)) c ≤ 1 / 3
```
ConceptClass FLT.Concept FinitePMF ProperFiniteSupportLearner ProperFiniteSupportLearner.learn ProperFiniteSupportLearner.sampleBound labeledSampleOfFinset supportError
Used by
- good_on_support_gives_row_response
Declfinite_support_vc_approxDeclaration kindtheorem
Finite-support distributions uniformly approximate any distribution on a VC class. For a class of VC dimension at most d and any ε > 0, there exists T = T(d, ε) such that every finitely supported distribution μ is within ε (uniformly over the class) of some empirical distribution on T points. A density-style reduction that lets the approximate minimax / MWU machinery, which lives in finite support, apply to general distributions.
```
∀ (d : ℕ) (ε : ℝ),
  0 < ε →
    ∃ T,
      ∃ (hT : 0 < T),
        ∀ {H : Type u_1} [inst : Fintype H] [inst_1 : DecidableEq H] (A : Finset (H → Bool)),
          A.boolVCDim ≤ d →
            ∀ (μ : FinitePMF H),
              ∃ hs, ∀ a ∈ A, |boolTestExpectation μ a - boolTestExpectation (empiricalPMF hT hs) a| ≤ ε
```
ConceptClass EmpiricalError FLT.Concept FinitePMF FinitePMF.prob FinitePMF.toPMF Finset.boolVCDim GrowthFunction Shatters TrueErrorReal VCDim boolFamilyToFinsetFamily boolTestExpectation empiricalPMF extendBool liftClass zeroOneLoss
Uses
Used by
- moran_yehudayoff_forward_construction
- vcdim_finite_imp_proper_finite_support_learner

DecltrueErrorReal_extend_falseDeclaration kindtheorem

∀ {H : Type u_1} [inst : Fintype H] [DecidableEq H] [inst_2 : MeasurableSpace H] [MeasurableSingletonClass H]
  (μ : FinitePMF H) (a : H → Bool),
  TrueErrorReal (H ⊕ ℕ) (extendBool✝ a) (fun x => false) (PMF.map Sum.inl (FinitePMF.toPMF✝ μ)).toMeasure =
    boolTestExpectation μ a

FinitePMF FinitePMF.prob FinitePMF.toPMF TrueError TrueErrorReal boolTestExpectation extendBool

Uses

FinitePMF.prob_nonneg
FinitePMF.prob_sum_one

Used by

finite_support_vc_approx

Declsymmetrization_uc_boundDeclaration kindtheorem
The symmetrization uniform convergence bound: two-sided version. P[∃h∈C: |TrueErr-EmpErr| ≥ ε] ≤ 4·GF(C,2m)·exp(-mε²/8).
Proof strategy (4 steps):
1. Decompose absolute value: |TrueErr - EmpErr| ≥ ε ↔ (TrueErr - EmpErr ≥ ε) ∨ (EmpErr - TrueErr ≥ ε)
have abs_decomp : ∀ (a b : ℝ), |a - b| ≥ ε ↔ a - b ≥ ε ∨ b - a ≥ ε := by intro a b; constructor · intro h; by_cases h' : a - b ≥ ε · exact Or.inl h' · exact Or.inr (by linarith [abs_sub_comm a b, le_abs_self (a - b)]) · intro h; cases h with | inl h => exact le_trans (le_of_eq (abs_of_nonneg (by linarith))) (by linarith) | inr h => exact le_trans (le_of_eq (abs_of_nonpos (by linarith) ▸ ...)) ...
2. Upper tail: P[∃h∈C: TrueErr-EmpErr ≥ ε] ≤ 2·GF(C,2m)·exp(-mε²/8)
- Direct application of symmetrization_step + double_sample_pattern_bound.
3. Lower tail: P[∃h∈C: EmpErr-TrueErr ≥ ε] ≤ 2·GF(C,2m)·exp(-mε²/8)
- Apply the symmetric argument: swap roles of S and S' in the double sample.
- Equivalently, apply symmetrization_step to the event EmpErr-TrueErr ≥ ε and bound the double-sample event {EmpErr_S - EmpErr_{S'} ≥ ε/2}.
- The bound is symmetric because D^m ⊗ D^m is symmetric under swapping factors. have swap_symmetry : DoubleSampleMeasure D m {p | ∃ h ∈ C, EmpErr(S) - EmpErr(S') ≥ ε/2} = DoubleSampleMeasure D m {p | ∃ h ∈ C, EmpErr(S') - EmpErr(S) ≥ ε/2} := Measure.prod_swap ...
4. Union bound: P[|gap| ≥ ε] ≤ P[gap ≥ ε] + P[gap ≤ -ε] ≤ 2·GF·exp(...) + 2·GF·exp(...) = 4·GF(C,2m)·exp(-mε²/8)
-- Uses: MeasureTheory.measure_union_le for the union of two events -- CAST: 2 * X + 2 * X = 4 * X in ENNReal (need ENNReal.add_mul or similar)
References: SSBD Theorem 6.7, Kakade-Tewari Lecture 19
```
∀ {X : Type u} [inst : MeasurableSpace X] [Infinite X] (D : MeasureTheory.Measure X)
  [MeasureTheory.IsProbabilityMeasure D] (C : ConceptClass X Bool) (c : Concept X Bool),
  (∀ h ∈ C, Measurable h) →
    Measurable c →
      ∀ (m : ℕ),
        0 < m →
          ∀ (ε : ℝ),
            0 < ε →
              2 * Real.log 2 ≤ ↑m * ε ^ 2 →
                MeasureTheory.NullMeasurableSet
                    {p |
                      ∃ h ∈ C,
                        EmpiricalError X Bool h (fun i => (p.2 i, c (p.2 i))) (zeroOneLoss Bool) -
                            EmpiricalError X Bool h (fun i => (p.1 i, c (p.1 i))) (zeroOneLoss Bool) ≥
                          ε / 2}
                    ((MeasureTheory.Measure.pi fun x => D).prod (MeasureTheory.Measure.pi fun x => D)) →
                  (MeasureTheory.Measure.pi fun x => D)
                      {xs |
                        ∃ h ∈ C,
                          |TrueErrorReal X h c D -
                                EmpiricalError X Bool h (fun i => (xs i, c (xs i))) (zeroOneLoss Bool)| ≥
                            ε} ≤
                    ENNReal.ofReal (4 * ↑(GrowthFunction X C (2 * m)) * Real.exp (-(↑m * ε ^ 2 / 8)))
```
ConceptClass EmpiricalError FLT.Concept GrowthFunction TrueErrorReal zeroOneLoss
Uses
Used by
- finite_support_vc_approx

Declsymmetrization_step_lowerDeclaration kindtheorem

Symmetrization step for the lower tail: P[∃h: EmpErr-TrueErr ≥ ε] ≤ 2·P_{double}[∃h: EmpErr_S-EmpErr_{S'} ≥ ε/2].

Mirror of symmetrization_step for the opposite direction. Uses hoeffding_one_sided_upper instead of hoeffding_one_sided.

∀ {X : Type u} [inst : MeasurableSpace X] (D : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure D]
  (C : ConceptClass X Bool) (c : Concept X Bool),
  (∀ h ∈ C, Measurable h) →
    Measurable c →
      ∀ (m : ℕ),
        0 < m →
          ∀ (ε : ℝ),
            0 < ε →
              2 * Real.log 2 ≤ ↑m * ε ^ 2 →
                (MeasureTheory.Measure.pi fun x => D)
                    {xs |
                      ∃ h ∈ C,
                        EmpiricalError X Bool h (fun i => (xs i, c (xs i))) (zeroOneLoss Bool) - TrueErrorReal X h c D ≥
                          ε} ≤
                  2 *
                    ((MeasureTheory.Measure.pi fun x => D).prod (MeasureTheory.Measure.pi fun x => D))
                      {p |
                        ∃ h ∈ C,
                          EmpiricalError X Bool h (fun i => (p.1 i, c (p.1 i))) (zeroOneLoss Bool) -
                              EmpiricalError X Bool h (fun i => (p.2 i, c (p.2 i))) (zeroOneLoss Bool) ≥
                            ε / 2}

ConceptClass EmpiricalError FLT.Concept TrueErrorReal zeroOneLoss

Uses

hoeffding_one_sided_upper

Used by

symmetrization_uc_bound

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))

EmpiricalError FLT.Concept TrueErrorReal zeroOneLoss

Used by

symmetrization_step_lower

Declsymmetrization_stepDeclaration kindtheorem
Symmetrization: the probability of a large gap TrueErr-EmpErr is at most twice the probability of a large gap EmpErr'-EmpErr on the double sample.
Proof strategy (6 steps):
1. Witness selection: For S in the bad event, ∃h* ∈ C with TrueErr(h) - EmpErr_S(h) ≥ ε.
-- In the bad event set, extract h* by classical choice have h_witness : ∀ xs ∈ bad_event, ∃ h* ∈ C, TrueErrorReal X h* c D - EmpiricalError X Bool h* (sample xs) (zeroOneLoss Bool) ≥ ε
2. Ghost sample mean: E_{S'}[EmpErr_{S'}(h)] = TrueErr(h) ≥ EmpErr_S(h*) + ε.
- Uses: MeasureTheory.integral_pi to compute E[EmpErr] over product measure.
- KEY LEMMA: For fixed h, E_{D^m}[EmpiricalError(h,S)] = TrueErrorReal(h,c,D). This is because EmpErr = (1/m)∑ indicator(x_i), and E[indicator(x_i)] = TrueErrorReal. have expected_emp_err : ∀ h* : Concept X Bool, ∫ xs, EmpiricalError X Bool h* (sample xs) (zeroOneLoss Bool) ∂(Measure.pi (fun _ : Fin m => D)) = TrueErrorReal X h* c D := by ...
3. Hoeffding on ghost sample: P_{S'}[EmpErr_{S'}(h) < TrueErr(h) - ε/2] ≤ exp(-mε²/2).
- Apply hoeffding_one_sided with t = ε/2.
- The hm_large hypothesis ensures exp(-mε²/2) < 1/2: 2·ln2 ≤ mε² ⟹ mε²/2 ≥ ln2 ⟹ exp(-mε²/2) ≤ 1/2. have hoeffding_ghost : ∀ h* ∈ C, Measure.pi (fun _ : Fin m => D) {xs' | EmpiricalError X Bool h* (sample xs') (zeroOneLoss Bool) < TrueErrorReal X h* c D - ε/2} ≤ ENNReal.ofReal (Real.exp (-m * (ε/2)^2 * 2)) := by intro h* _; exact hoeffding_one_sided D h* c m hm (ε/2) (by linarith) (by ...) (by ...)
4. Complementary probability: P_{S'}[EmpErr_{S'}(h) - EmpErr_S(h) ≥ ε/2] ≥ 1/2.
- From step 2: TrueErr(h) ≥ EmpErr_S(h) + ε
- From step 3: P[EmpErr_{S'} ≥ TrueErr - ε/2] ≥ 1/2
- Chain: EmpErr_{S'} ≥ TrueErr - ε/2 ≥ EmpErr_S + ε - ε/2 = EmpErr_S + ε/2
5. Conditional to unconditional: The witness h* from step 1 also witnesses the double-sample event ∃h∈C: EmpErr'-EmpErr ≥ ε/2. So: P_{S'}[double event | S bad] ≥ 1/2.
have conditional_bound : ∀ xs ∈ bad_event, Measure.pi (fun _ : Fin m => D) {xs' | ∃ h ∈ C, EmpiricalError ... xs' - EmpiricalError ... xs ≥ ε/2} ≥ ENNReal.ofReal (1/2) := by ...
6. Fubini integration: By Measure.prod_apply and Fubini: P_{S,S'}[double event] = ∫_S P_{S'}[double event | S] ≥ (1/2) · P_S[bad event] ⟹ P_S[bad event] ≤ 2 · P_{S,S'}[double event].
-- Uses: MeasureTheory.Measure.prod_apply or lintegral_prod -- MEASURABILITY: the double-sample event is measurable as a finite union -- of sets of the form {(xs,xs') | EmpErr'(h) - EmpErr(h) ≥ ε/2} for h ∈ C. -- Since C may be infinite, measurability requires care: the sup over h -- must be shown to be measurable. For finite restriction patterns (≤ 2^m -- on Fin m → Bool), this is a finite union.
MEASURABILITY CONCERNS:
- {xs | ∃ h ∈ C, ...} is NOT obviously measurable for infinite C. Strategy: decompose via restriction patterns. On any fixed xs, the set of labelings {(h(xs 0), ..., h(xs(m-1))) | h ∈ C} has at most GF(C,m) ≤ 2^m elements. So the ∃h event is a finite union of measurable sets.
- EmpiricalError is a finite sum of measurable functions, hence measurable.
- The product σ-algebra on (Fin m → X) × (Fin m → X) is generated by cylinder sets, and our events are in this σ-algebra.
References: SSBD Lemma 4.5, Kakade-Tewari Lecture 19 Lemma 1
```
∀ {X : Type u} [inst : MeasurableSpace X] (D : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure D]
  (C : ConceptClass X Bool) (c : Concept X Bool),
  (∀ h ∈ C, Measurable h) →
    Measurable c →
      ∀ (m : ℕ),
        0 < m →
          ∀ (ε : ℝ),
            0 < ε →
              2 * Real.log 2 ≤ ↑m * ε ^ 2 →
                (MeasureTheory.Measure.pi fun x => D)
                    {xs |
                      ∃ h ∈ C,
                        TrueErrorReal X h c D - EmpiricalError X Bool h (fun i => (xs i, c (xs i))) (zeroOneLoss Bool) ≥
                          ε} ≤
                  2 *
                    ((MeasureTheory.Measure.pi fun x => D).prod (MeasureTheory.Measure.pi fun x => D))
                      {p |
                        ∃ h ∈ C,
                          EmpiricalError X Bool h (fun i => (p.2 i, c (p.2 i))) (zeroOneLoss Bool) -
                              EmpiricalError X Bool h (fun i => (p.1 i, c (p.1 i))) (zeroOneLoss Bool) ≥
                            ε / 2}
```
ConceptClass EmpiricalError FLT.Concept TrueErrorReal zeroOneLoss
Uses
- hoeffding_one_sided
Used by
- symmetrization_uc_bound
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_half infrastructure 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.pi independence structure.
- Needs: Measure.pi integral 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 : ℝ)
- EmpiricalError returns ℝ, TrueErrorReal returns ℝ, good — no ENNReal gap
- The measure value is ENNReal, the bound exp(-2mt²) is ℝ≥0∞ via ENNReal.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))
```
EmpiricalError FLT.Concept TrueErrorReal zeroOneLoss
Used by
- symmetrization_step
Decldouble_sample_pattern_boundDeclaration kindtheorem
On the double sample, the probability that any hypothesis has EmpErr' - EmpErr ≥ ε/2 is bounded by GF(C,2m) · exp(-mε²/8).
Proof strategy (Approach A — standard exchangeability, 5 steps):
1. EXCHANGEABILITY: Under D^m ⊗ D^m, the 2m draws z₁,...,z_{2m} are iid from D. The joint distribution is invariant under permutations of {1,...,2m}.
Key lemma: P_{D^m⊗D^m}[event(S,S')] = E_z[P_{split}[event | z]] where z = merged sample and the split is uniformly random among all C(2m,m) ways to partition z into two groups of m.
-- Measure.pi permutation invariance have pi_perm_invariant : ∀ (σ : Equiv.Perm (Fin (2*m))), (Measure.pi (fun _ : Fin (2*m) => D)).map (fun z i => z (σ i)) = Measure.pi (fun _ : Fin (2*m) => D) := by ... -- Consequence: the event probability equals the split-averaged probability have exchangeability : DoubleSampleMeasure D m {p | ∃ h ∈ C, gap(p) ≥ ε/2} = ∫ z, SplitMeasure m {vs | ∃ h ∈ C, gap(split z vs) ≥ ε/2} ∂(Measure.pi (fun _ : Fin (2*m) => D)) := by ...
2. CONDITIONING: For fixed merged sample z of 2m points:
- C restricts to at most GF(C,2m) distinct labeling patterns on z (deterministic).
- For each pattern p, define: diff(p, split) = EmpErr_{S'}(p) - EmpErr_S(p) = (1/m) ∑_{i∈S'} a_i - (1/m) ∑_{i∈S} a_i where a_i = 1[pattern(z_i) ≠ c(z_i)] ∈ {0,1}.
-- Number of distinct patterns have num_patterns : ∀ (z : MergedSample X m), Set.ncard {p : Fin (2*m) → Bool | ∃ h ∈ C, ∀ i, p i = (h (z i) ≠ c (z i))} ≤ GrowthFunction X C (2*m) := by ...
3. PER-PATTERN HOEFFDING ON SPLITS: For fixed z and fixed pattern p: Under uniformly random split (S,S') of z into two groups of m: diff(p, split) = (1/m) ∑_{i∈S'} a_i - (1/m) ∑_{i∈S} a_i
This is a function of the random partition. By Hoeffding's inequality for sampling without replacement (Serfling 1974): P_split[diff ≥ ε/2] ≤ exp(-mε²/8)
Alternative derivation: Hoeffding without replacement from Hoeffding with replacement (iid signs) via coupling. The without-replacement bound is actually TIGHTER (variance reduction), but the with-replacement bound suffices.
-- Per-pattern concentration have per_pattern_bound : ∀ (z : MergedSample X m) (a : Fin (2*m) → ℝ) (ha : ∀ i, a i ∈ Set.Icc 0 1), SplitMeasure m {vs | (1/m) * ∑ i ∈ second_group vs, a i - (1/m) * ∑ i ∈ first_group vs, a i ≥ ε/2} ≤ ENNReal.ofReal (Real.exp (-(m : ℝ) * (ε/2)^2 / 2)) := by ... -- Note: m*(ε/2)^2/2 = mε²/8
4. UNION BOUND: P_split[∃ pattern: diff ≥ ε/2 | z] ≤ (number of patterns) · max_pattern P_split[diff ≥ ε/2] ≤ GF(C,2m) · exp(-mε²/8)
have union_bound : ∀ (z : MergedSample X m), SplitMeasure m {vs | ∃ h ∈ C, gap(split z vs, h) ≥ ε/2} ≤ ENNReal.ofReal (GrowthFunction X C (2*m) * Real.exp (-(m : ℝ) * ε^2 / 8)) := by ...
5. INTEGRATE: P_{D^m⊗D^m}[event] = E_z[P_split[event|z]] (by step 1) ≤ E_z[GF(C,2m) · exp(-mε²/8)] (by step 4, pointwise) = GF(C,2m) · exp(-mε²/8) (bound is independent of z)
-- The bound is a constant, so integrating gives the same constant -- (using IsProbabilityMeasure for the 2m-fold product)
Infrastructure needed:
- Fin.sumFinEquiv : Fin m ⊕ Fin n ≃ Fin (m + n) (available in Mathlib)
- mergeSamples / splitMergedSample (defined above)
- SplitMeasure and ValidSplit (defined above)
- Measure.pi permutation invariance (to be proved or imported)
- Hoeffding for sampling without replacement
- GrowthFunction on 2m points + sauer_shelah_exp_bound from Rademacher.lean
MEASURABILITY CONCERNS:
- The merged sample z ↦ P_split[event|z] must be measurable as a function of z. Since the event is a finite union over patterns, and each pattern's indicator is a measurable function of z (finite evaluation), this follows.
- GrowthFunction X C (2*m) is a natural number (deterministic), no measurability issue.
References: SSBD Theorem 6.7, Hoeffding (1963), Serfling (1974)
```
∀ {X : Type u} [inst : MeasurableSpace X] [Infinite X] (D : MeasureTheory.Measure X)
  [MeasureTheory.IsProbabilityMeasure D] (C : ConceptClass X Bool) (c : Concept X Bool),
  (∀ h ∈ C, Measurable h) →
    Measurable c →
      ∀ (m : ℕ),
        0 < m →
          ∀ (ε : ℝ),
            0 < ε →
              MeasureTheory.NullMeasurableSet
                  {p |
                    ∃ h ∈ C,
                      EmpiricalError X Bool h (fun i => (p.2 i, c (p.2 i))) (zeroOneLoss Bool) -
                          EmpiricalError X Bool h (fun i => (p.1 i, c (p.1 i))) (zeroOneLoss Bool) ≥
                        ε / 2}
                  ((MeasureTheory.Measure.pi fun x => D).prod (MeasureTheory.Measure.pi fun x => D)) →
                ((MeasureTheory.Measure.pi fun x => D).prod (MeasureTheory.Measure.pi fun x => D))
                    {p |
                      ∃ h ∈ C,
                        EmpiricalError X Bool h (fun i => (p.2 i, c (p.2 i))) (zeroOneLoss Bool) -
                            EmpiricalError X Bool h (fun i => (p.1 i, c (p.1 i))) (zeroOneLoss Bool) ≥
                          ε / 2} ≤
                  ENNReal.ofReal (↑(GrowthFunction X C (2 * m)) * Real.exp (-(↑m * ε ^ 2 / 8)))
```
ConceptClass EmpiricalError FLT.Concept GrowthFunction zeroOneLoss
Uses
- exchangeability_chain_bound
Used by
- symmetrization_uc_bound

Declexchangeability_chain_boundDeclaration kindtheorem

∀ {X : Type u} [inst : MeasurableSpace X] [Infinite X] (D : MeasureTheory.Measure X)
  [MeasureTheory.IsProbabilityMeasure D] (C : ConceptClass X Bool) (c : Concept X Bool),
  (∀ h ∈ C, Measurable h) →
    Measurable c →
      ∀ (m : ℕ),
        0 < m →
          ∀ (ε : ℝ),
            0 < ε →
              ε ≤ 2 →
                Set.Nonempty C →
                  MeasureTheory.NullMeasurableSet
                      {p |
                        ∃ h ∈ C,
                          EmpiricalError X Bool h (fun i => (p.2 i, c (p.2 i))) (zeroOneLoss Bool) -
                              EmpiricalError X Bool h (fun i => (p.1 i, c (p.1 i))) (zeroOneLoss Bool) ≥
                            ε / 2}
                      ((MeasureTheory.Measure.pi fun x => D).prod (MeasureTheory.Measure.pi fun x => D)) →
                    have μ := MeasureTheory.Measure.pi fun x => D;
                    (μ.prod μ)
                        {p |
                          ∃ h ∈ C,
                            EmpiricalError X Bool h (fun i => (p.2 i, c (p.2 i))) (zeroOneLoss Bool) -
                                EmpiricalError X Bool h (fun i => (p.1 i, c (p.1 i))) (zeroOneLoss Bool) ≥
                              ε / 2} ≤
                      ENNReal.ofReal (↑(GrowthFunction X C (2 * m)) * Real.exp (-(↑m * ε ^ 2 / 8)))

ConceptClass EmpiricalError FLT.Concept GrowthFunction SignVector boolToSign zeroOneLoss

Uses

finite_exchangeability_bound
rademacher_mgf_bound
restriction_pattern_count
zeroOneLoss.congr_simp

Used by

double_sample_pattern_bound

DeclzeroOneLoss.congr_simpDeclaration kindtheorem

∀ (Y : Type v) {inst : DecidableEq Y} [inst_1 : DecidableEq Y] (a a_1 : Y),
  a = a_1 → ∀ (a_2 a_3 : Y), a_2 = a_3 → zeroOneLoss Y a a_2 = zeroOneLoss Y a_1 a_3

zeroOneLoss

Used by

exchangeability_chain_bound

Declrestriction_pattern_countDeclaration kindtheorem
The number of distinct restriction patterns of C on any n points is at most GF(C,n). For z : Fin n → X, define patterns(z) = {p : Fin n → Bool | ∃ h ∈ C, ∀ i, p i = (h(z i) ≠ c(z i))}. Then patterns(z).ncard ≤ GrowthFunction X C n by definition of GrowthFunction.
```
∀ {X : Type u} [MeasurableSpace X] [Infinite X] (C : ConceptClass X Bool) (c : Concept X Bool) (n : ℕ) (z : Fin n → X),
  {p | ∃ h ∈ C, ∀ (i : Fin n), p i = decide (h (z i) ≠ c (z i))}.ncard ≤ GrowthFunction X C n
```
ConceptClass FLT.Concept GrowthFunction
Used by
- exchangeability_chain_bound

Declrademacher_mgf_boundDeclaration kindtheorem

Rademacher MGF bound.

∀ {m : ℕ},
  0 < m →
    ∀ (a : Fin m → ℝ) (c : ℝ),
      0 ≤ c →
        (∀ (i : Fin m), |a i| ≤ c) →
          ∀ (t : ℝ),
            0 ≤ t →
              1 / ↑(Fintype.card (SignVector m)) * ∑ σ, Real.exp (t * (1 / ↑m * ∑ i, a i * boolToSign (σ i))) ≤
                Real.exp (t ^ 2 * c ^ 2 / (2 * ↑m))

SignVector boolToSign

Uses

cosh_le_exp_sq_half

Used by

exchangeability_chain_bound

Declcosh_le_exp_sq_halfDeclaration kindtheorem
cosh(x) ≤ exp(x²/2). Standard sub-Gaussian bound.
```
∀ (x : ℝ), Real.cosh x ≤ Real.exp (x ^ 2 / 2)
```
Used by
- rademacher_mgf_bound

Declfinite_exchangeability_boundDeclaration kindtheorem

Generic finite exchangeability bound. Given a measure-preserving family of transformations on a probability space, a NullMeasurableSet S, and a pointwise bound on the sum of preimage indicators, conclude ν(S) ≤ B.

∀ {Ω : Type u_1} {G : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : Fintype G] [Nonempty G]
  {ν : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure ν] (T : G → Ω → Ω) (S : Set Ω),
  (∀ (g : G), MeasureTheory.MeasurePreserving (T g) ν ν) →
    MeasureTheory.NullMeasurableSet S ν →
      ∀ (B : ENNReal), (∀ (z : Ω), ∑ g, (T g ⁻¹' S).indicator 1 z ≤ B * ↑(Fintype.card G)) → ν S ≤ B

Used by

exchangeability_chain_bound

Declgrowth_exp_le_deltaDeclaration kindtheorem

∀ {X : Type u} [MeasurableSpace X] (C : ConceptClass X Bool) (v : ℕ),
  0 < v →
    ∀ (m : ℕ),
      0 < m →
        ∀ (ε δ : ℝ),
          0 < ε →
            0 < δ →
              δ < 1 →
                (∀ (n : ℕ), v ≤ n → GrowthFunction X C n ≤ ∑ i ∈ Finset.range (v + 1), n.choose i) →
                  (16 * Real.exp 1 * (↑v + 1) / ε ^ 2) ^ (v + 1) / δ ≤ ↑m →
                    4 * ↑(GrowthFunction X C (2 * m)) * Real.exp (-(↑m * ε ^ 2 / 8)) ≤ δ ∧ 2 * Real.log 2 ≤ ↑m * ε ^ 2

ConceptClass GrowthFunction

Uses

growth_function_le_two_pow
pow_mul_exp_neg_le_factorial_div
sum_choose_le_exp_pow

Used by

finite_support_vc_approx

Declsum_choose_le_exp_powDeclaration kindtheorem
Pure combinatorial inequality: ∑_{i=0}^d C(m,i) ≤ (em/d)^d for d ≤ m, d ≥ 1.
```
∀ (d m : ℕ), 0 < d → d ≤ m → ∑ i ∈ Finset.range (d + 1), ↑(m.choose i) ≤ (Real.exp 1 * ↑m / ↑d) ^ d
```
Used by
- growth_exp_le_delta
Declpow_mul_exp_neg_le_factorial_divDeclaration kindtheorem
Key arithmetic lemma for PAC bound: for t > 0, t^d * exp(-t) ≤ (d+1)!/t. Follows from exp(t) ≥ t^(d+1)/(d+1)! (partial sum of Taylor series).
```
∀ {d : ℕ} {t : ℝ}, 0 < t → t ^ d * Real.exp (-t) ≤ ↑(d + 1).factorial / t
```
Used by
- growth_exp_le_delta
Declgrowth_function_le_two_powDeclaration kindtheorem
Trivial bound: GrowthFunction ≤ 2^n for all concept classes. Each restriction to an n-element set yields a function in S → Bool, and there are at most 2^n such functions.
```
∀ {X : Type u} (C : ConceptClass X Bool) (n : ℕ), GrowthFunction X C n ≤ 2 ^ n
```
ConceptClass FLT.Concept GrowthFunction
Used by
- growth_exp_le_delta
DeclboolTestExpectation_nonnegDeclaration kindtheorem
A convex combination of values in {0, 1} is nonnegative.
```
∀ {H : Type u_1} [inst : Fintype H] (μ : FinitePMF H) (f : H → Bool), 0 ≤ boolTestExpectation μ f
```
FinitePMF FinitePMF.prob boolTestExpectation
Uses
- FinitePMF.prob_nonneg
Used by
- finite_support_vc_approx
DeclboolTestExpectation_le_oneDeclaration kindtheorem
A convex combination of values in {0, 1} is at most 1.
```
∀ {H : Type u_1} [inst : Fintype H] (μ : FinitePMF H) (f : H → Bool), boolTestExpectation μ f ≤ 1
```
FinitePMF FinitePMF.prob boolTestExpectation
Uses
- FinitePMF.prob_nonneg
- FinitePMF.prob_sum_one
Used by
- finite_support_vc_approx
DeclFinitePMF.prob_nonnegDeclaration kindtheorem
```
∀ {H : Type u_1} [inst : Fintype H] (self : FinitePMF H) (h : H), 0 ≤ self.prob h
```
FinitePMF FinitePMF.prob
Used by
DeclFinitePMF.prob_sum_oneDeclaration kindtheorem
```
∀ {H : Type u_1} [inst : Fintype H] (self : FinitePMF H), ∑ h, self.prob h = 1
```
FinitePMF FinitePMF.prob
Used by

DeclfinalizeIncidenceSchemeDeclaration kindtheorem

Final existential wrapper: closes the theorem in the exact form expected.

∀ {X : Type u} {C : ConceptClass X Bool} (T K : ℕ)
  (compressCore : {m : ℕ} → (Fin m → X × Bool) → Finset (X × Bool) × IncidenceInfo T K)
  (blockHyp : Finset (X × Bool) → IncidenceInfo T K → Fin T → X → Bool)
  (rowHyp : {m : ℕ} → (S : Fin m → X × Bool) → (∃ c ∈ C, ∀ (i : Fin m), c (S i).1 = (S i).2) → Fin T → X → Bool),
  0 < T →
    (∀ {m : ℕ} (S : Fin m → X × Bool), (compressCore S).1.card ≤ K) →
      (∀ {m : ℕ} (S : Fin m → X × Bool), ↑(compressCore S).1 ⊆ Set.range S) →
        (∀ {m : ℕ} (S : Fin m → X × Bool) (hreal : ∃ c ∈ C, ∀ (i : Fin m), c (S i).1 = (S i).2) (i : Fin m) (t : Fin T),
            blockHyp (compressCore S).1 (compressCore S).2 t (S i).1 = rowHyp S hreal t (S i).1) →
          (∀ {m : ℕ} (S : Fin m → X × Bool) (hreal : ∃ c ∈ C, ∀ (i : Fin m), c (S i).1 = (S i).2) (i : Fin m),
              (∑ t, if rowHyp S hreal t (S i).1 = (S i).2 then 1 else 0) / ↑T > 1 / 2) →
            ∃ k cs, CompressionSchemeWithInfo.size cs = k

CompressionSchemeWithInfo.size CompressionSchemeWithInfo0 ConceptClass FLT.Concept IncidenceInfo mkIncidenceSchemeOfMajority

Used by

moran_yehudayoff_forward_construction

DeclencodeWitnessInfo.congr_simpDeclaration kindtheorem

∀ {X : Type u} {inst : DecidableEq X} [inst_1 : DecidableEq X] (kernel kernel_1 : Finset (X × Bool)),
  kernel = kernel_1 →
    ∀ (c c_1 : X → Bool),
      c = c_1 →
        ∀ (K : ℕ) (W W_1 : Finset X), W = W_1 → encodeWitnessInfo kernel c K W = encodeWitnessInfo kernel_1 c_1 K W_1

encodeWitnessInfo

Used by

moran_yehudayoff_forward_construction

DeclboolTestExpectation_empirical_eq_avgDeclaration kindtheorem
Bridges the FinitePMF view and the sample-average view: the expectation of a Bool-valued test under the empirical PMF of a sample equals the sample average (1/T) ∑_t f (s_t). This lets the MWU updates and the approximation transfer principle live in the same distributional framework.
```
∀ {H : Type u_1} [inst : Fintype H] [inst_1 : DecidableEq H] {T : ℕ} (hT : 0 < T) (hs : Fin T → H) (f : H → Bool),
  boolTestExpectation (empiricalPMF hT hs) f = (∑ t, if f (hs t) = true then 1 else 0) / ↑T
```
FinitePMF.prob boolTestExpectation empiricalPMF
Used by
DeclboolGamePayoff_eq_boolTestExpectationDeclaration kindtheorem
Identifies the game-theoretic payoff (a row distribution against a fixed column in the Bool game) with the corresponding test expectation. The translation that lets the MWU regret bound be applied directly to the compression problem.
```
∀ {R : Type u_1} [inst : Fintype R] [DecidableEq R] {C : Type u_2} (M : R → C → Bool) (p : FinitePMF R) (c : C),
  boolGamePayoff M p c = boolTestExpectation p fun r => M r c
```
FinitePMF FinitePMF.prob boolGamePayoff boolTestExpectation
Used by
- moran_yehudayoff_forward_construction
DeclagreeTests_boolVCDim_leDeclaration kindtheorem
VC dimension of the agreement-test family is bounded by 2^(d+1) - 1, where d bounds the VC dimension of the concept class C. Uses Assouad's coding argument directly: if a shattered set T in ↥HY has |T| ≥ 2^(d+1), embed bitstrings into T, extract d+1 distinct points from Y via shattering, and show these points are shattered by C (using the XOR trick where b(j) = decide(g(x_j) = c(x_j)) absorbs the agree/disagree flip).
```
∀ {X : Type u} [DecidableEq X] (C : ConceptClass X Bool) (c : X → Bool) (Y : Finset X) (HY : Finset (X → Bool)),
  (∀ h ∈ HY, h ∈ C) → ∀ {d : ℕ}, VCDim X C ≤ ↑d → (agreeTests c Y HY).boolVCDim ≤ 2 ^ (d + 1) - 1
```
ConceptClass FLT.Concept Finset.boolVCDim Shatters VCDim agreeTest agreeTests boolFamilyToFinsetFamily
Used by
- moran_yehudayoff_forward_construction
Declcompression_with_info_imp_vcdim_finiteDeclaration kindtheorem
Compression with side info implies finite VC dimension. Proof by pigeonhole: compress is injective on C-realizable labelings (by correctness), but compressed outputs form a bounded set.
```
∀ (X : Type u) (C : ConceptClass X Bool), (∃ k cs, cs.size = k) → VCDim X C < ⊤
```
CompressionSchemeWithInfo CompressionSchemeWithInfo.Info CompressionSchemeWithInfo.compress CompressionSchemeWithInfo.info_finite CompressionSchemeWithInfo.kernelSize CompressionSchemeWithInfo.size ConceptClass FLT.Concept Shatters VCDim
Uses
Used by
- fundamental_vc_compression_with_info
Declshatters_subset_compressionDeclaration kindtheorem
```
∀ {X : Type u} {C : ConceptClass X Bool} {S T : Finset X}, T ⊆ S → Shatters X C S → Shatters X C T
```
ConceptClass FLT.Concept Shatters
Used by
- compression_with_info_imp_vcdim_finite
Declexp_beats_poly_compressionDeclaration kindtheorem
Exponential beats polynomial for the compression pigeonhole argument.
```
∀ (s : ℕ), (s + 1) ^ 2 * (4 * (s + 1) ^ 2) ^ s < 2 ^ (2 * (s + 1) * (s + 1))
```
Uses
- succ_le_two_pow_compression
Used by
- compression_with_info_imp_vcdim_finite
Declsucc_le_two_pow_compressionDeclaration kindtheorem
```
∀ (k : ℕ), k + 1 ≤ 2 ^ k
```
Used by
- exp_beats_poly_compression
Declcompress_with_info_injective_on_labelingsDeclaration kindtheorem
Pigeonhole core: if two C-realizable samples over the same points with different labelings produce the same (kernel, info) pair, correctness forces the labelings to agree.
```
∀ {X : Type u} {n : ℕ} {C : ConceptClass X Bool} (cs : CompressionSchemeWithInfo X Bool C) (pts : Fin n → X),
  Function.Injective pts →
    ∀ (f g : Fin n → Bool),
      (∃ c ∈ C, ∀ (i : Fin n), c (pts i) = f i) →
        (∃ c ∈ C, ∀ (i : Fin n), c (pts i) = g i) →
          ((cs.compress fun i => (pts i, f i)) = cs.compress fun i => (pts i, g i)) → f = g
```
CompressionSchemeWithInfo CompressionSchemeWithInfo.Info CompressionSchemeWithInfo.compress CompressionSchemeWithInfo.reconstruct ConceptClass FLT.Concept
Uses
- CompressionSchemeWithInfo.correct
Used by
- compression_with_info_imp_vcdim_finite
DeclCompressionSchemeWithInfo.correctDeclaration kindtheorem
Correctness: reconstructed hypothesis agrees with every sample point, when the sample is C-realizable
```
∀ {X : Type u} {Y : Type v} {C : ConceptClass X Y} (self : CompressionSchemeWithInfo X Y C) {m : ℕ} (S : Fin m → X × Y),
  (∃ c ∈ C, ∀ (i : Fin m), c (S i).1 = (S i).2) →
    ∀ (i : Fin m), self.reconstruct (self.compress S).1 (self.compress S).2 (S i).1 = (S i).2
```
CompressionSchemeWithInfo CompressionSchemeWithInfo.Info CompressionSchemeWithInfo.compress CompressionSchemeWithInfo.reconstruct ConceptClass FLT.Concept
Used by
- compress_with_info_injective_on_labelings
DeclCompressionSchemeWithInfo.compress_subDeclaration kindtheorem
Compressed set is a subset of the sample
```
∀ {X : Type u} {Y : Type v} {C : ConceptClass X Y} (self : CompressionSchemeWithInfo X Y C) {m : ℕ} (S : Fin m → X × Y),
  ↑(self.compress S).1 ⊆ Set.range S
```
CompressionSchemeWithInfo CompressionSchemeWithInfo.Info CompressionSchemeWithInfo.compress ConceptClass
Used by
- compression_with_info_imp_vcdim_finite
DeclCompressionSchemeWithInfo.compress_smallDeclaration kindtheorem
Compressed set is small
```
∀ {X : Type u} {Y : Type v} {C : ConceptClass X Y} (self : CompressionSchemeWithInfo X Y C) {m : ℕ} (S : Fin m → X × Y),
  (self.compress S).1.card ≤ self.kernelSize
```
CompressionSchemeWithInfo CompressionSchemeWithInfo.Info CompressionSchemeWithInfo.compress CompressionSchemeWithInfo.kernelSize ConceptClass
Used by
- compression_with_info_imp_vcdim_finite
DefinitionCompressionSchemeWithInfostructure
A labeled compression scheme with finite side information. This is the object proved to exist by Moran-Yehudayoff (2016, arXiv:1503.06960).
The current CompressionScheme is strictly stronger: it requires reconstruction from the compressed Finset alone (no side information). See Open_NoInfoCompressionStrengthening for that conjecture.
```
(X : Type u) → (Y : Type v) → ConceptClass X Y → Type (max (max u (u_1 + 1)) v)
```

DefinitionCompressionSchemeWithInfo.Infodef

The side information type

{X : Type u} → {Y : Type v} → {C : ConceptClass X Y} → CompressionSchemeWithInfo X Y C → Type u_1

DefinitionCompressionSchemeWithInfo.compressdef

Compression: extract ≤ kernelSize labeled examples + side information

{X : Type u} →
  {Y : Type v} →
    {C : ConceptClass X Y} →
      (self : CompressionSchemeWithInfo X Y C) → {m : ℕ} → (Fin m → X × Y) → Finset (X × Y) × self.Info

DefinitionCompressionSchemeWithInfo.info_finitedef

Side information is finite

{X : Type u} → {Y : Type v} → {C : ConceptClass X Y} → (self : CompressionSchemeWithInfo X Y C) → Fintype self.Info

DefinitionCompressionSchemeWithInfo.kernelSizedef

Kernel size bound

{X : Type u} → {Y : Type v} → {C : ConceptClass X Y} → CompressionSchemeWithInfo X Y C → ℕ

DefinitionCompressionSchemeWithInfo.reconstructdef

Reconstruction: produce hypothesis from compressed subset AND side information

{X : Type u} →
  {Y : Type v} → {C : ConceptClass X Y} → (self : CompressionSchemeWithInfo X Y C) → Finset (X × Y) → self.Info → X → Y

DefinitionCompressionSchemeWithInfo.sizedef
Total size of a compression scheme with side information: kernel size + number of side information states. (The paper uses k + log₂(|I|+1); we use the simpler k + |I| which is an upper bound and avoids importing Real.log.)
```
{X : Type u} → {Y : Type v} → {C : ConceptClass X Y} → CompressionSchemeWithInfo X Y C → ℕ
```
DefinitionCompressionSchemeWithInfo0def
Fix the hidden Info universe parameter of CompressionSchemeWithInfo to 0. This resolves the universe elaboration obstruction: Fin T → Finset (Fin K) is Type 0, while CompressionSchemeWithInfo X Bool C with X : Type u infers Info : Type u. Pinning to .{u, 0, 0} allows Type 0 Info directly.
```
(X : Type u) → (Y : Type) → ConceptClass X Y → Type (max (max u 1) 0)
```
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)
```
DefinitionFinitePMFstructure
A probability mass function over a finite type. Named FinitePMF to avoid conflict with Mathlib's PMF.
```
(H : Type u_1) → [Fintype H] → Type u_1
```

DefinitionFinitePMF.probdef

{H : Type u_1} → [inst : Fintype H] → FinitePMF H → H → ℝ

DefinitionFinitePMF.toPMFdef

{H : Type u_1} → [inst : Fintype H] → FinitePMF H → PMF H

DefinitionFinset.boolVCDimdef
VC dimension of a finite Bool-valued family, computed via the set-system image boolFamilyToFinsetFamily and Mathlib's Finset.vcDim. Declared noncomputable because the underlying vcDim is.
```
{H : Type u_1} → [Fintype H] → [DecidableEq H] → Finset (H → Bool) → ℕ
```
DefinitionGrowthFunctiondef
Growth function (shattering coefficient): π_C(m) = max_{|S|=m} |{c|_S : c ∈ C}|. For each m-element set S, counts the number of distinct restrictions of C to S, then takes the supremum over all such S.
```
(X : Type u) → ConceptClass X Bool → ℕ → ℕ
```
DefinitionIncidenceInfodef
Concrete side information for the MY construction: each of the T recovered blocks is represented by the set of kernel positions it uses.
```
ℕ → ℕ → Type
```
DefinitionMWUConfigstructure
MWU config: weight vector with positivity proof.
```
(C : Type u_1) → [Fintype C] → Type u_1
```

DefinitionMWUConfig.potentialdef

Potential = sum of weights.

{C : Type u_1} → [inst : Fintype C] → MWUConfig C → ℝ

DefinitionMWUConfig.toPMFdef

Normalize config to PMF.

{C : Type u_1} → [inst : Fintype C] → [Nonempty C] → MWUConfig C → FinitePMF C

DefinitionMWUConfig.weightsdef

{C : Type u_1} → [inst : Fintype C] → MWUConfig C → C → ℝ

DefinitionProperFiniteSupportLearnerstructure
A proper finite-support learner for a concept class C. This structure captures the existence of a bounded-support ERM with error at most 1/3 for any C-realizable finite distribution. CORRECTED: good_on_support returns Finset X (not Fin k → X).
```
(X : Type u) → ConceptClass X Bool → Type u
```

DefinitionProperFiniteSupportLearner.learndef

{X : Type u} → {C : ConceptClass X Bool} → ProperFiniteSupportLearner X C → {m : ℕ} → (Fin m → X × Bool) → X → Bool

DefinitionProperFiniteSupportLearner.sampleBounddef

{X : Type u} → {C : ConceptClass X Bool} → ProperFiniteSupportLearner X C → ℕ

DefinitionShattersdefYaël Dillies
A set S ⊆ X is shattered by concept class C if every labeling of S is realized by some concept in C.
```
(X : Type u) → ConceptClass X Bool → Finset X → Prop
```
DefinitionSignVectordef
```
ℕ → Type
```
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 → ℝ
```
DefinitionVCDimdef
VC dimension of a concept class: the size of the largest shattered set. Returns ℕ∞ = WithTop ℕ.
```
(X : Type u) → ConceptClass X Bool → WithTop ℕ
```
DefinitionagreeTestdef
Per-point agreement test: for a fixed point x ∈ Y and concept c, maps hypothesis h to whether h(x) = c(x).
```
{X : Type u} → (X → Bool) → X → (HY : Finset (X → Bool)) → ↥HY → Bool
```

DefinitionagreeTestsdef

The family of agreement tests over all points in Y.

{X : Type u} → (X → Bool) → Finset X → (HY : Finset (X → Bool)) → Finset (↥HY → Bool)

DefinitionboolFamilyToFinsetFamilydef
Maps a finite family of Bool-valued functions to its image as a family of accepting sets. The set-system view is what Mathlib's Finset.Shatters and Finset.vcDim consume, so this is the entry point from the function-class view to the combinatorial VC machinery.
```
{H : Type u_1} → [Fintype H] → [DecidableEq H] → Finset (H → Bool) → Finset (Finset H)
```

DefinitionboolGamePayoffdef

Expected payoff of distribution p against column c in a Boolean game.

{R : Type u_1} → {C : Type u_2} → [inst : Fintype R] → (R → C → Bool) → FinitePMF R → C → ℝ

DefinitionboolTestExpectationdef
Expected value of a Bool-valued test under a finite distribution, via the indicator embedding if f h then 1 else 0. The central quantity of the finite-VC approximation layer: a TV bound on distributions translates to a uniform bound on test expectations via expectation_approx_of_tv.
```
{H : Type u_1} → [inst : Fintype H] → FinitePMF H → (H → Bool) → ℝ
```
DefinitionboolToSigndef
Convert Bool labels to ±1 reals. true ↦ 1, false ↦ -1.
```
Bool → ℝ
```
DefinitionboundedSubsamplesdef
Bounded subsamples: all subsets of Y with cardinality ≤ s.
```
{X : Type u} → Finset X → ℕ → Finset (Finset X)
```
DefinitiondecodeWitnessLabeldef
Decode labels from the kernel. This is exactly the current MY reconstruction convention in your file.
```
{X : Type u} → [DecidableEq X] → Finset (X × Bool) → X → Bool
```
DefinitiondecodeWitnessXCoordsdef
Decode the X-coordinates of a block from kernel positions. This matches the current blockHyp shape.
```
{X : Type u} → Finset (X × Bool) → {K : ℕ} → Finset (Fin K) → Finset X
```
DefinitiondisagreementFamilydef
The disagreement family: for each h ∈ C, the test y ↦ decide(h(y) ≠ c(y)) restricted to Y. Used for the VC approximation step in the proper learner proof.
```
{X : Type u} → ConceptClass X Bool → (X → Bool) → (Y : Finset X) → Finset (↥Y → Bool)
```

DefinitionempiricalPMFdef

Build FinitePMF from empirical frequencies of a finite sequence.

{α : Type u_1} → [inst : Fintype α] → [DecidableEq α] → {T : ℕ} → 0 < T → (Fin T → α) → FinitePMF α

DefinitionencodeWitnessInfodef
Encode a witness set W as the set of kernel positions of the pairs (x, c x). The bound kernel.card ≤ K is fed into the encoding through the if branch, so the result has the same shape as the current compressCore code.
```
{X : Type u} → [DecidableEq X] → Finset (X × Bool) → (X → Bool) → (K : ℕ) → Finset X → Finset (Fin K)
```

DefinitionextendBooldef

{H : Type u_1} → (H → Bool) → H ⊕ ℕ → Bool

DefinitionhypothesisEnvelopedef
The hypothesis envelope: the finite set of all possible learner outputs on bounded subsamples of Y, labeled by concept c.
```
{X : Type u} → {C : ConceptClass X Bool} → ProperFiniteSupportLearner X C → (X → Bool) → Finset X → Finset (X → Bool)
```
DefinitionlabeledSampleOfFinsetdef
Build a labeled sample from a Finset of points and a concept.
```
{X : Type u} → (X → Bool) → (Z : Finset X) → Fin Z.card → X × Bool
```

DefinitionliftClassdef

{H : Type u_1} → Finset (H → Bool) → ConceptClass (H ⊕ ℕ) Bool

DefinitionmkIncidenceSchemeOfMajoritydef

The actual final closure helper. Packages the majority-vote construction. If decoded hypotheses agree with reference hypotheses on sample points, and majority of reference hypotheses agree with each label, then majority-vote reconstruction is correct.

{X : Type u} →
  {C : ConceptClass X Bool} →
    (T K : ℕ) →
      (compressCore : {m : ℕ} → (Fin m → X × Bool) → Finset (X × Bool) × IncidenceInfo T K) →
        (blockHyp : Finset (X × Bool) → IncidenceInfo T K → Fin T → X → Bool) →
          (rowHyp :
              {m : ℕ} → (S : Fin m → X × Bool) → (∃ c ∈ C, ∀ (i : Fin m), c (S i).1 = (S i).2) → Fin T → X → Bool) →
            0 < T →
              (∀ {m : ℕ} (S : Fin m → X × Bool), (compressCore S).1.card ≤ K) →
                (∀ {m : ℕ} (S : Fin m → X × Bool), ↑(compressCore S).1 ⊆ Set.range S) →
                  (∀ {m : ℕ} (S : Fin m → X × Bool) (hreal : ∃ c ∈ C, ∀ (i : Fin m), c (S i).1 = (S i).2) (i : Fin m)
                      (t : Fin T),
                      blockHyp (compressCore S).1 (compressCore S).2 t (S i).1 = rowHyp S hreal t (S i).1) →
                    (∀ {m : ℕ} (S : Fin m → X × Bool) (hreal : ∃ c ∈ C, ∀ (i : Fin m), c (S i).1 = (S i).2) (i : Fin m),
                        (∑ t, if rowHyp S hreal t (S i).1 = (S i).2 then 1 else 0) / ↑T > 1 / 2) →
                      CompressionSchemeWithInfo0 X Bool C

DefinitionmwuConfigdef

The MWU config after T steps.

{R : Type u_1} →
  {C : Type u_2} →
    [Fintype R] →
      [inst : Fintype C] →
        [Nonempty C] →
          (M : R → C → Bool) →
            (η : ℝ) →
              η < 1 →
                (v : ℝ) →
                  (∀ (q : FinitePMF C), ∃ r, v ≤ ∑ c, q.prob c * if M r c = true then 1 else 0) → ℕ → MWUConfig C

DefinitionmwuHitCountdef

Count how many rounds hit a fixed column, aligned to the recursion of mwuRun.

{R : Type u_1} →
  {C : Type u_2} →
    [Fintype R] →
      [inst : Fintype C] →
        [Nonempty C] →
          (M : R → C → Bool) →
            (η : ℝ) →
              η < 1 →
                (v : ℝ) → (∀ (q : FinitePMF C), ∃ r, v ≤ ∑ c, q.prob c * if M r c = true then 1 else 0) → ℕ → C → ℕ

DefinitionmwuInitdef

Initial config: all weights = 1.

(C : Type u_1) → [inst : Fintype C] → MWUConfig C

DefinitionmwuRowsdef

The MWU row sequence after T steps.

{R : Type u_1} →
  {C : Type u_2} →
    [Fintype R] →
      [inst : Fintype C] →
        [Nonempty C] →
          (M : R → C → Bool) →
            (η : ℝ) →
              η < 1 →
                (v : ℝ) →
                  (∀ (q : FinitePMF C), ∃ r, v ≤ ∑ c, q.prob c * if M r c = true then 1 else 0) → (T : ℕ) → Fin T → R

DefinitionmwuRundef

MWU run: iterate T steps, returning final config and row sequence.

{R : Type u_1} →
  {C : Type u_2} →
    [Fintype R] →
      [inst : Fintype C] →
        [Nonempty C] →
          (M : R → C → Bool) →
            (η : ℝ) →
              η < 1 →
                (v : ℝ) →
                  (∀ (q : FinitePMF C), ∃ r, v ≤ ∑ c, q.prob c * if M r c = true then 1 else 0) →
                    (T : ℕ) → MWUConfig C × (Fin T → R)

DefinitionmwuUpdateWeightsdef

One MWU update step on weights.

{C : Type u_1} → [inst : Fintype C] → {R : Type u_2} → (R → C → Bool) → (η : ℝ) → η < 1 → MWUConfig C → R → MWUConfig C

DefinitionpointSupportdef
Extract the domain points from a labeled sample.
```
{X : Type u} → {m : ℕ} → (Fin m → X × Bool) → Finset X
```

DefinitionsupportErrordef

Weighted error of hypothesis h vs concept c over a FinitePMF on Y.

{X : Type u} → (Y : Finset X) → FinitePMF ↥Y → (X → Bool) → (X → Bool) → ℝ

DefinitionuniformPMFdef

Uniform PMF over a nonempty Fintype.

(C : Type u_1) → [inst : Fintype C] → [Nonempty C] → FinitePMF C

DefinitionzeroOneLossdef
The 0-1 loss for classification.
```
(Y : Type v) → [DecidableEq Y] → LossFunction Y
```

DOIMTH.R-2026-6009

Cite

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: 621b434c4018
Verified: 2026-09-24T00:00:00Z