Weighted retention of fixed coordinate witnesses

Double counting all subsets of a specified size retains the exact expected weight of equally sized witness sets. In particular, triples give a common retention factor for both two-primary and wide conjunction gates.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.exists_subset_weighted_witnesses {n a d : ℕ} (hda : d ≤ a) (han : a ≤ n) {J : Type u_1} [Fintype J] (witness : J → Finset (Fin n)) (card : ∀ (j : J), (witness j).card = d) (weight : J → ℝ) : ∃ (U : Finset (Fin n)), U.card = a ∧ ↑((n - d).choose (a - d)) * ∑ j : J, weight j ≤ ↑(n.choose a) * ∑ j : J, if witness j ⊆ U then weight j else 0

Some fixed-size subset retains at least the mean weight of fixed-size witnesses.

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Joint.tripleRetention (n a : ℕ) : ℝ

The exact probability that an a-subset retains a designated triple.

Equations

• Algebraic.Cutwidth.Aggregate.Geometry.Joint.tripleRetention n a = ↑a * (↑a - 1) * (↑a - 2) / (↑n * (↑n - 1) * (↑n - 2))

theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.exists_subset_weighted_triples {n a : ℕ} (ha : 3 ≤ a) (han : a ≤ n) {J : Type u_1} [Fintype J] (witness : J → Finset (Fin n)) (card : ∀ (j : J), (witness j).card = 3) (weight : J → ℝ) : ∃ (U : Finset (Fin n)), U.card = a ∧ tripleRetention n a * ∑ j : J, weight j ≤ ∑ j : J, if witness j ⊆ U then weight j else 0

Three-coordinate retention follows directly from weighted witness averaging.