Bounded changes on a Boolean cube

A bound for changing one coordinate extends to the ordinary, unnormalized Hamming distance. It also gives a discrete intermediate-value theorem: a natural-valued function on a finite Boolean cube cannot skip an interval wider than its one-coordinate bound. Neither conclusion assumes monotonicity.

theorem Algebraic.BooleanCube.update_induction {ι : Type u_1} [Fintype ι] [DecidableEq ι] (start finish : ι → Bool) (P : (ι → Bool) → Prop) (initial : P start) (step : ∀ (vector : ι → Bool) (index : ι) (value : Bool), P vector → P (Function.update vector index value)) : P finish

Every Boolean vector is reachable from any other by coordinate updates.

theorem Algebraic.BooleanCube.le_add_mul_hammingDist {ι : Type u_1} [Fintype ι] [DecidableEq ι] (measure : (ι → Bool) → ℕ) (bound : ℕ) (step : ∀ (vector : ι → Bool) (index : ι) (value : Bool), measure (Function.update vector index value) ≤ measure vector + bound) (start finish : ι → Bool) : measure finish ≤ measure start + bound * hammingDist start finish

A one-coordinate upper bound extends to Hamming distance.

theorem Algebraic.BooleanCube.dist_le_mul_hammingDist {ι : Type u_1} [Fintype ι] [DecidableEq ι] (measure : (ι → Bool) → ℕ) (bound : ℕ) (step : ∀ (vector : ι → Bool) (index : ι) (value : Bool), measure (Function.update vector index value) ≤ measure vector + bound) (start finish : ι → Bool) : (measure start).dist (measure finish) ≤ bound * hammingDist start finish

The symmetric form of the Hamming Lipschitz bound, using natural distance.

theorem Algebraic.BooleanCube.exists_between {ι : Type u_1} [Fintype ι] [DecidableEq ι] (measure : (ι → Bool) → ℕ) (bound threshold : ℕ) (step : ∀ (vector : ι → Bool) (index : ι) (value : Bool), measure (Function.update vector index value) ≤ measure vector + bound) (start finish : ι → Bool) (below : measure start ≤ threshold) (above : threshold < measure finish) : ∃ (vector : ι → Bool), threshold < measure vector ∧ measure vector ≤ threshold + bound

Discrete intermediate values on a Boolean cube. The first threshold crossing overshoots by at most the one-coordinate bound.