Finite expansions of low-order sign moments

Repeated sign coordinates cancel in pairs. After separating those equality patterns, the parity-bias assumption bounds each remaining term.

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

theorem Algebraic.Cutwidth.Extractor.Internal.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 * δ

theorem Algebraic.Cutwidth.Extractor.Internal.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 * δ

theorem Algebraic.Cutwidth.Extractor.Internal.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 * δ