Embedding finite vectors into series.

theorem NonMRR.exists_strictMono_perm {L : ℕ} (f : Fin L → ℕ) (hf : Function.Injective f) : ∃ (σ : Equiv.Perm (Fin L)), StrictMono (f ∘ ⇑σ)

A finite injective sequence can be ordered by a permutation of its labels.

theorem NonMRR.strictMono_cut {L : ℕ} (f : Fin L → ℕ) (hf : StrictMono f) (j : ℕ) : ∃ r ≤ L, ∀ (i : Fin L), f i < j ↔ ↑i < r

A cut through an increasing finite sequence is an initial segment of its labels.

def NonMRR.embedVector {L : ℕ} (e : Fin L ↪ ℕ) (v : Fin L → ℝ) (i : ℕ) : ℝ

Put a finite vector on an arbitrary injectively labelled subset of the naturals.

Equations

• NonMRR.embedVector e v i = ∑ k : Fin L, if e k = i then v k else 0

theorem NonMRR.rearrangedPartialSum_embedVector {L : ℕ} (e : Fin L ↪ ℕ) (v : Fin L → ℝ) (π : Equiv.Perm ℕ) (j : ℕ) : rearrangedPartialSum (embedVector e v) π j = ∑ k : Fin L with (Equiv.symm π) (e k) < j, v k

theorem NonMRR.exists_perm_embedVector_prefix {L : ℕ} (e : Fin L ↪ ℕ) (π : Equiv.Perm ℕ) : ∃ (σ : Equiv.Perm (Fin L)), ∀ (j : ℕ), ∃ r ≤ L, ∀ (v : Fin L → ℝ), rearrangedPartialSum (embedVector e v) π j = vectorPrefix (v ∘ ⇑σ) r

A permutation visits a finite support in one fixed finite ordering. Each global partial sum is a prefix of that ordering, with the same cut for every vector.

@[simp]

theorem NonMRR.embedVector_apply {L : ℕ} (e : Fin L ↪ ℕ) (v : Fin L → ℝ) (k : Fin L) : embedVector e v (e k) = v k

theorem NonMRR.embedVector_eq_zero {L : ℕ} (e : Fin L ↪ ℕ) (v : Fin L → ℝ) (i : ℕ) (hi : i ∉ Finset.image (⇑e) Finset.univ) : embedVector e v i = 0

theorem NonMRR.sum_embedVector {L : ℕ} (e : Fin L ↪ ℕ) (v : Fin L → ℝ) : ∑ i ∈ Finset.image (⇑e) Finset.univ, embedVector e v i = ∑ k : Fin L, v k

theorem NonMRR.sum_norm_embedVector {L : ℕ} (e : Fin L ↪ ℕ) (v : Fin L → ℝ) : ∑ i ∈ Finset.image (⇑e) Finset.univ, ‖embedVector e v i‖ = ∑ k : Fin L, ‖v k‖

theorem NonMRR.sum_norm_embedVector_eq_one {L : ℕ} (hL : 0 < L) (e : Fin L ↪ ℕ) (v : Fin L → ℝ) (habs : ∀ (k : Fin L), |v k| = 1 / ↑L) : ∑ i ∈ Finset.image (⇑e) Finset.univ, ‖embedVector e v i‖ = 1

theorem NonMRR.card_bad_embedVector_le {m L q : ℕ} (e : Fin L ↪ ℕ) (v : Fin m → Fin L → ℝ) (hbad : ∀ (σ : Equiv.Perm (Fin L)), {k : Fin m | ∃ r ≤ L, 1 / ↑q < |vectorPrefix (v k ∘ ⇑σ) r|}.card ≤ 4 * q ^ 4) (π : Equiv.Perm ℕ) : {k : Fin m | ∃ (j : ℕ), 1 / ↑q < ‖rearrangedPartialSum (embedVector e (v k)) π j‖}.card ≤ 4 * q ^ 4

The finite counting bound is unchanged when the coordinates are put on any finite subset of the naturals and visited by an arbitrary infinite permutation.

theorem NonMRR.card_bad_embedVector_two_orders_le {m L q : ℕ} (e : Fin L ↪ ℕ) (v : Fin m → Fin L → ℝ) (hbad : ∀ (σ : Equiv.Perm (Fin L)), {k : Fin m | ∃ r ≤ L, 1 / ↑q < |vectorPrefix (v k ∘ ⇑σ) r|}.card ≤ 4 * q ^ 4) (π : Equiv.Perm ℕ) : {k : Fin m | (∃ (j : ℕ), 1 / ↑q < ‖rearrangedPartialSum (embedVector e (v k)) (Equiv.refl ℕ) j‖) ∨ ∃ (j : ℕ), 1 / ↑q < ‖rearrangedPartialSum (embedVector e (v k)) π j‖}.card ≤ 8 * q ^ 4

The union of the exceptional values in the natural and permuted orders has cardinality at most 8*q^4.