Padding witnesses collapses the bad-sample dimension

def GenLimit.FiniteWitness.BadSample {α : Type u_1} (H : Set (Set α)) (T : Set α → Finset α) (S : Finset α) : Prop

A sample with a nonempty active subfamily whose common core is finite.

Equations

• GenLimit.FiniteWitness.BadSample H T S = ((GenLimit.FiniteWitness.active H T S).Nonempty ∧ (GenLimit.FiniteWitness.activeCore H T S).Finite)

noncomputable def GenLimit.FiniteWitness.badCost {α : Type u_1} (H : Set (Set α)) (T : Set α → Finset α) : WithTop ℕ

The supremum of one plus the size of every bad sample for an assignment.

Equations

• GenLimit.FiniteWitness.badCost H T = ⨆ (S : { S : Finset α // GenLimit.FiniteWitness.BadSample H T S }), ↑((↑S).card + 1)

noncomputable def GenLimit.FiniteWitness.paddedDimension {α : Type u_1} (H : Set (Set α)) : WithTop ℕ

The infimum of bad-sample costs over positive witness assignments.

Equations

• GenLimit.FiniteWitness.paddedDimension H = ⨅ (T : { T : Set α → Finset α // GenLimit.FiniteWitness.Positive H T }), GenLimit.FiniteWitness.badCost H ↑T

theorem GenLimit.FiniteWitness.badCost_le_iff {α : Type u_1} (H : Set (Set α)) (T : Set α → Finset α) (d : ℕ) : badCost H T ≤ ↑d ↔ ∀ (S : Finset α), BadSample H T S → S.card + 1 ≤ d

theorem GenLimit.FiniteWitness.badCost_zero_iff {α : Type u_1} {H : Set (Set α)} {T : Set α → Finset α} (hp : Positive H T) : badCost H T = 0 ↔ Valid H T

theorem GenLimit.FiniteWitness.padding_removes_finite_defects {α : Type u_1} {H : Set (Set α)} (hUUS : Generic.UUS H) {T : Set α → Finset α} (hp : Positive H T) (d : ℕ) (hb : ∀ (S : Finset α), BadSample H T S → S.card + 1 ≤ d) : ∃ (T' : Set α → Finset α), Valid H T' ∧ ∀ L ∈ H, T L ⊆ T' L

A finite bound on bad sample sizes can be removed by retaining and padding witnesses.

theorem GenLimit.FiniteWitness.finite_badCost_implies_finiteWitnesses {α : Type u_1} {H : Set (Set α)} (hUUS : Generic.UUS H) {T : Set α → Finset α} (hp : Positive H T) {d : ℕ} (hb : badCost H T ≤ ↑d) : HasFiniteWitnesses H

theorem GenLimit.FiniteWitness.paddedDimension_zero_of_finiteWitnesses {α : Type u_1} {H : Set (Set α)} (h : HasFiniteWitnesses H) : paddedDimension H = 0

theorem GenLimit.FiniteWitness.paddedDimension_top_of_not_finiteWitnesses {α : Type u_1} {H : Set (Set α)} (hUUS : Generic.UUS H) (h : ¬HasFiniteWitnesses H) : paddedDimension H = ⊤

theorem GenLimit.FiniteWitness.padding_collapse {α : Type u_1} [Countable α] [Infinite α] (H : Set (Set α)) (hUUS : Generic.UUS H) : (Generic.GeneratableInLimit H → paddedDimension H = 0) ∧ (¬Generic.GeneratableInLimit H → paddedDimension H = ⊤)