Finite analytic estimates.

theorem NonMRR.walk_square_le {L j : ℕ} (S : ℕ → ℝ) {d : ℝ} (hd : 0 ≤ d) (h0 : S 0 = 0) (hL : S L = 0) (hstep : ∀ i < L, |S (i + 1) - S i| ≤ d) (hj : j ≤ L) : S j ^ 2 ≤ 2 * d * ∑ i ∈ Finset.range L, |S i|

A closed real walk with increments bounded by d has this energy bound.

theorem NonMRR.walk_fourth_le {L j : ℕ} (S : ℕ → ℝ) {d : ℝ} (hd : 0 ≤ d) (h0 : S 0 = 0) (hL : S L = 0) (hstep : ∀ i < L, |S (i + 1) - S i| ≤ d) (hj : j ≤ L) : S j ^ 4 ≤ 4 * d ^ 2 * ↑L * ∑ i ∈ Finset.range L, S i ^ 2

A fourth-moment estimate for one closed walk.

theorem NonMRR.walk_fourth_le_normalized {L j : ℕ} (hLpos : 0 < L) (S : ℕ → ℝ) (h0 : S 0 = 0) (hL : S L = 0) (hstep : ∀ i < L, |S (i + 1) - S i| ≤ 1 / ↑L) (hj : j ≤ L) : S j ^ 4 ≤ 4 / ↑L * ∑ i ∈ Finset.range L, S i ^ 2

The normalized version used for balanced sign vectors.

theorem NonMRR.sum_walk_fourth_le {ι : Type u_1} [Fintype ι] {L : ℕ} (hLpos : 0 < L) (S : ι → ℕ → ℝ) (h0 : ∀ (k : ι), S k 0 = 0) (hL : ∀ (k : ι), S k L = 0) (hstep : ∀ (k : ι), ∀ i < L, |S k (i + 1) - S k i| ≤ 1 / ↑L) (hprefix : ∀ i < L, ∑ k : ι, S k i ^ 2 ≤ 1) (j : ι → ℕ) (hj : ∀ (k : ι), j k ≤ L) : ∑ k : ι, S k (j k) ^ 4 ≤ 4

A family with prefix-square sums at most one has total fourth moment at most four, even when a different time is selected in each walk.

noncomputable def NonMRR.badWalks {ι : Type u_1} [Fintype ι] (S : ι → ℕ → ℝ) (L q : ℕ) : Finset ι

The walks that at some time exceed the threshold 1/q.

Equations

• NonMRR.badWalks S L q = {k : ι | ∃ j ≤ L, 1 / ↑q < |S k j|}

theorem NonMRR.card_badWalks_le {ι : Type u_1} [Fintype ι] {L q : ℕ} (hLpos : 0 < L) (hqpos : 0 < q) (S : ι → ℕ → ℝ) (h0 : ∀ (k : ι), S k 0 = 0) (hL : ∀ (k : ι), S k L = 0) (hstep : ∀ (k : ι), ∀ i < L, |S k (i + 1) - S k i| ≤ 1 / ↑L) (hprefix : ∀ i < L, ∑ k : ι, S k i ^ 2 ≤ 1) : (badWalks S L q).card ≤ 4 * q ^ 4

The finite counting estimate, in terms of the prefix walks.