theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayKMain_max_le {Cscale x : ℝ} (hscale : 1 ≤ Cscale) (hx : 1 ≤ x) (a : ℤ) (K : WExtractedKey) (F : ℕ) (j : Fin 5 → ℕ) (ha : ↑a.natAbs ≤ Cscale * x) (hd : ↑K.1.2.1 ≤ x) (hF : ↑F ≤ 2 * x) (hn : 2 ^ j 2 ≤ 2 * x) (hs : 2 ^ j 4 ≤ x) (hH : 2 ^ j 0 ≤ 32 * x ^ 7) : ↑(mainRestrictedMax a K.1.2.1 (2 ^ (j 2 + 1)) (F / K.1.1) (2 ^ (j 0 + 1)) (2 ^ (j 4 + 1))) ≤ 3072 * Cscale * x ^ 12

Only the arithmetic input is enlarged; all physical dyadic scales stay at x.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayKMain_abs_rpow_le {Cscale x δ : ℝ} (hscale : 1 ≤ Cscale) (hx : 0 ≤ x) (hδ : 0 ≤ δ) (a : ℤ) (ha : ↑a.natAbs ≤ Cscale * x) : ↑a.natAbs ^ δ ≤ Cscale ^ δ * x ^ δ

The first of the two arithmetic subpower losses at fixed multiplier Cscale.