Dhruv Gupta

Pajor's inequality, with no finiteness assumptions: the traces of 𝒜 on A are at most as many as the subsets of A shattered by 𝒜. For a finite trace family this is a descent on the number of traces that never consumes the ground set; an infinite trace family forces infinitely many shattered singletons, and both sides are ⊤.

Dvir, Filmus and Moran, A Sauer-Shelah-Perles Lemma for Lattices, credit the Boolean lattice case to Pajor (Sous-espaces ℓ₁ⁿ des espaces de Banach, Travaux en Cours 16, Hermann, Paris, 1985) and to Aharoni and Holzman, unpublished. Their Theorem 1.2 is the lattice form, for finite lattices with nonvanishing Möbius function: a family shatters at least as many elements as it has members. Reading that for a family of traces on a ground set is the standard translation into the language of set families, and the statement here carries no finiteness hypothesis, which theirs does.

The cardinal Pajor inequality for determined traces: the traces of 𝒜 on A that are determined by finitely many points inject into the shattered subsets, with no hypotheses. Unlike the ℕ∞-valued encard_determined_le_encard_shatters, this bounds genuine cardinalities; the full trace family cannot replace the determined traces (not_mk_image_inter_le_mk_shatters).

The full trace family cannot replace the determined traces in mk_determined_le_mk_shatters: the half-line cuts over ℚ trace continuum-many sets while shattering only countably many.

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.

HasDSDimLE.hasNatarajanDimLE has no converse. The six-cycle on a two-point domain has Natarajan dimension 1, a Natarajan witness on both points being a four-cycle, while its whole trace family is a two-dimensional pseudo-cube, so its DS dimension is at least 2.

This is the hexagon Brukhim, Carmon, Dinur, Moran and Yehudayoff record after their Definition 6, and the four-cycle test the proof turns on is their Example 7. Their Theorem 2 pushes the separation to a class of Natarajan dimension 1 and infinite DS dimension; that construction rests on hyperbolic pseudo-manifolds and is cited in the module docstring rather than formalised here.

Shelah's ded bound on the traces of a family of finite VC dimension. On an infinite ground set a family of finite VC dimension traces at most ded #A sets, and by mk_image_inter_range_cut_eq_ded the bound is attained. The infiniteness of A is not decorative: see exists_finite_ground_hasVCDimLE_not_mk_image_inter_le_ded.

No cardinal function strictly smaller than ded bounds the traces of a family of finite VC dimension. For every infinite κ and every lam < ded κ there is a family of VC dimension 1 on a ground set of size exactly κ tracing more than lam sets. Together with HasVCDimLE.mk_image_inter_le_ded, which caps those traces at ded #A, this places ded at the exact strength of the bound.

The conclusion cannot be strengthened to a family tracing exactly ded κ sets. Chernikov and Shelah, On the number of Dedekind cuts and two-cardinal models of dependent theories, note after their definition of ded κ that "in general the supremum need not be attained", so at such a κ no family attains it and quantifying below the supremum is the available form. At κ = ℵ₀ the supremum is attained, by mk_image_inter_range_cut_eq_ded.

Littlestone characterization: C is online-learnable iff LittlestoneDim(C) < ∞.

The optimal mistake bound equals the Littlestone dimension (for nonempty C). Path B: OptimalMistakeBound : WithTop ℕ, LittlestoneDim : WithBot (WithTop ℕ). For nonempty C, LittlestoneDim ≥ 0, so the coercion ↑(OptimalMistakeBound) works.

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.

The Krapp–Wirth measurable-target separation holds unconditionally: the analytic non-Borel witness discharges the hypothesis of analytic_nonborel_set_gives_measTarget_separation.

The Ambainis composition lock, at every depth: the product partition of the (d+1)-fold Ambainis iterate — the construction giving the multiplicative upper bound on the partition number — is not the leaf partition of any deterministic protocol, for every depth d. Index 0 is the base partition itself (a kernel-checked eight-rectangle monochromatic partition of the base game); index 1 is the 64-rectangle object of the depth-two frontier.

If every candidate's loss is measurable and a.e. valued in [a, b] under Q, every training-generated trajectory is admissible for F, and the resulting uniform-deviation failure event is measurable, then on an i.i.d. panel of size n drawn from Q, measured cumulative empirical-loss progress exceeds population-loss progress by more than 2 · deltaFiniteExperts (card ι) n (b - a) δ with probability at most ENNReal.ofReal δ.

F2 — given A nonempty, BlackwellEquivalent (learnerExperiment K) publicOnlyExperiment ↔ AuditSealed K (blackwell1953).

F3 — AuditSealed K ↔ ∀ s a a', equalPriorBayesError (K (s, a)) (K (s, a')) = 1/2.

Choquet capacitability. For analytic sets, capacity equals the supremum over compact subsets (Kechris 30.13).

The discrete Vorob'ev theorem: a cover's base structure is acyclic exactly when local pairwise consistency always forces a global structure, i.e. every pairwise-consistent family of nonempty local relations on it glues.

Dirac's lemma, strong form: in a chordless-cycle-free adjacency structure, every vertex set is a clique or contains two nonadjacent simplicial vertices.

The two-clique quantum junction tree theorem (Lauritzen–Zwiernik, arXiv:2605.19453, Theorem 3.1): over the acyclic two-clique base, the base's compatibility datum decides base-side reconstruction. For strictly positive consistent marginals, a quantum Markov completion exists iff Tr T(R) = 1; the completion is then unique and equals the normalized logarithmic candidate σ(R) = T(R)/Tr T(R). Together with trC_le_one (the trace bound) this is the full theorem.

Closed form of the multivariate Gaussian KL divergence (M3b). For positive-definite covariances S₁, S₂, KL(N(m₁,S₁) ‖ N(m₂,S₂)) = ½ ( log(det S₂ / det S₁) + tr(S₂⁻¹ S₁) + ⟪m₁-m₂, S₂⁻¹(m₁-m₂)⟫ - d ).

The whitening reduction (klDivReal_multivariateGaussian_whiten) sends the pair to a KL against the standard Gaussian (klDivReal_multivariateGaussian_stdGaussian); the three scalar invariants of the whitened covariance (det_whitened, trace_whitened, normSq_cfcSqrt_inv_apply) then identify the arguments.

An analytic non-Borel subset of ℝ: the image of the Baire-space witness under the continuous injection. Analyticity transfers along the continuous image; non-Borelness transfers back along the injective preimage.

Pinsker's inequality with the sharp constant. tvDistReal P Q ≤ sqrt(klDivReal P Q / 2) for probability measures P ≪ Q with finite KL divergence.

d = 1 universality: every VC-1 class compresses at kernel size one, with no side information. No finiteness, no distinguished member, no chain hypothesis. Twist the class by any member to place ∅ in it; there the VC bound makes co-member points comparable in the membership order, so every label set is a finite chain; anchor at its maximum, reconstruct with interConvention, and transport the scheme back with the same kernels.

Fundamental theorem of statistical learning (5-way equivalence, BP₅).

The fundamental theorem of statistical learning. For a measurable concept class, finite VC dimension, eventually polynomial growth, and PAC learnability are mutually equivalent.

Online learning is strictly stronger than PAC learning.

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.

VC dimension of homogeneous linear halfspaces is exactly n (Cover 1965; Vapnik–Chervonenkis). The class signClass (coordSpace n) of homogeneous linear halfspaces of ℝⁿ has VC dimension equal to the ambient dimension n: the Dudley bound gives ≤ n, and the n standard basis points are shattered, giving ≥ n.

Assouad's dual VC bound. If VCDim X C ≤ d, then VCDim(dualClass C) ≤ 2^(d+1) − 1.

Assouad's lower bound. For a finite-VC class, ⌊log₂ VCDim⌋ ≤ VCDim(dualClass): the exponential blow-up under dualization is necessary, not merely permitted. Together with the proven upper bound vcDim_dualClass_le (VCDim(dual) ≤ 2^(VCDim+1) − 1) this sandwiches the dual VC dimension between ⌊log₂ d⌋ and 2^(d+1) − 1.

Stated with d := VCDim C extracted as a natural number (finite by hypothesis). The proof picks a shattered set T with 2^(log₂ d) ≤ |T| (which exists because 2^(log₂ d) ≤ d ≤ |T| for the supremal shattered set) and applies pow_le_vcDim_imp_le_vcDim_dualClass.