Logarithmic payment of beta divisor deletion in the actual signed error

The thresholds precede the changing residue, scales, finite supports and signed coefficients. All three divisor orders may be zero. The equality progression is paid separately, without a nondivisibility, SW, Shiu or distribution input.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaPayment_eventually_log_mul_rpow_le (K : ℝ) (hK : 0 ≤ K) (B : ℕ) {b d : ℝ} (hbd : b < d) : ∀ᶠ (x : ℝ) in Filter.atTop, K * (1 + Real.log x) ^ B * x ^ b ≤ x ^ d

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaPayment_eventually_tau_le (k : ℕ) {δ : ℝ} (hδ : 0 < δ) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (n : ℕ), 0 < n → ↑n ≤ 2 * x → ↑((fouvryTau k) n) ≤ x ^ δ

Uniformity also covers bounded small integers, not just integers tending to infinity along with the scale.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaPayment_card_dyadic_le {M : ℝ} (hM : 1 ≤ M) (S : Finset ℕ) (hS : ∀ m ∈ S, M ≤ ↑m ∧ ↑m ≤ 2 * M) : ↑S.card ≤ 2 * M

A finite cardinality estimate for arbitrary, possibly sparse, dyadic alpha supports.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaPayment_eventually_signedError_bound (i k j : ℕ) {δ : ℝ} (hδ : 0 < δ) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (M T L : ℝ), 1 ≤ M → 1 ≤ T → 1 ≤ L → x = 4 * M * T → L ≤ x → ∀ (S N Q : Finset ℕ), (∀ m ∈ S, M ≤ ↑m ∧ ↑m ≤ 2 * M) → (∀ 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 : ℤ), a ≠ 0 → |↑a| ≤ x → |signedError S N Q α (betaDivisorPart β a) c a| ≤ 4 * (M + L) * x ^ (3 * δ)

The actual signed error after deletion, before spending the power saving. The equality m*n=a is included in this estimate.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaDivisorPart_signedError_power_saving (i k j : ℕ) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (M T L : ℝ), 1 ≤ M → 1 ≤ T → 1 ≤ L → x = 4 * M * T → x ^ ε ≤ T → L ≤ x ^ (5 / 9) → ∀ (S N Q : Finset ℕ), (∀ m ∈ S, M ≤ ↑m ∧ ↑m ≤ 2 * M) → (∀ 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 : ℤ), a ≠ 0 → |↑a| ≤ x → |signedError S N Q α (betaDivisorPart β a) c a| ≤ x ^ (1 - min ε (4 / 9) / 2)

Power saving uniform in the complete changing input. In particular, the residue may vary throughout 0 < |a| ≤ x, including equality progressions.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaClean_signedError_log_payment (i k j A : ℕ) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (M T L : ℝ), 1 ≤ M → 1 ≤ T → 1 ≤ L → x = 4 * M * T → x ^ ε ≤ T → L ≤ x ^ (5 / 9) → ∀ (S N Q : Finset ℕ), (∀ m ∈ S, M ≤ ↑m ∧ ↑m ≤ 2 * M) → (∀ 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 : ℤ), a ≠ 0 → |↑a| ≤ x → |signedError S N Q α (betaDivisorPart β a) c a| ≤ x / Real.log x ^ A ∧ |signedError S N Q α β c a - signedError S N Q α (betaClean β a) c a| ≤ x / Real.log x ^ A ∧ |signedError S N Q α β c a| ≤ |signedError S N Q α (betaClean β a) c a| + x / Real.log x ^ A

The genuine C.2 preprocessing payment, not an assumed error estimate. For fixed orders (including zero), saving order, and positive epsilon, one threshold works simultaneously for all scales, supports, signed sequences and nonzero residues in the full permitted range. The original-to-clean difference and the triangle transfer are part of the same uniform conclusion.