Local finiteness of the cutoff families.

FILES 11-14: local finiteness of the cutoff families (why every tsum below is a finite

sum, no junk value). INFRA helper + FILE 11-14 [PROVED, characterizations].

theorem AVenhance.finite_lattice_near {τ : ℝ} (hτ : 0 < τ) (t ρ : ℝ) : {l : ℤ | |t - ↑l * τ| ≤ ρ}.Finite

INFRA (private helper, Infra/Ingredients/LatticeNear.lean).

theorem AVenhance.indIcc_eq_zero_of_not_mem {a b t : ℝ} (h : t ∉ Set.Icc a b) : indIcc a b t = 0

theorem AVenhance.indIcc_nonneg' (a b t : ℝ) : 0 ≤ indIcc a b t

theorem AVenhance.Ingredients.tau_pos' {β : ℝ} (I : Ingredients β) (m : ℕ) : 0 < tau β I.Λ m

theorem AVenhance.Ingredients.tauPP_pos' {β : ℝ} (I : Ingredients β) (m : ℕ) : 0 < tauPP β I.Λ m

theorem AVenhance.Ingredients.xiMK_support_finite {β : ℝ} (I : Ingredients β) (m : ℕ) (t : ℝ) : {k : ℤ | I.xiMK m k t ≠ 0}.Finite

{k | ξ_{m,k}(t) ≠ 0} is finite.

theorem AVenhance.Ingredients.zetaMK_support_finite {β : ℝ} (I : Ingredients β) (m : ℕ) (t : ℝ) : {k : ℤ | I.zetaMK m k t ≠ 0}.Finite

{k | ζ_{m,k}(t) ≠ 0} is finite.

theorem AVenhance.Ingredients.hatZetaML_support_finite {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (t : ℝ) : {l : ℤ | I.hatZetaML m l t ≠ 0}.Finite

{l | ζ̂_{m,l}(t) ≠ 0} is finite.

theorem AVenhance.Ingredients.hatXiML_support_finite {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (t : ℝ) : {l : ℤ | I.hatXiML m l t ≠ 0}.Finite

{l | ξ̂_{m,l}(t) ≠ 0} is finite.