Both sign-sum tails from low-order parity bias #
The budget 100 * m² * δ ≤ 1 lets the first four parity-bias moment bounds
satisfy the quartic certificate in FourthMoment. Each tail beyond one eighth
of the square root of m has weighted mass at least 1/36.
This normalization is a direct deduction from the checked moment bounds and
quartic estimate. SourceReduction.Tests derives parity bias from the source
reduction of Chattopadhyay and Liao, Extractors for Sum of Two Sources (2021),
Lemma 5.4, equation (5).
theorem
Algebraic.Cutwidth.Extractor.signSum_positive_tail_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 σ δ)
:
Sufficiently small parity bias forces a positive sign-sum tail of mass
at least 1/36, beyond one eighth of sqrt m.
theorem
Algebraic.Cutwidth.Extractor.signSum_negative_tail_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 σ δ)
:
The same parity-bias budget forces the corresponding negative sign-sum tail, with the same mass and threshold.