Finite vector constructions.

@[simp]

theorem NonMRR.prefix_zero {L : ℕ} (v : Fin L → ℝ) : vectorPrefix v 0 = 0

@[simp]

theorem NonMRR.prefix_length {L : ℕ} (v : Fin L → ℝ) : vectorPrefix v L = ∑ i : Fin L, v i

theorem NonMRR.prefix_succ_sub {L i : ℕ} (v : Fin L → ℝ) (hi : i < L) : vectorPrefix v (i + 1) - vectorPrefix v i = v ⟨i, hi⟩

theorem NonMRR.card_bad_prefixes_le {m L q : ℕ} (hL : 0 < L) (hq : 0 < q) (v : Fin m → Fin L → ℝ) (hbalanced : ∀ (k : Fin m), ∑ i : Fin L, v k i = 0) (habs : ∀ (k : Fin m) (i : Fin L), |v k i| = 1 / ↑L) (hprefix : ∀ (σ : Equiv.Perm (Fin L)) (j : ℕ), ∑ k : Fin m, vectorPrefix (v k ∘ ⇑σ) j ^ 2 ≤ 1) (σ : Equiv.Perm (Fin L)) : {k : Fin m | ∃ j ≤ L, 1 / ↑q < |vectorPrefix (v k ∘ ⇑σ) j|}.card ≤ 4 * q ^ 4

The counting estimate for every ordering of a family satisfying the Walsh identities.

theorem NonMRR.finite_counting_estimate (m : ℕ) {q : ℕ} (hq : 0 < q) : ∃ (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)), {k : Fin m | ∃ j ≤ L, 1 / ↑q < |vectorPrefix (v k ∘ ⇑σ) j|}.card ≤ 4 * q ^ 4

For each m and positive q, there are balanced sign vectors such that every permutation has at most 4*q^4 vectors with a vectorPrefix exceeding 1/q. This is the finite counting estimate in Section 3 of Determining the Rearrangement Number.