The original error reduced to the actual low-omega factored W

The original modulus weight is unchanged on the left. Its difference from the trimmed convolution is paid at the original signed error, including the equality progression. Only then is the accepted five-small-factor reduction applied to the trimmed convolution and its second coefficient expanded.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError_sub_modulus (S N Q : Finset ℕ) (α β c d : ℕ → ℝ) (a : ℤ) : signedError S N Q α β c a - signedError S N Q α β d a = signedError S N Q α β (fun (q : ℕ) => c q - d q) a

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError_sub_factorLowOmega (S N Q : Finset ℕ) (α β γ ζ : ℕ → ℝ) (a : ℤ) (ξ : ℝ) : signedError S N Q α β (factorConvolution γ ζ) a - signedError S N Q α β (factorConvolution γ (betaLowOmega ζ ξ)) a = signedError S N Q α β (factorConvolution γ (betaHighOmega ζ ξ)) a

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.factorLowOmega_signedError_difference_payment (i k u v 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⌋₊ → ∀ (α β γ ζ : ℕ → ℝ), (∀ m ∈ S, |α m| ≤ ↑((fouvryTau i) m)) → (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → (∀ (r : ℕ), |γ r| ≤ ↑((fouvryTau u) r)) → (∀ (s : ℕ), |ζ s| ≤ ↑((fouvryTau v) s)) → ∀ (a : ℤ), a ≠ 0 → |↑a| ≤ x → |signedError S N Q α β (factorConvolution γ ζ) a - signedError S N Q α β (factorConvolution γ (betaLowOmega ζ (highOmegaCutoff x))) a| ≤ x / Real.log x ^ A

The difference is paid for original beta, not just its clean part. The threshold precedes both chosen factors and every changing residue.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.c2FiveSmallMask (x η : ℝ) (t : WOriginalTuple) : Prop

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.c2FiveSmallMask x η t = ((((↑(t.2.1.gcd t.2.2) ≤ x ^ η ∧ ↑t.2.1.primeFactors.card ≤ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.highOmegaCutoff x ∧ ↑t.2.2.primeFactors.card ≤ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.highOmegaCutoff x) ∧ ↑(t.1.1.gcd t.1.2) ≤ x ^ η) ∧ ↑(MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDTuple t).d₁ ≤ x ^ η) ∧ ↑(MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDTuple t).δ₁ ≤ x ^ η ∧ ↑(MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDTuple t).δ₂ ≤ x ^ η)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError_sq_le_five_small_factored_c2 {ι : Type u_1} {κ k i u v : ℕ} (A : ℕ) {T : ι → ℝ} {N : ι → Finset ℕ} {β : ι → ℕ → ℝ} (hSW : BetaCoprimeSWFamily κ T N β) (hT : ∀ (z : ι), 1 ≤ T z) (hN : ∀ (z : ι), ∀ n ∈ N z, T z ≤ ↑n ∧ ↑n ≤ 2 * T z) (hβ : ∀ (z : ι), ∀ n ∈ N z, |β z n| ≤ ↑((fouvryTau k) n)) {ε η : ℝ} (hε : 0 < ε) (hη : 0 < η) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (z : ι) (M L R₀ S₀ : ℝ), 1 ≤ M → 1 ≤ L → 4 * M * T z = x → x ^ ε ≤ T z → T z ≤ x ^ (1 / 10) → L ≤ x ^ (5 / 9) → ∀ (S Q : Finset ℕ), (∀ m ∈ S, M ≤ ↑m ∧ ↑m ≤ 2 * M) → Q ⊆ Finset.Ioc 0 ⌊L⌋₊ → ∀ (α c γ ζ : ℕ → ℝ), (∀ m ∈ S, |α m| ≤ ↑((fouvryTau i) m)) → (∀ (r : ℕ), |γ r| ≤ ↑((fouvryTau u) r)) → (∀ (s : ℕ), |ζ s| ≤ ↑((fouvryTau v) s)) → factorSupported R₀ γ → factorSupported S₀ ζ → c = factorConvolution γ ζ → ∀ (a : ℤ), a ≠ 0 → |↑a| ≤ x → signedError S (N z) Q α (β z) c a ^ 2 ≤ (8 * ∑ m ∈ S, α m ^ 2) * wMaskedFactoredTruncated M (wUniformCutoff M (x ^ η)) (N z) Q (betaClean (β z) a) (factorConvolution γ (betaLowOmega ζ (highOmegaCutoff x))) γ ζ a (c2FiveSmallMask x η) R₀ S₀ (highOmegaCutoff x) + x ^ 2 / Real.log x ^ A

A genuine reduction of the original error to the factored retained W. The factor orders can differ and can be zero. The harmless coefficient is eight after the additional square perturbation; no sign of W is assumed.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wellFactorable_signedError_sq_le_five_small_factored_c2 {ι : Type u_1} {κ k i j : ℕ} (A : ℕ) {T : ι → ℝ} {N : ι → Finset ℕ} {β : ι → ℕ → ℝ} (hSW : BetaCoprimeSWFamily κ T N β) (hT : ∀ (z : ι), 1 ≤ T z) (hN : ∀ (z : ι), ∀ n ∈ N z, T z ≤ ↑n ∧ ↑n ≤ 2 * T z) (hβ : ∀ (z : ι), ∀ n ∈ N z, |β z n| ≤ ↑((fouvryTau k) n)) {ε η : ℝ} (hε : 0 < ε) (hη : 0 < η) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (z : ι) (M ν : ℝ), 1 ≤ M → 4 * M * T z = x → ε ≤ ν → ν ≤ 1 / 10 → T z = x ^ ν → ∀ (S Q : Finset ℕ), (∀ m ∈ S, M ≤ ↑m ∧ ↑m ≤ 2 * M) → Q ⊆ Finset.Ioc 0 ⌊x ^ ((5 - 5 * ν) / 9 - ε)⌋₊ → ∀ (α c : ℕ → ℝ), (∀ m ∈ S, |α m| ≤ ↑((fouvryTau i) m)) → SignedWellFactorable j (x ^ ((5 - 5 * ν) / 9 - ε)) c → have R₀ := x ^ c2RExponent ν ε; have S₀ := x ^ c2SExponent ν ε; R₀ * S₀ = x ^ ((5 - 5 * ν) / 9 - ε) ∧ ∃ (γ : ℕ → ℝ) (ζ : ℕ → ℝ), factorSupported R₀ γ ∧ factorSupported S₀ ζ ∧ (∀ (r : ℕ), |γ r| ≤ ↑((fouvryTau j) r)) ∧ (∀ (s : ℕ), |ζ s| ≤ ↑((fouvryTau j) s)) ∧ c = factorConvolution γ ζ ∧ ∀ (a : ℤ), a ≠ 0 → |↑a| ≤ x → signedError S (N z) Q α (β z) c a ^ 2 ≤ (8 * ∑ m ∈ S, α m ^ 2) * wMaskedFactoredTruncated M (wUniformCutoff M (x ^ η)) (N z) Q (betaClean (β z) a) (factorConvolution γ (betaLowOmega ζ (highOmegaCutoff x))) γ ζ a (c2FiveSmallMask x η) R₀ S₀ (highOmegaCutoff x) + x ^ 2 / Real.log x ^ A

Choose a legal split of the original WF level and feed the resulting factors into the actual retained W. Factors are chosen before the residue. This is preprocessing, not the missing IV.3 estimate of the displayed W.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.factorLowOmega_eq_self_c2_near_endpoint {x ν ε ξ : ℝ} {ζ : ℕ → ℝ} (h : (1 - 10 * ν) / 9 ≤ ε / 2) (hζ : factorSupported (x ^ c2SExponent ν ε) ζ) (hξ : 0 ≤ ξ) : betaLowOmega ζ ξ = ζ

Throughout the near-endpoint branch, the low-omega operation deletes nothing from the second factor, not merely an asymptotically small error.