Mathesis
Dhruv GuptaDhruv GuptaZetetic-Dhruvperson2026-09-24T00:00:00Z
ClaimMTH.C-2026-6005ArgumentMTH.R-2026-6005

Pajor's inequality for multiclass concept classes, with no hypotheses on the domain, the label type or the family: the traces of π’ž on S are at most as many as the pair-cubes of π’ž supported inside S.

The count runs on a split of the family at a point where two traces differ, taking one branch per realised value with no residual bucket. A cube of a branch never constrains the split point, so a cube pair-shattered by ΞΌ branches is counted ΞΌ times on the left and supplies 1 + ΞΌ.choose 2 cubes on the right, which closes the accounting because ΞΌ ≀ 1 + ΞΌ.choose 2 for ΞΌ β‰₯ 1, with equality exactly at ΞΌ ∈ {1, 2}. An infinite trace family forces infinitely many one-point cubes and both sides are ⊀.

At Y = Bool this specialises to encard_image_inter_le_encard_shatters, which is encard_image_inter_le_encard_shatters_of_multiclass below. The pair-cube is Natarajan's shattering witness for spaces of functions, from p. 81 of On learning sets and functions; see the module docstring.

Declencard_image_restrict_le_encard_pairCubes
βˆ€ {X : Type u_1} {Y : Type u_2} (π’ž : Set (X β†’ Y)) (S : Set X), (S.restrict '' π’ž).encard ≀ (pairCubes π’ž S).encard
TopicMulticlass dimensions

Relations

Layout
ThesisStepDefinition
encard_image_restrict_le_…theoreminfinite_pairCubes_of_inf…theoremsingCube_right_injectivetheoremsingCube_apply_selftheoremsingCube_mem_pairCubestheorempairSupport_singCubetheoremexists_injOn_pairCubestheorempairOf_right_injectivetheoremncard_image_restrict_sep_…theoremdisjoint_image_restrict_s…theoremmem_pairCubes_graft_pairOftheorempairSupport_graft_subsettheorempairShatters_grafttheorempairSupport_grafttheorempairOf_isPairPatterntheorempairOf_selftheorempairOf_of_netheoremisPairPattern_grafttheoremgraft_empty_selftheoremmonotheoremgraft_eq_grafttheoremgraft_selftheoremgraft_of_netheoremexists_sel_attheoremexists_seltheoremexists_injOn_of_subsingle…theoremconst_empty_mem_pairCubestheorempairSupport_const_emptytheoremIsPairPatterndefPairShattersdefgraftdefpairCubesdefpairOfdefpairSupportdefsingCubedef
  1. Declencard_image_restrict_le_encard_pairCubesDeclaration kindtheorem
    βˆ€ {X : Type u_1} {Y : Type u_2} (π’ž : Set (X β†’ Y)) (S : Set X), (S.restrict '' π’ž).encard ≀ (pairCubes π’ž S).encard
    pairCubes
    Uses
  2. Declinfinite_pairCubes_of_infinite_image_restrictDeclaration kindtheorem

    Infinitely many traces force infinitely many cubes. Either the family disagrees at infinitely many points of S, each of which carries a one-point cube, or it realises infinitely many labels at one point, which carries infinitely many one-point cubes. The proof runs the contrapositive: finitely many cubes bound both the disagreement set and, above each of its points, the set of realised labels, and a trace is determined by its values on the disagreement set, so the traces embed in a finite product. This is what makes the multiclass inequality hypothesis-free, as infinite_setOf_shatters does in the binary case.

    βˆ€ {X : Type u_1} {Y : Type u_2} {π’ž : Set (X β†’ Y)} {S : Set X}, (S.restrict '' π’ž).Infinite β†’ (pairCubes π’ž S).Infinite
    pairCubespairSupportsingCube
    Uses
    Used by
  3. DeclsingCube_right_injectiveDeclaration kindtheorem
    βˆ€ {X : Type u_1} {Y : Type u_2} (z : X) (u : Y), Function.Injective (singCube✝ z u)
    pairOfsingCube
    Uses
    Used by
  4. DeclsingCube_apply_selfDeclaration kindtheorem
    βˆ€ {X : Type u_1} {Y : Type u_2} (z : X) (u v : Y), singCube✝ z u v z = pairOf✝ u v
    pairOfsingCube
    Uses
    Used by
  5. DeclsingCube_mem_pairCubesDeclaration kindtheorem
    βˆ€ {X : Type u_1} {Y : Type u_2} {π’ž : Set (X β†’ Y)} {S : Set X} {u v : Y} {z : X},
  z ∈ S β†’ (βˆƒ c ∈ π’ž, c z = u) β†’ (βˆƒ c ∈ π’ž, c z = v) β†’ singCube✝ z u v ∈ pairCubes π’ž S
    pairCubessingCube
    Uses
    Used by
  6. DeclpairSupport_singCubeDeclaration kindtheorem
    βˆ€ {X : Type u_1} {Y : Type u_2} {u v : Y} (z : X), u β‰  v β†’ pairSupport (singCube✝ z u v) = {z}
    graftpairOfpairSupportsingCube
    Uses
    Used by
  7. Declexists_injOn_pairCubesDeclaration kindtheorem

    The whole accounting, as one injection from traces to cubes.

    At a point where two traces differ, every realised value gets its own branch, and a trace is routed by the value it takes there. The branch injections supplied by the induction hypothesis land in cubes that avoid that point, and a cube pair-shattered by ΞΌ branches carries ΞΌ traces into ΞΌ of the 1 + ΞΌ.choose 2 cubes available above it: the cube itself for the branch selected as the anchor, and one graft for each of the other ΞΌ - 1. Injectivity is read off the graft, since pairOf u Β· is injective and the pattern below the new point is recovered by evaluating away from it.

    βˆ€ {X : Type u_1} {Y : Type u_2} (S : Set X) (N : β„•) (π’ž : Set (X β†’ Y)),
  (S.restrict '' π’ž).Finite β†’
    (S.restrict '' π’ž).ncard ≀ N β†’ βˆƒ Ο†, Set.MapsTo Ο† (S.restrict '' π’ž) (pairCubes π’ž S) ∧ Set.InjOn Ο† (S.restrict '' π’ž)
    IsPairPatternPairShattersgraftpairCubespairOfpairSupport
    Uses
    Used by
  8. DeclpairOf_right_injectiveDeclaration kindtheorem
    βˆ€ {Y : Type u_2} (u : Y), Function.Injective (pairOf✝ u)
    pairOf
    Uses
    Used by
  9. Declncard_image_restrict_sep_ltDeclaration kindtheorem

    Splitting off one realised value at a point of S where the family is not constant strictly lowers the number of traces, because a second value survives outside the branch.

    βˆ€ {X : Type u_1} {Y : Type u_2} {π’ž : Set (X β†’ Y)} {S : Set X} {x : X} {u : Y},
  x ∈ S β†’
    βˆ€ {c : X β†’ Y},
      c ∈ π’ž β†’ c x β‰  u β†’ (S.restrict '' π’ž).Finite β†’ (S.restrict '' {d | d ∈ π’ž ∧ d x = u}).ncard < (S.restrict '' π’ž).ncard
    Uses
    Used by
  10. Decldisjoint_image_restrict_sepDeclaration kindtheorem

    Two branches at one point of S cut disjoint families of traces.

    βˆ€ {X : Type u_1} {Y : Type u_2} {π’ž : Set (X β†’ Y)} {S : Set X} {x : X} {u v : Y},
  x ∈ S β†’ u β‰  v β†’ Disjoint (S.restrict '' {d | d ∈ π’ž ∧ d x = u}) (S.restrict '' {d | d ∈ π’ž ∧ d x = v})
    Used by
  11. Declmem_pairCubes_graft_pairOfDeclaration kindtheorem
    βˆ€ {X : Type u_1} {Y : Type u_2} {π’ž : Set (X β†’ Y)} {S : Set X} {P : X β†’ Set Y} {x : X} {u v : Y},
  x ∈ S β†’
    P ∈ pairCubes {c | c ∈ π’ž ∧ c x = u} S β†’
      P ∈ pairCubes {c | c ∈ π’ž ∧ c x = v} S β†’ graft P x (pairOf✝ u v) ∈ pairCubes π’ž S
    IsPairPatternPairShattersgraftpairCubespairOfpairSupport
    Uses
    Used by
  12. DeclpairSupport_graft_subsetDeclaration kindtheorem
    βˆ€ {X : Type u_1} {Y : Type u_2} {S : Set X} {P : X β†’ Set Y} {x : X},
  x ∈ S β†’ pairSupport P βŠ† S β†’ βˆ€ (s : Set Y), pairSupport (graft P x s) βŠ† S
    graftpairSupport
    Uses
    Used by
  13. DeclpairShatters_graftDeclaration kindtheorem

    The graft. A pattern pair-shattered by the branch at a and by the branch at b extends by one unconstrained point carrying the pair {a, b} there to a pattern pair-shattered by the whole family. The selection at the new point names the branch that realises it. This is the multiclass exchange step, and it mirrors Shatters.insert.

    The two labels are not required to differ. Distinctness is what makes the result a pair pattern, and it enters at mem_pairCubes_graft_pairOf, not here.

    βˆ€ {X : Type u_1} {Y : Type u_2} {π’ž : Set (X β†’ Y)} {P : X β†’ Set Y} {x : X} {a b : Y},
  P x = βˆ… β†’
    PairShatters {c | c ∈ π’ž ∧ c x = a} P β†’ PairShatters {c | c ∈ π’ž ∧ c x = b} P β†’ PairShatters π’ž (graft P x {a, b})
    PairShattersgraftpairSupport
    Uses
    Used by
  14. DeclpairSupport_graftDeclaration kindtheorem
    βˆ€ {X : Type u_1} {Y : Type u_2} (P : X β†’ Set Y) (x : X) {s : Set Y},
  s.Nonempty β†’ pairSupport (graft P x s) = insert x (pairSupport P)
    graftpairSupport
    Uses
    Used by
  15. DeclpairOf_isPairPatternDeclaration kindtheorem
    βˆ€ {Y : Type u_2} (u v : Y), pairOf✝ u v = βˆ… ∨ (pairOf✝ u v).encard = 2
    pairOf
    Uses
    Used by
  16. DeclpairOf_selfDeclaration kindtheorem
    βˆ€ {Y : Type u_2} {u v : Y}, u = v β†’ pairOf✝ u v = βˆ…
    pairOf
    Used by
  17. DeclpairOf_of_neDeclaration kindtheorem
    βˆ€ {Y : Type u_2} {u v : Y}, u β‰  v β†’ pairOf✝ u v = {u, v}
    pairOf
    Used by
  18. DeclisPairPattern_graftDeclaration kindtheorem
    βˆ€ {X : Type u_1} {Y : Type u_2} {P : X β†’ Set Y},
  IsPairPattern P β†’ βˆ€ (x : X) {s : Set Y}, s = βˆ… ∨ s.encard = 2 β†’ IsPairPattern (graft P x s)
    IsPairPatterngraft
    Uses
    Used by
  19. Declgraft_empty_selfDeclaration kindtheorem
    βˆ€ {X : Type u_1} {Y : Type u_2} {P : X β†’ Set Y} {x : X}, P x = βˆ… β†’ graft P x βˆ… = P
    graft
    Uses
    Used by
  20. DeclPairShatters.monoDeclaration kindtheorem
    βˆ€ {X : Type u_1} {Y : Type u_2} {π’ž π’Ÿ : Set (X β†’ Y)} {P : X β†’ Set Y}, π’ž βŠ† π’Ÿ β†’ PairShatters π’ž P β†’ PairShatters π’Ÿ P
    PairShatterspairSupport
    Used by
  21. Declgraft_eq_graftDeclaration kindtheorem
    βˆ€ {X : Type u_1} {Y : Type u_2} {P P' : X β†’ Set Y} {x : X},
  P x = βˆ… β†’ P' x = βˆ… β†’ βˆ€ {s s' : Set Y}, graft P x s = graft P' x s' β†’ P = P' ∧ s = s'
    graft
    Uses
    Used by
  22. Declgraft_selfDeclaration kindtheorem
    βˆ€ {X : Type u_1} {Y : Type u_2} (P : X β†’ Set Y) (x : X) (s : Set Y), graft P x s x = s
    graft
    Used by
  23. Declgraft_of_neDeclaration kindtheorem
    βˆ€ {X : Type u_1} {Y : Type u_2} {x z : X} (P : X β†’ Set Y) (s : Set Y), z β‰  x β†’ graft P x s z = P z
    graft
    Used by
  24. Declexists_sel_atDeclaration kindtheorem

    The single-point case: an admissible label at x extends to a selection taking it there.

    βˆ€ {X : Type u_1} {Y : Type u_2} {P : X β†’ Set Y} {x : X} {u : Y},
  u ∈ P x β†’ βˆƒ Ο„, Ο„ x = u ∧ βˆ€ ⦃z : X⦄, z ∈ pairSupport P β†’ Ο„ z ∈ P z
    pairSupport
    Uses
    Used by
  25. Declexists_selDeclaration kindtheorem

    A choice of admissible labels prescribed on part of the domain extends to a selection for the whole pattern. The prescribed values arrive as a total function, so off the support there is always a label to copy and no hypothesis on Y is needed.

    βˆ€ {X : Type u_1} {Y : Type u_2} {P : X β†’ Set Y} {B : Set X} {Οƒ : X β†’ Y},
  (βˆ€ ⦃z : X⦄, z ∈ B β†’ z ∈ pairSupport P β†’ Οƒ z ∈ P z) β†’ βˆƒ Ο„, (βˆ€ ⦃z : X⦄, z ∈ pairSupport P β†’ Ο„ z ∈ P z) ∧ Set.EqOn Ο„ Οƒ B
    pairSupport
    Used by
  26. Declexists_injOn_of_subsingletonDeclaration kindtheorem
    βˆ€ {X : Type u_1} {Y : Type u_2} {π’ž : Set (X β†’ Y)} {S : Set X},
  (S.restrict '' π’ž).Subsingleton β†’ βˆƒ Ο†, Set.MapsTo Ο† (S.restrict '' π’ž) (pairCubes π’ž S) ∧ Set.InjOn Ο† (S.restrict '' π’ž)
    pairCubes
    Uses
    Used by
  27. Declconst_empty_mem_pairCubesDeclaration kindtheorem

    The unconstrained pattern is a cube of every nonempty family. It is the multiclass reading of shatters_bot.

    βˆ€ {X : Type u_1} {Y : Type u_2} {π’ž : Set (X β†’ Y)} (S : Set X), π’ž.Nonempty β†’ (fun x => βˆ…) ∈ pairCubes π’ž S
    IsPairPatternPairShatterspairCubespairSupport
    Uses
    Used by
  28. DeclpairSupport_const_emptyDeclaration kindtheorem
    βˆ€ {X : Type u_1} {Y : Type u_2}, (pairSupport fun x => βˆ…) = βˆ…
    pairSupport
    Used by
  29. DefinitionIsPairPatterndef

    A pattern is a pair pattern when it offers either no constraint or exactly two labels at each point. The two labels are recorded as a set, so their order carries no information.

    {X : Type u_1} β†’ {Y : Type u_2} β†’ (X β†’ Set Y) β†’ Prop
  30. DefinitionPairShattersdef

    A family pair-shatters a pattern when every choice of one admissible label per constrained point is realised by some member.

    {X : Type u_1} β†’ {Y : Type u_2} β†’ Set (X β†’ Y) β†’ (X β†’ Set Y) β†’ Prop
  31. Definitiongraftdef

    Overwrite a pattern at one point. Stated without a decidable equality on X, since the two branches are separated by a hypothesis rather than by a test.

    {X : Type u_1} β†’ {Y : Type u_2} β†’ (X β†’ Set Y) β†’ X β†’ Set Y β†’ X β†’ Set Y
  32. DefinitionpairCubesdef

    The pair-cubes of π’ž over S: pair patterns supported inside S and pair-shattered by π’ž.

    {X : Type u_1} β†’ {Y : Type u_2} β†’ Set (X β†’ Y) β†’ Set X β†’ Set (X β†’ Set Y)
  33. DefinitionpairOfdef

    The unordered pair {u, v}, degenerating to the empty set when u = v. Carrying the degenerate case inside the pair lets one formula cover both branches of the injection.

    {Y : Type u_2} β†’ Y β†’ Y β†’ Set Y
  34. DefinitionpairSupportdef

    The points at which a pattern constrains a concept.

    {X : Type u_1} β†’ {Y : Type u_2} β†’ (X β†’ Set Y) β†’ Set X
  35. DefinitionsingCubedef

    The cube supported at the single point z, offering the labels u and v there.

    {X : Type u_1} β†’ {Y : Type u_2} β†’ X β†’ Y β†’ Y β†’ X β†’ Set Y
DOIMTH.R-2026-6005
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
fd764e365885
Verified
2026-09-24T00:00:00Z