Equal neighbors and index-sum bounds in finite arrays

A repeated value in a monotone finite array has an equal predecessor or successor. The value type needs only a partial order. Also bounds the sum of all indices in Fin n by n * n.

Main results

• Fin.exists_ne_apply_eq_iff_adjacent: an adjacent witness suffices for any repeated value.
• Fin.exists_adjacent_ne_of_monotone_comp: two distinct entries with equal keys in a monotone-key array force an adjacent pair of distinct entries with that key.
• Fin.sum_val_le_mul_self: (∑ j : Fin n, j.val) ≤ n * n.

References

• Adapted from MassProduction/Nonuniform/AdjacentDuplicates.lean in S. Schlesinger, Boolean circuit mass production formalization.
• Adapted from lean/Proofs/{Collisions,Selection}.lean in S. Schlesinger, Square-root circuit bounds for iterated functions.
• [OAI26a]

theorem Fin.exists_ne_apply_eq_iff_adjacent {α : Type u_1} [PartialOrder α] {count : ℕ} (f : Fin count → α) (ordered : Monotone f) (i : Fin count) : (∃ (j : Fin count), j ≠ i ∧ f j = f i) ↔ (∃ (positive : 0 < ↑i), f ⟨↑i - 1, ⋯⟩ = f i) ∨ ∃ (fits : ↑i + 1 < count), f ⟨↑i + 1, fits⟩ = f i

In a monotone finite array, every repeated value has an equal neighbor.

theorem Fin.exists_adjacent_ne_of_monotone_comp {α : Type u_1} {β : Type u_2} [PartialOrder β] {R : ℕ} (records : Fin R → α) (key : α → β) (hs : Monotone (key ∘ records)) (i j : Fin R) (hij : i < j) (hne : records i ≠ records j) (heq : key (records i) = key (records j)) : ∃ (p : ℕ) (hp : p + 1 < R), records ⟨p, ⋯⟩ ≠ records ⟨p + 1, hp⟩ ∧ key (records ⟨p, ⋯⟩) = key (records ⟨p + 1, hp⟩) ∧ key (records ⟨p, ⋯⟩) = key (records i)

In a finite array with monotone keys, two different records with equal keys force an adjacent pair of different records with that key.

theorem Fin.sum_val_le_mul_self (n : ℕ) : ∑ j : Fin n, ↑j ≤ n * n

The sum of all values in Fin n is at most n * n.