Walsh sign families.

def NonMRR.vectorPrefix {L : ℕ} (v : Fin L → ℝ) (j : ℕ) : ℝ

The sum of the first j coordinates of a finite real vector.

Equations

• NonMRR.vectorPrefix v j = ∑ i : Fin L with ↑i < j, v i

theorem NonMRR.exists_walsh_subset_vectors (m : ℕ) : ∃ (L : ℕ), 0 < L ∧ ∃ (v : Fin m → Fin L → ℝ), (∀ (k : Fin m), ∑ i : Fin L, v k i = 0) ∧ (∀ (k : Fin m) (i : Fin L), |v k i| = 1 / ↑L) ∧ ∀ (s : Finset (Fin L)), ∑ k : Fin m, (∑ i ∈ s, v k i) ^ 2 ≤ 1

Walsh sign vectors are balanced and satisfy Bessel's bound on every subset of coordinates. The length is the cardinality of the Boolean cube.

theorem NonMRR.exists_walsh_vectors (m : ℕ) : ∃ (L : ℕ), 0 < L ∧ ∃ (v : Fin m → Fin L → ℝ), (∀ (k : Fin m), ∑ i : Fin L, v k i = 0) ∧ (∀ (k : Fin m) (i : Fin L), |v k i| = 1 / ↑L) ∧ ∀ (σ : Equiv.Perm (Fin L)) (j : ℕ), ∑ k : Fin m, vectorPrefix (v k ∘ ⇑σ) j ^ 2 ≤ 1

The Walsh vectors satisfy the prefix-square estimate in every ordering.