Counting via involutions

If σ is an involution on a finset s and every orbit {x, σ x} meets a predicate p, then at least half of s satisfies p. This is the combinatorial core of pairing arguments such as the Ehrenfeucht–Haussler– Kearns–Valiant lower bound on PAC sample complexity.

Main statements

• Finset.card_filter_not_le_card_filter_of_involution: the elements of s failing p inject via σ into those satisfying p.
• Finset.card_div_two_le_card_filter_of_involution: at least half of s satisfies p.

theorem Finset.card_filter_not_le_card_filter_of_involution {α : Type u_1} {s : Finset α} {σ : α → α} {p : α → Prop} [DecidablePred p] (hσ : ∀ x ∈ s, σ (σ x) = x) (hσs : ∀ x ∈ s, σ x ∈ s) (hp : ∀ x ∈ s, p x ∨ p (σ x)) : {x ∈ s | ¬p x}.card ≤ (filter p s).card

If σ is an involution on s and every orbit {x, σ x} meets p, then σ injects the elements of s failing p into those satisfying p.

theorem Finset.card_div_two_le_card_filter_of_involution {α : Type u_1} {s : Finset α} {σ : α → α} {p : α → Prop} [DecidablePred p] (hσ : ∀ x ∈ s, σ (σ x) = x) (hσs : ∀ x ∈ s, σ x ∈ s) (hp : ∀ x ∈ s, p x ∨ p (σ x)) : s.card / 2 ≤ (filter p s).card

If σ is an involution on s and every orbit {x, σ x} meets p, then at least half of s satisfies p.