Uniform constants for the bounded decomposition iteration

noncomputable def EGZ.FlagDecomposition.Iteration.faceCapacity (d : ℕ) (ε : ℝ) : ℕ

A positive integer upper bound for face events on one surviving lineage.

Equations

• EGZ.FlagDecomposition.Iteration.faceCapacity d ε = max 1 ⌈(((ε / 2) ^ 3)⁻¹ + ↑d + 2) ^ (d + 2)⌉₊

theorem EGZ.FlagDecomposition.Iteration.one_le_faceCapacity (d : ℕ) (ε : ℝ) : 1 ≤ faceCapacity d ε

theorem EGZ.FlagDecomposition.Iteration.le_faceCapacity_of_real_le {d n : ℕ} {ε : ℝ} (h : ↑n ≤ (((ε / 2) ^ 3)⁻¹ + ↑d + 2) ^ (d + 2)) : n ≤ faceCapacity d ε

noncomputable def EGZ.FlagDecomposition.Iteration.intervalCapacity (d : ℕ) (ε : ℝ) (a : ℕ) : ℕ

Capacity of the interval beginning at a given iteration index.

Equations

• EGZ.FlagDecomposition.Iteration.intervalCapacity d ε a = 2 ^ a * EGZ.FlagDecomposition.Iteration.faceCapacity d ε

theorem EGZ.FlagDecomposition.Iteration.pow_le_intervalCapacity (d : ℕ) (ε : ℝ) (a : ℕ) : 2 ^ a ≤ intervalCapacity d ε a

theorem EGZ.FlagDecomposition.Iteration.one_le_intervalCapacity (d : ℕ) (ε : ℝ) (a : ℕ) : 1 ≤ intervalCapacity d ε a

noncomputable def EGZ.FlagDecomposition.Iteration.stoppingBound (d : ℕ) (ε : ℝ) : ℕ

Uniform stopping bound derived from the interval capacities.

Equations

• EGZ.FlagDecomposition.Iteration.stoppingBound d ε = EGZ.intervalCapacityBound (2 * (d + 1) ^ 2 + 1) (EGZ.FlagDecomposition.Iteration.intervalCapacity d ε)

theorem EGZ.FlagDecomposition.Iteration.stoppingBound_pos (d : ℕ) (ε : ℝ) : 0 < stoppingBound d ε

noncomputable def EGZ.FlagDecomposition.Iteration.finalScale (d : ℕ) (ε : ℝ) : ℝ

The scale at the uniform stopping bound of the decomposition iteration.

Equations

• EGZ.FlagDecomposition.Iteration.finalScale d ε = EGZ.FlagDecomposition.Iteration.stageScale d ε (EGZ.FlagDecomposition.Iteration.stoppingBound d ε)

theorem EGZ.FlagDecomposition.Iteration.finalScale_pos (d : ℕ) {ε : ℝ} (hε : 0 < ε) : 0 < finalScale d ε

theorem EGZ.FlagDecomposition.Iteration.finalScale_le {d i : ℕ} (hd : 1 ≤ d) {ε : ℝ} (hε : 0 < ε) (hi : i ≤ stoppingBound d ε) : finalScale d ε ≤ stageScale d ε i