Normalizing the first four sign-sum moments #
The raw parity-bias bounds, divided by powers of the square root of the number
of signs, satisfy the approximate-moment certificate in FourthMoment.
theorem
Algebraic.Cutwidth.Extractor.Internal.signSum_tails_of_parityBias
{α : Type u_1}
{m : ℕ}
{s : Finset α}
{w : α → ℝ}
{σ : α → Fin m → ℝ}
{δ : ℝ}
(hw : ∀ a ∈ s, 0 ≤ w a)
(hmass : ∑ a ∈ s, w a = 1)
(hm : 0 < m)
(hσ : ∀ a ∈ s, ∀ (i : Fin m), σ a i = 1 ∨ σ a i = -1)
(hδ : 0 ≤ δ)
(hbudget : 100 * ↑m ^ 2 * δ ≤ 1)
(h : ParityBiasBound s w σ δ)
: