theorem AnalyticNumberTheory.LargeSieve.pointwiseSW_horizontal_le_tail {X ε T Q L : ℝ} (hX : 0 ≤ X) (hε : 0 < ε) (hT : 0 < T) (hQ : Q ≤ T) : Q * X / (ε * (1 + T ^ 2)) ≤ X * (1 + L ^ 2) / (ε * T)

A horizontal error with coefficient at most the height is paid by the tail budget.