Scalar endgame, with every remaining input labelled. This is not the unconditional distribution theorem until the actual prefix producer is supplied.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.direct_error_scalar {M T x A J Y V P Cα Ccost Ccell δ η ε : ℝ} (hM : 0 ≤ M) (_hT : 0 ≤ T) (hx : 0 < x) (_hA : 0 ≤ A) (hJ : 0 ≤ J) (hY : 0 ≤ Y) (hV : 0 ≤ V) (hP : 0 ≤ P) (hCα : 0 ≤ Cα) (hCcost : 0 ≤ Ccost) (_hCcell : 0 ≤ Ccell) (hMT : x = 4 * M * T) (halpha : A ≤ Cα * M * x ^ δ) (hcost : J * Y * V ≤ Ccost * x ^ (12 * η + δ)) (hcell : P ≤ Ccell * T ^ 2 * x ^ (δ - ε / 2)) : 3072 * M * A * J * Y * V * P ≤ 192 * Cα * Ccost * Ccell * x ^ 2 * x ^ (12 * η + 3 * δ - ε / 2)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.direct_power_to_log (C : ℝ) (hC : 0 ≤ C) (A : ℕ) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (x : ℝ) in Filter.atTop, C * x ^ 2 * x ^ (-ε) ≤ x ^ 2 / Real.log x ^ A

Uniform power saving implies any requested logarithmic saving.