Pointwise consequences of the large-scale cutoff requirements.

theorem AVenhance.Infra.Ingredients.CutoffConsequences.indIcc_nonneg (a b t : ℝ) : 0 ≤ indIcc a b t

theorem AVenhance.Infra.Ingredients.CutoffConsequences.indIcc_le_one (a b t : ℝ) : indIcc a b t ≤ 1

theorem AVenhance.Infra.Ingredients.hatXiML_partition {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (t : ℝ) : ∑' (l : ℤ), I.hatXiML m l t = 1

e.hatxi.partition (1345-1347): the translated ξ̂ functions sum to one.

theorem AVenhance.Infra.Ingredients.hatXiML_mem_Icc {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (l : ℤ) (t : ℝ) : I.hatXiML m l t ∈ Set.Icc 0 1

e.hatxi.partition and e.zeta.prime.ml.fitting (1327-1347): each translated ξ̂ cutoff lies between zero and one.

theorem AVenhance.Infra.Ingredients.hatZetaML_nonneg {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (l : ℤ) (t : ℝ) : 0 ≤ I.hatZetaML m l t

e.zeta.prime.ml.fitting (1327-1334): each translated ζ̂ cutoff is nonnegative.