Growth functions for completeness refinements

One step of the width sequence dominates the requested width after changing to the bounded lattice coordinates. The same sequence bounds every possible number of added directions up to the ambient dimension.

def EGZ.refinementGrowth (A g : ℕ → ℕ) (n : ℕ) : ℕ

The next refinement bound, chosen above both the current index and the prescribed growth at A n.

Equations

• EGZ.refinementGrowth A g n = max (n + 1) (g (A n))

theorem EGZ.refinementGrowth_isGrowing {A g : ℕ → ℕ} (hA : Monotone A) (hg : Monotone g) : IsGrowing (refinementGrowth A g)

def EGZ.refinementWidth (A g : ℕ → ℕ) (K i : ℕ) : ℕ

The width after i iterations of the refinement growth function starting at K.

Equations

• EGZ.refinementWidth A g K i = (EGZ.refinementGrowth A g)^[i] K

@[simp]

theorem EGZ.refinementWidth_zero (A g : ℕ → ℕ) (K : ℕ) : refinementWidth A g K 0 = K

theorem EGZ.refinementWidth_succ (A g : ℕ → ℕ) (K i : ℕ) : refinementWidth A g K (i + 1) = refinementGrowth A g (refinementWidth A g K i)

theorem EGZ.refinementWidth_mono (A g : ℕ → ℕ) (K : ℕ) : Monotone (refinementWidth A g K)

theorem EGZ.le_refinementWidth (A g : ℕ → ℕ) (K i : ℕ) : K ≤ refinementWidth A g K i

theorem EGZ.desired_width_le_refinementWidth_succ (A g : ℕ → ℕ) (K i : ℕ) : g (A (refinementWidth A g K i)) ≤ refinementWidth A g K (i + 1)

theorem EGZ.refinementWidth_le_of_index_le (A g : ℕ → ℕ) (K : ℕ) {i d : ℕ} (hi : i ≤ d) : refinementWidth A g K i ≤ refinementWidth A g K d

theorem EGZ.refinementWidth_mono_initial {A g : ℕ → ℕ} (hA : Monotone A) (hg : Monotone g) (i : ℕ) : Monotone fun (K : ℕ) => refinementWidth A g K i