theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalytic_phase_budget_kscale {v : WGCDData} {q r N₁ N₂ : ℕ} (hv : v.Valid q r N₁ N₂) {Cscale M T x u : ℝ} (hC : 1 ≤ Cscale) (hM : 0 ≤ M) (hT : 0 < T) (hNT : T ≤ ↑N₁) (hx : x = 4 * M * T) {a : ℤ} (ha : |↑a| ≤ Cscale * x) (hu : |u| ≤ 3 * M) (h : ℤ) : |↑h| * (|u| / ↑(v.D * v.k₁ * v.k₂) + |↑a| / ↑(v.n₁ * v.k₁ * v.k₂ * v.D')) ≤ (3 + 4 * Cscale) * M * |↑h| / ↑(q.lcm r)