Low-order sign-sum moments from parity bias

The bounds hold for finite weighted averages. Nonnegative weights of mass one specialize them to finite probability distributions. SourceReduction.Tests derives the parity-bias hypothesis for the actual source reduction.

theorem Algebraic.Cutwidth.Extractor.signSum_first_moment {α : Type u_1} {m : ℕ} {s : Finset α} {w : α → ℝ} {σ : α → Fin m → ℝ} {δ : ℝ} (h : ParityBiasBound s w σ δ) : |weightedMean s w (signSum σ)| ≤ ↑m * δ

Singleton parity bias bounds the first moment of the sum of m signs.

theorem Algebraic.Cutwidth.Extractor.signSum_second_moment {α : Type u_1} {m : ℕ} {s : Finset α} {w : α → ℝ} {σ : α → Fin m → ℝ} {δ : ℝ} (hδ : 0 ≤ δ) (hmass : ∑ a ∈ s, w a = 1) (hσ : ∀ a ∈ s, ∀ (i : Fin m), σ a i = 1 ∨ σ a i = -1) (h : ParityBiasBound s w σ δ) : |(weightedMean s w fun (a : α) => signSum σ a ^ 2) - ↑m| ≤ ↑m ^ 2 * δ

Pair parity bias bounds the deviation of the second moment from m.

theorem Algebraic.Cutwidth.Extractor.signSum_third_moment {α : Type u_1} {m : ℕ} {s : Finset α} {w : α → ℝ} {σ : α → Fin m → ℝ} {δ : ℝ} (hσ : ∀ a ∈ s, ∀ (i : Fin m), σ a i = 1 ∨ σ a i = -1) (h : ParityBiasBound s w σ δ) : |weightedMean s w fun (a : α) => signSum σ a ^ 3| ≤ ↑m ^ 3 * δ

Every odd triple reduces to a nonempty parity of at most three signs.

theorem Algebraic.Cutwidth.Extractor.signSum_fourth_moment {α : Type u_1} {m : ℕ} {s : Finset α} {w : α → ℝ} {σ : α → Fin m → ℝ} {δ : ℝ} (hδ : 0 ≤ δ) (hmass : ∑ a ∈ s, w a = 1) (hσ : ∀ a ∈ s, ∀ (i : Fin m), σ a i = 1 ∨ σ a i = -1) (h : ParityBiasBound s w σ δ) : (weightedMean s w fun (a : α) => signSum σ a ^ 4) ≤ 3 * ↑m ^ 2 + ↑m ^ 4 * δ

The three possible pairings account for at most 3m² unbiased terms; each remaining fourth-degree term is controlled by its parity bias.