theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.direct_alpha_mass_subpower (i : ℕ) {δ : ℝ} (hδ : 0 < δ) : ∃ (C : ℝ), 0 < C ∧ ∀ (x M : ℝ), 1 ≤ x → 1 ≤ M → 2 * M ≤ x → ∀ (U : Finset ℕ) (α : ℕ → ℝ), (∀ n ∈ U, M ≤ ↑n ∧ ↑n ≤ 2 * M) → (∀ n ∈ U, |α n| ≤ ↑((fouvryTau i) n)) → ∑ n ∈ U, α n ^ 2 ≤ C * M * x ^ δ

Actual outer alpha square sum, including divisor order zero, uniformly in support.