theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directJoinedSecondary_uniform {κ δ ρ η Cnonzero Csecondary Ccoeff Couter : ℝ} (hκ : 0 ≤ κ) (hδ : 0 < δ) (hρ : 0 ≤ ρ) (hη : 0 ≤ η) (hη1 : η ≤ 1) (hC : 0 ≤ Cnonzero) (hCsec : 0 ≤ Csecondary) (hCo : 0 ≤ Couter) : ∃ (C : ℝ), 0 < C ∧ ∀ (x M T R S : ℝ), 4 ≤ x → 1 ≤ M → 1 ≤ T → x = 4 * M * T → 1 ≤ R → 1 ≤ S → R * S ≤ x → ∀ (N : Finset ℕ), (∀ n ∈ N, 0 < n) → (∀ n ∈ N, ↑n ≤ 2 * T) → ∀ (a : ℤ), |↑a| ≤ x → ∀ (F : ℕ), ↑F ≤ 2 * T → ∀ K ∈ wExtractedKeyBox (x ^ η), ∀ (j cap : Fin 5 → ℕ) (positive : Bool) (b : ℕ), ∀ t ∈ wAnalyticDyadicBlock (wExtractedKeyFiber (wFloorCutoff M (x ^ η)) N (Finset.Ioc 0 ⌊R * S⌋₊) a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K) j positive, wBlockAmplitude K j * √(directJoinedMass ρ Couter x T j) * √(directJoinedSecondary κ δ ρ Cnonzero Csecondary Ccoeff x a R S K F j cap) / T ^ 2 ≤ C * x ^ (100 * (κ + δ + ρ + η)) * (T * R ^ (3 / 4) * S ^ (3 / 2) / √x)

Uniform payment of the actual joined secondary term. The constant is selected before x, all scales, the family, the signed shift, keys and dyadic data.