A discrete intermediate value theorem

A sequence of natural numbers that grows by at most one per step takes every value between its value at the start and any of its later values (Nat.exists_eq_of_forall_le_add_one). Compare SimpleGraph.Walk.mem_support_hasse_of_ge_of_le, the same fact for walks in the Hasse diagram of a linear order.

Similarly, if changing one coordinate of a function on a finite domain raises a natural-valued measure by at most B, and the measure starts at most t and ends above t, then it takes some intermediate value in (t, t + B] (Nat.exists_lt_le_add_of_update_le).

Main results

• Nat.exists_eq_of_forall_le_add_one: the discrete intermediate value theorem for sequences.
• Nat.exists_lt_le_add_of_update_le: discrete intermediate values under coordinate updates.

theorem Nat.exists_eq_of_forall_le_add_one {a : ℕ → ℕ} {k T : ℕ} (h0 : a 0 ≤ k) (hT : k ≤ a T) (hstep : ∀ t < T, a (t + 1) ≤ a t + 1) : ∃ t ≤ T, a t = k

A discrete intermediate value theorem. A sequence of natural numbers that grows by at most one per step up to time T takes, by time T, every value between a 0 and a T.

theorem Nat.exists_lt_le_add_of_update_le {ι : Type u_1} {α : Type u_2} [Finite ι] [DecidableEq ι] (μ : (ι → α) → ℕ) {B t : ℕ} (hμ : ∀ (w : ι → α) (i : ι) (a : α), μ (Function.update w i a) ≤ μ w + B) {u v : ι → α} (hu : μ u ≤ t) (hv : t < μ v) : ∃ (w : ι → α), t < μ w ∧ μ w ≤ t + B

Discrete intermediate values under coordinate updates. If changing one coordinate raises a measure by at most B, and the measure is at most t at u and above t at v, then it lies in (t, t + B] somewhere.