theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPaySecondary_scalar {D d k n r s H Z x T R S m E : ℝ} (hD : 1 ≤ D) (hd : 0 ≤ d) (hdZ : d ≤ Z ^ 5) (hk : 0 < k) (hn : 0 < n) (hr : 0 < r) (hs : 0 < s) (hZ : 1 ≤ Z) (hx : 0 < x) (hT : 1 ≤ T) (hR : 1 ≤ R) (hS : 1 ≤ S) (hm : 0 ≤ m) (hE : 0 ≤ E) (hkRS : k ≤ R * S) (hnT : n ≤ 2 * T) (hrR : r ≤ R) (hsS : s ≤ S) (hH : H ≤ 32 * D * k * r * s * Z * T / x) : (D * k * r * s)⁻¹ ^ 2 * (m * (8 * k * r * T)) * (E * H * n ^ 2 * T ^ 2 * r * √r * s ^ 3 * (d + 2 * k / (n * r * s * s))) / T ^ 4 ≤ 2048 * E * m * Z ^ 6 * T ^ 2 * R * √R * S ^ 3 / x

Both section-length contributions are paid after the original reciprocal. The second summand is never bounded by the first local summand.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPaySecondary_root_of_sq {A mass energy U T B : ℝ} (hA : 0 ≤ A) (hm : 0 ≤ mass) (hU : 0 ≤ U) (hB : 0 ≤ B) (he : energy ≤ U) (hb : A ^ 2 * mass * U / T ^ 4 ≤ B ^ 2) : A * √mass * √energy / T ^ 2 ≤ B

Root extraction is monotone even if the original energy is totalized below zero.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPaySecondary_body_sq {x R S T : ℝ} (hx : 0 ≤ x) (hR : 0 < R) (hS : 0 ≤ S) : (T * R ^ (3 / 4) * S ^ (3 / 2) / √x) ^ 2 = T ^ 2 * R * √R * S ^ 3 / x

Exact square of the requested secondary body.