theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPaySecondary_n_bound {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {T : ℝ} (hNT : ∀ n ∈ N, ↑n ≤ 2 * T) {a : ℤ} {P : WOriginalTuple → Prop} {R S ξ : ℝ} {b : ℕ} {K : WExtractedKey} {j : Fin 5 → ℕ} {positive : Bool} {t : WExtractedTuple × ℤ} (ht : t ∈ wAnalyticDyadicBlock (wExtractedKeyFiber H N Q a P R S ξ b K) j positive) : 2 ^ j 2 ≤ 2 * T

The beta coordinate is n₁, not silently T.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPaySecondary_growth_data {x η M T R S : ℝ} (hx : 4 ≤ x) (_hη : 0 ≤ η) (hη1 : η ≤ 1) (hM : 1 ≤ M) (hT : 1 ≤ T) (hxMT : x = 4 * M * T) (hR : 1 ≤ R) (hS : 1 ≤ S) (hRS : R * S ≤ x) {N : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hNT : ∀ n ∈ N, ↑n ≤ 2 * T) {a : ℤ} (ha : |↑a| ≤ x) {F : ℕ} (hF : ↑F ≤ 2 * T) {K : WExtractedKey} (hK : K ∈ wExtractedKeyBox (x ^ η)) {j : Fin 5 → ℕ} {positive : Bool} {b : ℕ} {t : WExtractedTuple × ℤ} (ht : t ∈ wAnalyticDyadicBlock (wExtractedKeyFiber (wFloorCutoff M (x ^ η)) N (Finset.Ioc 0 ⌊R * S⌋₊) a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K) j positive) : 2 ^ j 0 ≤ 8 * x ^ 6 ∧ ↑(wGramSecondaryNumeratorMax a K F j) ≤ 16 * x ^ 9 ∧ 16 * 2 ^ j 2 * 2 ^ j 3 * 2 ^ j 4 * 2 ^ j 4 ≤ 16 * x ^ 4

Coarse polynomial growth is used only for small powers and logarithms.