Finite covering by a dense relation

The elementary greedy covering argument used in sparse synthesis: if each target is covered by at least a fixed fraction of the candidates, successive choices shrink the uncovered set geometrically.

theorem Complexity.CircuitSparseSynthesis.Internal.sum_card_filter_comm {α β : Type} [Fintype α] (s : Finset β) (r : α → β → Prop) [DecidableRel r] : ∑ a : α, (Finset.filter (r a) s).card = ∑ b ∈ s, {a : α | r a b}.card

theorem Complexity.CircuitSparseSynthesis.Internal.exists_dense_row {α β : Type} [Fintype α] (s : Finset β) (r : α → β → Prop) [DecidableRel r] [Nonempty α] (a : ℕ) (dense : ∀ b ∈ s, Fintype.card α ≤ a * {x : α | r x b}.card) : ∃ (x : α), s.card ≤ a * (Finset.filter (r x) s).card

theorem Complexity.CircuitSparseSynthesis.Internal.exists_partial_cover {α β : Type} [Fintype α] (s : Finset β) (r : α → β → Prop) [DecidableRel r] [Nonempty α] [DecidableEq α] (a : ℕ) (positive : 0 < a) (dense : ∀ b ∈ s, Fintype.card α ≤ a * {x : α | r x b}.card) (steps : ℕ) : ∃ (chosen : Finset α), chosen.card ≤ steps ∧ ↑{b ∈ s | ∀ x ∈ chosen, ¬r x b}.card ≤ ↑s.card * (1 - 1 / ↑a) ^ steps

theorem Complexity.CircuitSparseSynthesis.Internal.exists_cover {α β : Type} [Fintype α] (s : Finset β) (r : α → β → Prop) [DecidableRel r] [Nonempty α] [DecidableEq α] (a length : ℕ) (positive : 0 < a) (size : s.card ≤ 4 ^ length) (dense : ∀ b ∈ s, Fintype.card α ≤ a * {x : α | r x b}.card) : ∃ (chosen : Finset α), chosen.card ≤ (4 * length + 1) * a ∧ ∀ b ∈ s, ∃ x ∈ chosen, r x b