Bounds after restarting and stopping a finite interval

theorem EGZ.FlagDecomposition.Iteration.card_filter_range_offset (χ : ℕ → ℕ) (a b l : ℕ) (hab : a ≤ b) : {i ∈ Finset.range (b + 1 - a) | χ (a + i) = l}.card = {i ∈ Finset.Icc a b | χ i = l}.card

theorem EGZ.FlagDecomposition.Iteration.intervalState_mass_tail {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {s : ℕ → State p d f} {ε : ℝ} {a n N : ℕ} (hbound : a + n ≤ N) (htail : ∀ (i j : ℕ), i ≤ j → j ≤ N → ↑(s i).decomposition.retainedMass - ↑(s j).decomposition.retainedMass ≤ ε ^ 2 / 4 * ↑(s i).decomposition.retainedMass) (i j : ℕ) (hij : i ≤ j) : ↑(intervalState s a n i).decomposition.retainedMass - ↑(intervalState s a n j).decomposition.retainedMass ≤ ε ^ 2 / 4 * ↑(intervalState s a n i).decomposition.retainedMass

theorem EGZ.FlagDecomposition.Iteration.intervalState_zero {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (s : ℕ → State p d f) (a n : ℕ) : intervalState s a n 0 = s a