theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayMain_root_identity {A m E T : ℝ} (hA : 0 ≤ A) (hm : 0 ≤ m) (hE : 0 ≤ E) : A * √m * √E / T ^ 2 = √(A ^ 2 * m * E / T ^ 4)

Exact transport of the real reciprocal and T² normalization under a root.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayMain_npow {n T p : ℝ} (hn : 0 ≤ n) (hT : 0 ≤ T) (hnT : n ≤ 2 * T) (hp : 0 ≤ p) (hp2 : p ≤ 2) : n ^ p ≤ 4 * T ^ p

An upper dyadic n endpoint is paid by a fixed factor two, not by n=T.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayMain_two_monomials {k n r s Dp Z T R S : ℝ} (hk : 0 ≤ k) (hn : 0 ≤ n) (hr : 0 ≤ r) (hs : 0 ≤ s) (hDp : 0 ≤ Dp) (hZ : 1 ≤ Z) (hT : 1 ≤ T) (hR : 1 ≤ R) (hS : 1 ≤ S) (hkRS : k ≤ R * S) (hnT : n ≤ 2 * T) (hrR : r ≤ R) (hsS : s ≤ S) (hDpZ : Dp ≤ Z ^ 5) : k * n ^ (3 / 2) * r ^ (5 / 2) * s ^ 3 * Dp + 2 * k ^ 2 * n ^ (1 / 2) * r ^ (3 / 2) * s ≤ 12 * Z ^ 5 * T ^ (3 / 2) * R ^ (7 / 2) * S ^ 4

Both long-interval and D' summands have nonnegative post-payment exponents.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayMain_square_expand {A C L H k n r s Dp T : ℝ} (hn : 0 < n) (hr : 0 < r) (hs : 0 < s) (hT : 0 < T) : A ^ 2 * (8 * C * k * r * T) * (256 * L * H ^ 2 * n ^ (3 / 2) * T ^ 2 * r ^ (3 / 2) * s ^ 3 * (Dp + 2 * k / (n * r * s ^ 2))) / T ^ 4 = 2048 * C * L * (A * H) ^ 2 / T * (k * n ^ (3 / 2) * r ^ (5 / 2) * s ^ 3 * Dp + 2 * k ^ 2 * n ^ (1 / 2) * r ^ (3 / 2) * s)

Exact squared normalization after the reciprocal, before floor payment. The second summand is the actual span/q contribution.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayMain_square_paid {A C L H k n r s Dp Z T R S x : ℝ} (hA : 0 ≤ A) (hC : 0 ≤ C) (hL : 0 ≤ L) (hH : 0 ≤ H) (hk : 0 < k) (hn : 0 < n) (hr : 0 < r) (hs : 0 < s) (hDp : 0 ≤ Dp) (hZ : 1 ≤ Z) (hT : 1 ≤ T) (hR : 1 ≤ R) (hS : 1 ≤ S) (hx : 0 < x) (hAH : A * H ≤ 32 * Z * T / x) (hkRS : k ≤ R * S) (hnT : n ≤ 2 * T) (hrR : r ≤ R) (hsS : s ≤ S) (hDpZ : Dp ≤ Z ^ 5) : A ^ 2 * (8 * C * k * r * T) * (256 * L * H ^ 2 * n ^ (3 / 2) * T ^ 2 * r ^ (3 / 2) * s ^ 3 * (Dp + 2 * k / (n * r * s ^ 2))) / T ^ 4 ≤ 25165824 * C * L * Z ^ 7 * T ^ (5 / 2) * R ^ (7 / 2) * S ^ 4 / x ^ 2

The real floor bound is substituted before all global enlargement.