Weighted majority from selected sign coordinates #
The selected coordinates are indexed by an embedding, so their sign sum is the existing integer vote margin. The remaining coordinates may depend arbitrarily on the selected ones; only their number enters the margin bound.
theorem
Algebraic.Cutwidth.Extractor.Internal.signSum_eq_voteMargin
{α : Type u_1}
{m n : ℕ}
(good : Fin m ↪ Fin n)
(x : α → Fin n → Bool)
(a : α)
:
signSum (fun (a : α) (i : Fin m) => if x a (good i) = true then 1 else -1) a = ↑(voteMargin (Finset.map good Finset.univ) (x a))
theorem
Algebraic.Cutwidth.Extractor.Internal.majority_mass_ge_of_signSum_tails
{α : Type u_1}
{m n : ℕ}
(good : Fin m ↪ Fin n)
(x : α → Fin n → Bool)
(s : Finset α)
(w : α → ℝ)
{t ρ : ℝ}
(hw : ∀ a ∈ s, 0 ≤ w a)
(bad : ↑(n - m) ≤ t)
(positive :
ρ ≤ ∑ a ∈ s, if t < signSum (fun (a : α) (i : Fin m) => if x a (good i) = true then 1 else -1) a then w a else 0)
(negative :
ρ ≤ ∑ a ∈ s, if signSum (fun (a : α) (i : Fin m) => if x a (good i) = true then 1 else -1) a < -t then w a else 0)
(b : Bool)
:
theorem
Algebraic.Cutwidth.Extractor.Internal.majority_mass_ge_of_parityBias
{α : Type u_1}
{m n : ℕ}
{s : Finset α}
{w : α → ℝ}
(good : Fin m ↪ Fin n)
(x : α → Fin n → Bool)
(hw : ∀ a ∈ s, 0 ≤ w a)
(hmass : ∑ a ∈ s, w a = 1)
(hm : 0 < m)
{δ : ℝ}
(hδ : 0 ≤ δ)
(budget : 100 * ↑m ^ 2 * δ ≤ 1)
(bias : ParityBiasBound s w (fun (a : α) (i : Fin m) => if x a (good i) = true then 1 else -1) δ)
(bad : ↑(n - m) ≤ √↑m / 8)
(b : Bool)
: