DirectionDeletion.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Deleting the supports of a maximal family of bad tuples

The finite powerset construction below chooses a family of maximum cardinality. Its maximality is proved inside the argument; it is not an input hypothesis. Repeated indices within any tuple are allowed.

theorem OAI.MetricEntropyDuality.DirectionDeletion.exists_good_subset line 25

Source documentation

If there are no w bad tuples with pairwise disjoint supports, deleting at most h * (w - 1) indices removes every bad tuple.

theorem exists_good_subset {U : Type uU} [Fintype U] {h w : ℕ}
    (bad : (Fin h → U) → Prop) (hh : 0 < h)
    (hno : ¬ ∃ L : Fin w → Fin h → U,
      (∀ i, bad (L i)) ∧ DisjointSupports L) :
    ∃ T : Finset U, (Finset.univ \ T).card ≤ h * (w - 1) ∧
      ∀ a : Fin h → U, (∀ j, a j ∈ T) → ¬bad a := by
…

Mentions: OAI.MetricEntropyDuality.DisjointSupports