theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.kClean_smooth_error_scale_product_le {x M T L : ℝ} (hx : 0 < x) (hT : 0 ≤ T) (hL : 0 ≤ L) (hMT : M * T ≤ x) (hTx : T ≤ 2 * x ^ (1 / 9)) (hLx : L ≤ x ^ (5 / 9)) : M * T ^ 2 * L ≤ 2 * x ^ (5 / 3)

The higher short-variable endpoint leaves a full one-third power saving.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.kClean_alpha_sq_mul_smooth_envelopes_le_c2 {i k j : ℕ} (hi : 1 ≤ i) (hk : 1 ≤ k) (hj : 1 ≤ j) {x M T L : ℝ} (hx : 1 ≤ x) (hM : 1 ≤ M) (hT : 1 ≤ T) (hL : 1 ≤ L) (hMT : M * T ≤ x) (hTx : T ≤ 2 * x ^ (1 / 9)) (hLx : L ≤ x ^ (5 / 9)) (S N Q : Finset ℕ) (hS : ∀ m ∈ S, M ≤ ↑m ∧ ↑m ≤ 2 * M) (hN : N ⊆ Finset.Ioc 0 ⌊T⌋₊) (hQ : Q ⊆ Finset.Ioc 0 ⌊L⌋₊) (α β c : ℕ → ℝ) (hα : ∀ m ∈ S, |α m| ≤ ↑((fouvryTau i) m)) (hβ : ∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) (hc : ∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) (a : ℤ) : (∑ m ∈ S, α m ^ 2) * (smoothUErrorEnvelope N Q β c a + smoothVErrorEnvelope N Q β c a) ≤ 8 * x ^ (5 / 3) * (1 + Real.log (2 * x)) ^ (i ^ 2 - 1 + 2 * (k - 1) + 8 * j)

Simultaneous payment of the actual two envelopes after the unrestricted fixed-order alpha second moment. All three orders and the residue are retained.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.kClean_eventually_smooth_error_log_payment (K A : ℕ) {C : ℝ} (hC : 0 ≤ C) : ∀ᶠ (x : ℝ) in Filter.atTop, C * x ^ (5 / 3) * (1 + Real.log (2 * x)) ^ K ≤ x ^ 2 / Real.log x ^ A

Every fixed logarithm loss is absorbed by the explicit 1/3 polynomial slack. The constant may depend on the fixed orders, not on x.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.kClean_alpha_sq_mul_smooth_envelopes_c2_log_payment {i k j : ℕ} (hi : 1 ≤ i) (hk : 1 ≤ k) (hj : 1 ≤ j) (A : ℕ) {C : ℝ} (hC : 0 ≤ C) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (M T L : ℝ), 1 ≤ M → 1 ≤ T → 1 ≤ L → M * T ≤ x → T ≤ 2 * x ^ (1 / 9) → L ≤ x ^ (5 / 9) → ∀ (S N Q : Finset ℕ), (∀ m ∈ S, M ≤ ↑m ∧ ↑m ≤ 2 * M) → N ⊆ Finset.Ioc 0 ⌊T⌋₊ → Q ⊆ Finset.Ioc 0 ⌊L⌋₊ → ∀ (α β c : ℕ → ℝ), (∀ m ∈ S, |α m| ≤ ↑((fouvryTau i) m)) → (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → (∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) → ∀ (a : ℤ), C * ((∑ m ∈ S, α m ^ 2) * (smoothUErrorEnvelope N Q β c a + smoothVErrorEnvelope N Q β c a)) ≤ x ^ 2 / Real.log x ^ A

Uniform logarithmic payment after alpha L2 on the growing C.2 domains. The threshold is chosen before every scale, support, signed coefficient, and integer residue. In particular, a may vary freely with x.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.kClean_dispersionUV_smooth_c2_log_payment {i k j : ℕ} (hi : 1 ≤ i) (hk : 1 ≤ k) (hj : 1 ≤ j) (A : ℕ) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (M T L : ℝ), 1 ≤ M → 1 ≤ T → 1 ≤ L → M * T ≤ x → T ≤ 2 * x ^ (1 / 9) → L ≤ x ^ (5 / 9) → ∀ (S P N Q : Finset ℕ), (∀ m ∈ S, M ≤ ↑m ∧ ↑m ≤ 2 * M) → (∀ (m : ℕ), scaledDyadicCutoff M ↑m ≠ 0 → m ∈ P) → N ⊆ Finset.Ioc 0 ⌊T⌋₊ → Q ⊆ Finset.Ioc 0 ⌊L⌋₊ → ∀ (α β c : ℕ → ℝ), (∀ m ∈ S, |α m| ≤ ↑((fouvryTau i) m)) → (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → (∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) → ∀ (a : ℤ), (∑ m ∈ S, α m ^ 2) * (|dispersionU P N Q (fun (m : ℕ) => scaledDyadicCutoff M ↑m) β c a - smoothUMain M N Q β c a| + 2 * |dispersionV P N Q (fun (m : ℕ) => scaledDyadicCutoff M ↑m) β c a - smoothUMain M N Q β c a|) ≤ x ^ 2 / Real.log x ^ A

The actual signed U and V remainders, with the dispersion coefficient 2 on V, are paid without any assumed error bound. The alpha support and the larger finite cutoff support are separate, so smoothing introduces no false support restriction. This does not estimate the W/Kloosterman term.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.kClean_dispersionUV_smooth_c2_dyadic_log_payment {i k j : ℕ} (hi : 1 ≤ i) (hk : 1 ≤ k) (hj : 1 ≤ j) (A : ℕ) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (M T L : ℝ), 1 ≤ M → 1 ≤ T → 1 ≤ L → 4 * M * T = x → T ≤ x ^ (1 / 9) → L ≤ x ^ (5 / 9) → ∀ (S P N Q : Finset ℕ), (∀ m ∈ S, M ≤ ↑m ∧ ↑m ≤ 2 * M) → (∀ (m : ℕ), scaledDyadicCutoff M ↑m ≠ 0 → m ∈ P) → (∀ n ∈ N, T ≤ ↑n ∧ ↑n ≤ 2 * T) → Q ⊆ Finset.Ioc 0 ⌊L⌋₊ → ∀ (α β c : ℕ → ℝ), (∀ m ∈ S, |α m| ≤ ↑((fouvryTau i) m)) → (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → (∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) → ∀ (a : ℤ), (∑ m ∈ S, α m ^ 2) * (|dispersionU P N Q (fun (m : ℕ) => scaledDyadicCutoff M ↑m) β c a - smoothUMain M N Q β c a| + 2 * |dispersionV P N Q (fun (m : ℕ) => scaledDyadicCutoff M ↑m) β c a - smoothUMain M N Q β c a|) ≤ x ^ 2 / Real.log x ^ A

The original two dyadic intervals with x = 4 M N, including the closed short-variable endpoint N = x^(1/9).