The mean number of k-local maxima of a random permutation

The k-local maxima of a permutation are the distinct values among the maxima of its windows of length k. Summed over the n! permutations, (k + 1) · Σ_σ #maxima = n! (2n − k + 1): the mean is (2n − k + 1)/(k + 1) (Theorem of the Day, after Austin–Fagen–Lehrer–Penney 1957). Proof: the window maximum changes between windows i − 1 and i exactly when the maximum of the block of k + 1 positions [i − 1, i + k − 1] sits at one of its ends, which by symmetry happens for 2 n!/(k + 1) permutations.

Main results

• LocalMaxima.card_image_windowMax: number of distinct window maxima = 1 + number of blocks whose maximum is at an end
• LocalMaxima.card_argmax_end: the maximum of a block of k + 1 positions is at an end for 2 n!/(k+1) permutations
• LocalMaxima.sum_card_windowMax: (k + 1) Σ_σ #k-local maxima = n! (2n − k + 1)

References

• R. Whitty, Theorem of the Day, «Distribution of local maxima in random samples» (Statistics/PermLocalMax).
• T. L. Austin, R. E. Fagen, T. A. Lehrer, W. F. Penney, The distribution of the number of locally maximal elements in a random sample, Ann. Math. Statist. 28 (1957).

def LocalMaxima.windowMax {n : ℕ} (σ : Equiv.Perm (Fin n)) (k i : ℕ) : ℕ

The maximum of the window [i, i + k) of σ (values as natural numbers).

Equations

• LocalMaxima.windowMax σ k i = (Finset.image (fun (j : Fin n) => ↑(σ j)) {j : Fin n | i ≤ ↑j ∧ ↑j < i + k}).sup id

def LocalMaxima.IsBlockMax {n : ℕ} (σ : Equiv.Perm (Fin n)) (a k : ℕ) (p : Fin n) : Prop

p is a position of the block [a, a + k] carrying the largest value of σ on the block.

Equations

• LocalMaxima.IsBlockMax σ a k p = (a ≤ ↑p ∧ ↑p ≤ a + k ∧ ∀ (j : Fin n), a ≤ ↑j → ↑j ≤ a + k → ↑(σ j) ≤ ↑(σ p))

def LocalMaxima.EndMax {n : ℕ} (σ : Equiv.Perm (Fin n)) (a k : ℕ) : Prop

The maximum of the block [a, a + k] of σ sits at one of its two ends.

Equations

• LocalMaxima.EndMax σ a k = ∃ (p : Fin n), (↑p = a ∨ ↑p = a + k) ∧ LocalMaxima.IsBlockMax σ a k p

theorem LocalMaxima.le_windowMax {n : ℕ} (σ : Equiv.Perm (Fin n)) (k i : ℕ) (j : Fin n) (h1 : i ≤ ↑j) (h2 : ↑j < i + k) : ↑(σ j) ≤ windowMax σ k i

theorem LocalMaxima.exists_windowMax {n : ℕ} (σ : Equiv.Perm (Fin n)) (k i : ℕ) (hk : 1 ≤ k) (hi : i + k ≤ n) : ∃ (j : Fin n), i ≤ ↑j ∧ ↑j < i + k ∧ ↑(σ j) = windowMax σ k i

theorem LocalMaxima.exists_blockMax {n : ℕ} (σ : Equiv.Perm (Fin n)) (a k : ℕ) (h : a + k < n) : ∃ (p : Fin n), IsBlockMax σ a k p

theorem LocalMaxima.windowMax_eq {n : ℕ} (σ : Equiv.Perm (Fin n)) (k i a : ℕ) (hk : 1 ≤ k) (hi : i + k ≤ n) (q : Fin n) (hq : IsBlockMax σ a k q) (h1 : a ≤ i) (h2 : i + k ≤ a + k + 1) (hq1 : i ≤ ↑q) (hq2 : ↑q < i + k) : windowMax σ k i = ↑(σ q)

theorem LocalMaxima.mem_image_iff {n : ℕ} (σ : Equiv.Perm (Fin n)) (k m : ℕ) (hk : 1 ≤ k) (hm : m + 1 + k ≤ n) : windowMax σ k (m + 1) ∈ Finset.image (windowMax σ k) (Finset.range (m + 1)) ↔ ¬EndMax σ m k

theorem LocalMaxima.card_image_range {n : ℕ} (σ : Equiv.Perm (Fin n)) (k : ℕ) (hk : 1 ≤ k) (m : ℕ) : m + k ≤ n → (Finset.image (windowMax σ k) (Finset.range (m + 1))).card = 1 + {a ∈ Finset.range m | EndMax σ a k}.card

theorem LocalMaxima.card_image_windowMax {n : ℕ} (σ : Equiv.Perm (Fin n)) (k : ℕ) (hk : 1 ≤ k) (hkn : k ≤ n) : (Finset.image (windowMax σ k) (Finset.range (n - k + 1))).card = 1 + {a ∈ Finset.range (n - k) | EndMax σ a k}.card

The number of distinct window maxima of σ is 1 + the number of blocks [a, a + k] (0 ≤ a < n - k) whose maximum sits at an end.

theorem LocalMaxima.isBlockMax_swap {n : ℕ} (σ : Equiv.Perm (Fin n)) (a k : ℕ) (p q : Fin n) (hp1 : a ≤ ↑p) (hp2 : ↑p ≤ a + k) (hq1 : a ≤ ↑q) (hq2 : ↑q ≤ a + k) (h : IsBlockMax σ a k p) : IsBlockMax (σ * Equiv.swap p q) a k q

theorem LocalMaxima.card_blockMax_eq {n : ℕ} (a k : ℕ) (p q : Fin n) (hp1 : a ≤ ↑p) (hp2 : ↑p ≤ a + k) (hq1 : a ≤ ↑q) (hq2 : ↑q ≤ a + k) : {σ : Equiv.Perm (Fin n) | IsBlockMax σ a k p}.card = {σ : Equiv.Perm (Fin n) | IsBlockMax σ a k q}.card

theorem LocalMaxima.card_block {n : ℕ} (a k : ℕ) (h : a + k < n) : {j : Fin n | a ≤ ↑j ∧ ↑j ≤ a + k}.card = k + 1

theorem LocalMaxima.card_blockMax_mul {n : ℕ} (a k : ℕ) (h : a + k < n) (p : Fin n) (hp1 : a ≤ ↑p) (hp2 : ↑p ≤ a + k) : {σ : Equiv.Perm (Fin n) | IsBlockMax σ a k p}.card * (k + 1) = n.factorial

The block maximum is uniformly distributed on the k + 1 positions of the block.

theorem LocalMaxima.card_argmax_end {n : ℕ} (a k : ℕ) (hk : 1 ≤ k) (h : a + k < n) : {σ : Equiv.Perm (Fin n) | EndMax σ a k}.card * (k + 1) = 2 * n.factorial

For a block [a, a + k] inside Fin n, the maximum is at an end for exactly 2 n! / (k + 1) permutations.

theorem LocalMaxima.sum_card_windowMax (n k : ℕ) (hk : 1 ≤ k) (hkn : k ≤ n) : (k + 1) * ∑ σ : Equiv.Perm (Fin n), (Finset.image (windowMax σ k) (Finset.range (n - k + 1))).card = n.factorial * (2 * n - k + 1)

Sum over permutations of the number of distinct window maxima.