Combining the three event capacities #
noncomputable def
EGZ.FlagDecomposition.Iteration.progressColor
{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)
(i : ℕ)
:
Colors outside the finite run are arbitrary and never used.
Equations
Instances For
theorem
EGZ.FlagDecomposition.Iteration.hasIntervalCapacity_of_event_bounds
{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)
(hδ : Antitone δ)
(hδnonneg : ∀ (i : ℕ), 0 ≤ δ i)
(hcomplete :
∀ (a b L : ℕ),
a ≤ b →
b < N →
L < (d + 1) ^ 2 →
(∀ i ∈ Finset.Icc a b, 2 * L ≤ progressColor P i) →
{i ∈ Finset.Icc a b | progressColor P i = 2 * L}.card ≤ 2 ^ a)
(hface :
∀ (a b L : ℕ),
a ≤ b →
b < N →
L < (d + 1) ^ 2 →
(∀ i ∈ Finset.Icc a b, 2 * L + 1 ≤ progressColor P i) →
{i ∈ Finset.Icc a b | progressColor P i = 2 * L + 1}.card ≤ intervalCapacity d ε a)
:
HasIntervalCapacity (progressColor P) (intervalCapacity d ε) N
Complete and face event bounds, together with the checked gap bound, give precisely the interval-capacity hypothesis of the finite-color lemma.
theorem
EGZ.FlagDecomposition.Iteration.length_lt_stoppingBound_of_event_bounds
{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)
(hδ : Antitone δ)
(hδnonneg : ∀ (i : ℕ), 0 ≤ δ i)
(hcomplete :
∀ (a b L : ℕ),
a ≤ b →
b < N →
L < (d + 1) ^ 2 →
(∀ i ∈ Finset.Icc a b, 2 * L ≤ progressColor P i) →
{i ∈ Finset.Icc a b | progressColor P i = 2 * L}.card ≤ 2 ^ a)
(hface :
∀ (a b L : ℕ),
a ≤ b →
b < N →
L < (d + 1) ^ 2 →
(∀ i ∈ Finset.Icc a b, 2 * L + 1 ≤ progressColor P i) →
{i ∈ Finset.Icc a b | progressColor P i = 2 * L + 1}.card ≤ intervalCapacity d ε a)
: