Averaging designated pairs over coordinate subsets

Every fixed pair lies in the same number of subsets of a specified cardinality. Double counting therefore supplies a partition retaining the exact expected number of designated pairs, without probabilistic independence assumptions.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.exists_subset_many_pairs {n a : ℕ} (ha : 2 ≤ a) (han : a ≤ n) {J : Type u_1} [Fintype J] (left right : J → Fin n) (distinct : ∀ (j : J), left j ≠ right j) : ∃ (U : Finset (Fin n)), U.card = a ∧ n.choose a * {j : J | left j ∈ U ∧ right j ∈ U}.card ≥ (n - 2).choose (a - 2) * Fintype.card J

An input subset retains at least the average number of designated distinct pairs.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.exists_subset_pair_ratio {n a : ℕ} (ha : 2 ≤ a) (han : a ≤ n) {J : Type u_1} [Fintype J] (left right : J → Fin n) (distinct : ∀ (j : J), left j ≠ right j) : ∃ (U : Finset (Fin n)), U.card = a ∧ ↑a * (↑a - 1) / (↑n * (↑n - 1)) * ↑(Fintype.card J) ≤ ↑{j : J | left j ∈ U ∧ right j ∈ U}.card

The real-valued form of pair averaging has the exact two-coordinate survival factor.