The concrete catalogue of balanced finite blocks

The blocks are Walsh vectors supported on consecutive disjoint intervals. The geometrically decaying error bound makes their eventual prefix bounds summable.

def NonMRR.blockDenominator (n : ℕ) : ℕ

The denominators of the prescribed prefix tolerances.

Equations

• NonMRR.blockDenominator n = 2 ^ (n + 1)

theorem NonMRR.blockDenominator_pos (n : ℕ) : 0 < blockDenominator n

noncomputable def NonMRR.blockTolerance (n : ℕ) : ℝ

A summable sequence of allowed prefix errors.

Equations

• NonMRR.blockTolerance n = 1 / ↑(NonMRR.blockDenominator n)

def NonMRR.blockCapacity (n : ℕ) : ℕ

The number of exceptional choices allowed at each stage.

Equations

• NonMRR.blockCapacity n = 8 * NonMRR.blockDenominator n ^ 4

theorem NonMRR.blockCapacity_pos (n : ℕ) : 0 < blockCapacity n

theorem NonMRR.blockTolerance_nonneg (n : ℕ) : 0 ≤ blockTolerance n

theorem NonMRR.blockTolerance_summable : Summable blockTolerance

structure NonMRR.FiniteBlock (m q : ℕ) : Type

A finite balanced family together with its uniform counting estimate.

• length : ℕ

  Number of coordinates in each balanced vector.

• length_pos : 0 < self.length
• value : Fin m → Fin self.length → ℝ

  The entries of the finite family of balanced vectors.

• balance (k : Fin m) : ∑ i : Fin self.length, self.value k i = 0
• abs_value (k : Fin m) (i : Fin self.length) : |self.value k i| = 1 / ↑self.length
• bad_card (σ : Equiv.Perm (Fin self.length)) : {k : Fin m | ∃ j ≤ self.length, 1 / ↑q < |vectorPrefix (self.value k ∘ ⇑σ) j|}.card ≤ 4 * q ^ 4

theorem NonMRR.finiteBlock_nonempty (m q : ℕ) (hq : 0 < q) : Nonempty (FiniteBlock m q)

noncomputable def NonMRR.chosenBlock (g : ℕ → ℕ) (n : ℕ) : FiniteBlock (g n) (blockDenominator n)

Choose one of the finite families supplied by the counting lemma.

Equations

• NonMRR.chosenBlock g n = Classical.choice ⋯

def NonMRR.blockStart (g : ℕ → ℕ) : ℕ → ℕ

The left endpoints of consecutive blocks.

Equations

• NonMRR.blockStart g 0 = 0
• NonMRR.blockStart g n.succ = NonMRR.blockStart g n + (NonMRR.chosenBlock g n).length

theorem NonMRR.blockStart_monotone (g : ℕ → ℕ) : Monotone (blockStart g)

noncomputable def NonMRR.blockEmbedding (g : ℕ → ℕ) (n : ℕ) : Fin (chosenBlock g n).length ↪ ℕ

The order-preserving embedding of a finite block into its assigned interval.

Equations

• NonMRR.blockEmbedding g n = { toFun := fun (i : Fin (NonMRR.chosenBlock g n).length) => NonMRR.blockStart g n + ↑i, inj' := ⋯ }

noncomputable def NonMRR.blockInterval (g : ℕ → ℕ) (n : ℕ) : Finset ℕ

The finite support assigned to block n.

Equations

• NonMRR.blockInterval g n = Finset.map (NonMRR.blockEmbedding g n) Finset.univ

theorem NonMRR.blockInterval_pairwise_disjoint (g : ℕ → ℕ) : Pairwise fun (n m : ℕ) => Disjoint (blockInterval g n) (blockInterval g m)

noncomputable def NonMRR.catalogueVector (g : ℕ → ℕ) (n k : ℕ) : ℕ → ℝ

Use the selected finite vector on the assigned interval, and zero for an unavailable choice.

Equations

• NonMRR.catalogueVector g n k = if hk : k < g n then NonMRR.embedVector (NonMRR.blockEmbedding g n) ((NonMRR.chosenBlock g n).value ⟨k, hk⟩) else fun (x : ℕ) => 0

theorem NonMRR.catalogueVector_support (g : ℕ → ℕ) (n k : ℕ) (hk : k < g n) (i : ℕ) (hi : i ∉ blockInterval g n) : catalogueVector g n k i = 0

theorem NonMRR.catalogueVector_balance (g : ℕ → ℕ) (n k : ℕ) (hk : k < g n) : ∑ i ∈ blockInterval g n, catalogueVector g n k i = 0

theorem NonMRR.catalogueVector_mass (g : ℕ → ℕ) (n k : ℕ) (hk : k < g n) : 1 ≤ ∑ i ∈ blockInterval g n, ‖catalogueVector g n k i‖

theorem NonMRR.catalogueVector_bad_card (g : ℕ → ℕ) (π : Equiv.Perm ℕ) (n : ℕ) : (badValues (catalogueVector g) g π blockTolerance n).card ≤ blockCapacity n

noncomputable def NonMRR.walshCatalogue : BlockCatalogue blockCapacity blockTolerance

The explicit catalogue supplying all concrete data for the rearrangement construction. Its only choices select the finite Walsh families already proved to exist.

Equations

• One or more equations did not get rendered due to their size.