Uniform termination of certified finite refinement runs #
theorem
EGZ.FlagDecomposition.Iteration.hasIntervalCapacity
{p d : ℕ}
[NeZero p]
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
{s : ℕ → State p d f}
{ε : ℝ}
{δ : ℕ → ℝ}
{g : ℕ → ℕ}
{N : ℕ}
(P : (i : ℕ) → i < N → Progress (s i) (s (i + 1)) ε (δ i) g)
(hp : Odd p)
(hε : 0 < ε)
(hεhalf : ε ≤ 1 / 2)
(hδ : Antitone δ)
(hδnonneg : ∀ (i : ℕ), 0 ≤ δ i)
(hcard : ∀ i ≤ N, Fintype.card (s i).decomposition.flag.Node ≤ 2 ^ i)
(htail :
∀ (i j : ℕ),
i ≤ j →
j ≤ N →
↑(s i).decomposition.retainedMass - ↑(s j).decomposition.retainedMass ≤ ε ^ 2 / 4 * ↑(s i).decomposition.retainedMass)
:
HasIntervalCapacity (progressColor P) (intervalCapacity d ε) N
theorem
EGZ.FlagDecomposition.Iteration.length_lt_stoppingBound
{p d : ℕ}
[NeZero p]
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
{s : ℕ → State p d f}
{ε : ℝ}
{δ : ℕ → ℝ}
{g : ℕ → ℕ}
{N : ℕ}
(P : (i : ℕ) → i < N → Progress (s i) (s (i + 1)) ε (δ i) g)
(hp : Odd p)
(hε : 0 < ε)
(hεhalf : ε ≤ 1 / 2)
(hδ : Antitone δ)
(hδnonneg : ∀ (i : ℕ), 0 ≤ δ i)
(hcard : ∀ i ≤ N, Fintype.card (s i).decomposition.flag.Node ≤ 2 ^ i)
(htail :
∀ (i j : ℕ),
i ≤ j →
j ≤ N →
↑(s i).decomposition.retainedMass - ↑(s j).decomposition.retainedMass ≤ ε ^ 2 / 4 * ↑(s i).decomposition.retainedMass)
: