Finite sign averages and low-order parity bias

These finite weighted sums describe the moment hypotheses needed after the source reduction in Chattopadhyay and Liao, Extractors for Sum of Two Sources (2021), Lemma 5.4, equation (5). No source reduction is assumed or constructed here. The m selected good coordinates are indexed by Fin m.

def Algebraic.Cutwidth.Extractor.weightedMean {α : Type u_1} (s : Finset α) (w X : α → ℝ) : ℝ

Weighted average over a finite sample set. Probability applications use nonnegative weights of total mass one.

Equations

• Algebraic.Cutwidth.Extractor.weightedMean s w X = ∑ a ∈ s, w a * X a

def Algebraic.Cutwidth.Extractor.signSum {α : Type u_1} {m : ℕ} (σ : α → Fin m → ℝ) (a : α) : ℝ

Sum of the selected sign coordinates at a sample.

Equations

• Algebraic.Cutwidth.Extractor.signSum σ a = ∑ i : Fin m, σ a i

def Algebraic.Cutwidth.Extractor.ParityBiasBound {α : Type u_1} {m : ℕ} (s : Finset α) (w : α → ℝ) (σ : α → Fin m → ℝ) (δ : ℝ) : Prop

Every nonempty parity on at most four selected coordinates has absolute weighted sign bias at most δ. The signs being ±1 is a separate hypothesis.

Equations

• Algebraic.Cutwidth.Extractor.ParityBiasBound s w σ δ = ∀ (T : Finset (Fin m)), T.Nonempty → T.card ≤ 4 → |Algebraic.Cutwidth.Extractor.weightedMean s w fun (a : α) => ∏ i ∈ T, σ a i| ≤ δ