Limits along block-density ultrafilters

A free ultrafilter cannot remain in finitely many finite blocks. Consequently the block label of an ultrafilter-generic position tends to infinity. This turns the vanishing geometric error on a retained member of the ultrafilter into convergence to zero in the circle.

theorem Wallace.tendsto_blockOf_atTop (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) {p : Ultrafilter ℕ} (hp : ↑p ≤ Filter.cofinite) : Filter.Tendsto (TriangularPreprocess.blockOf N hN) (↑p) Filter.atTop

Along a free ultrafilter, the label of the finite block containing n tends to infinity.

theorem Wallace.tendsto_stageError_blockOf (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) {p : Ultrafilter ℕ} (hp : ↑p ≤ Filter.cofinite) : Filter.Tendsto (fun (n : ℕ) => FusionSchedule.stageError (TriangularPreprocess.blockOf N hN n)) (↑p) (nhds 0)

The scheduled error evaluated at the block label tends to zero along every free ultrafilter.

theorem Wallace.tendsto_zero_of_norm_le_stageError_on_mem (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) {p : Ultrafilter ℕ} (hp : ↑p ≤ Filter.cofinite) {f : ℕ → UnitAddCircle} {U : Set ℕ} (hU : U ∈ p) (hbound : ∀ n ∈ U, ‖f n‖ ≤ 2 * FusionSchedule.stageError (TriangularPreprocess.blockOf N hN n)) : Filter.Tendsto f (↑p) (nhds 0)

If a circle-valued sequence is bounded by twice the scheduled error on a member of a free ultrafilter, then it converges to zero along that ultrafilter.