Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.Extractor.SourceReduction.Reduction

Parity bias of the actual XOR source reduction #

Every product of outer-coordinate signs has exactly the absolute bias of the product of its component-call signs. This identifies the quantity used by the fourth-moment majority argument with the affine correlation-breaker quantity in Chattopadhyay--Liao, Lemma 5.4, equation (5).

theorem Algebraic.Cutwidth.Extractor.affineSourceReduction_parity_bias_eq {n N C : ℕ} {α : Type u_1} {Seed : Type u_2} {Advice : Type u_3} (cb : (Fin n → Bool) → Seed → Advice → Bool) (sampler : (Fin n → Bool) → Fin N → Fin C → Seed) (advice : Fin N → Fin C → Advice) (s : Finset α) (w : α → ℝ) (input : α → Fin n → Bool) (U : Finset (Fin N)) :
|weightedMean s w fun (x : α) => ∏ i ∈ U, if affineSourceReduction cb sampler advice (input x) i = true then 1 else -1| = |weightedMean s w fun (x : α) => ∏ i ∈ U, ∏ z : Fin C, if cb (input x) (sampler (input x) i z) (advice i z) = true then 1 else -1|

Taking XORs within coordinates preserves the absolute bias of the full component parity.