Canonical divisor extraction in the actual delayed W

Fouvry (1987), p. 627, §III.5: extract δ δ₂ from q₂ = r s. The explicit finite target retains the original support, compatibility, mask, low omega of s, signed first coefficient, and exactly the same cutoff H. This is a finite preprocessing identity, not (3.12) or an IV.3 estimate.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wSecondExtractionDivisor (t : WOriginalTuple) : ℕ

This is δ δ₂, not WGCDData.D = δ δ₁ δ₂.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wSecondExtractionDivisor t = (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDTuple t).δ * (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDTuple t).δ₂

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wSecondExtractionDivisor_pos_dvd {t : WOriginalTuple} (ht : 0 < t.1.2) : 0 < wSecondExtractionDivisor t ∧ wSecondExtractionDivisor t ∣ t.1.2

Positivity of the original second modulus alone suffices. No conditions on the beta indices, mask, or first modulus are hidden in this construction.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wFactorExtractionMask (Q : Finset ℕ) (a : ℤ) (P : WOriginalTuple → Prop) (ξ : ℝ) (r s : ℕ) (u : ℕ × ℕ × ℕ) : Prop

The auxiliary coordinates range over the original q₁,n₁,n₂ box. The remaining tests include low omega on the original second factor s.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wFactorExtractionMask Q a P ξ r s u = (↑s.primeFactors.card ≤ ξ ∧ r * s ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q a ∧ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WCompatible u.1 (r * s) u.2.1 u.2.2 ∧ P ((u.1, r * s), u.2))

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wFactorExtractionTuples (N Q : Finset ℕ) (a : ℤ) (P : WOriginalTuple → Prop) (R S ξ : ℝ) : Finset (FactorExtractionTuple × ℕ × ℕ × ℕ)

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wFactorExtractionTuples N Q a P R S ξ = MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.factorExtractionTarget ⌊R⌋₊ ⌊S⌋₊ (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q a ×ˢ N ×ˢ N) (fun (r s : ℕ) (u : ℕ × ℕ × ℕ) => MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wSecondExtractionDivisor ((u.1, r * s), u.2)) (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wFactorExtractionMask Q a P ξ)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mem_wFactorExtractionTuples_iff {N Q : Finset ℕ} {a : ℤ} {P : WOriginalTuple → Prop} {R S ξ : ℝ} {z : FactorExtractionTuple × ℕ × ℕ × ℕ} : z ∈ wFactorExtractionTuples N Q a P R S ξ ↔ have r := z.1.1.1 * z.1.2.1; have s := z.1.1.2 * z.1.2.2; z.1.1.1 ∈ Finset.Ioc 0 ⌊R⌋₊ ∧ z.1.1.2 ∈ Finset.Ioc 0 ⌊S⌋₊ ∧ z.1.2.1 ∈ Finset.Ioc 0 ⌊R⌋₊ ∧ z.1.2.2 ∈ Finset.Ioc 0 ⌊S⌋₊ ∧ r ≤ ⌊R⌋₊ ∧ s ≤ ⌊S⌋₊ ∧ z.2.1 ∈ reducedModuli Q a ∧ z.2.2.1 ∈ N ∧ z.2.2.2 ∈ N ∧ r * s ∈ reducedModuli Q a ∧ WCompatible z.2.1 (r * s) z.2.2.1 z.2.2.2 ∧ P ((z.2.1, r * s), z.2.2) ∧ ↑s.primeFactors.card ≤ ξ ∧ wSecondExtractionDivisor ((z.2.1, r * s), z.2.2) = z.1.1.1 * z.1.1.2 ∧ z.1.2.2.Coprime z.1.1.1

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedFactorExtractedTruncated (M : ℝ) (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) (R S ξ : ℝ) : ℝ

The actual W after the unique arithmetic extraction. In particular the second modulus is (Δ*r')*(Δ'*s'), not a free or enlarged modulus variable.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedFactorExtractedTruncated M H N Q β c₁ γ ζ a P R S ξ = ∑ z ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wFactorExtractionTuples N Q a P R S ξ, γ (z.1.1.1 * z.1.2.1) * ζ (z.1.1.2 * z.1.2.2) * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wSecondModulusKernel M H β c₁ a ((z.2.1, z.1.1.1 * z.1.2.1 * (z.1.1.2 * z.1.2.2)), z.2.2)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedFactoredTruncated_eq_extracted (M : ℝ) (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) (R S ξ : ℝ) : wMaskedFactoredTruncated M H N Q β c₁ γ ζ a P R S ξ = wMaskedFactorExtractedTruncated M H N Q β c₁ γ ζ a P R S ξ

Exact transport of the accepted delayed sum, with no sign assumptions and no new support or coprimality premises supplied by the caller.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedTruncated_eq_factorExtracted_of_eq {R S ξ : ℝ} {γ ζ c : ℕ → ℝ} (hγ : factorSupported R γ) (hζ : factorSupported S ζ) (hc : c = factorConvolution γ (betaLowOmega ζ ξ)) (M : ℝ) (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) : wMaskedTruncated M H N Q β c a P = wMaskedFactorExtractedTruncated M H N Q β c γ ζ a P R S ξ

The same exact transport starting from the original masked retained W. Only its second coefficient is expanded, and the first copy of c survives.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.c2FiveSmall_factored_eq_extracted (M x η R S : ℝ) (N Q : Finset ℕ) (β γ ζ : ℕ → ℝ) (a : ℤ) : wMaskedFactoredTruncated M (wUniformCutoff M (x ^ η)) N Q (betaClean β a) (factorConvolution γ (betaLowOmega ζ (highOmegaCutoff x))) γ ζ a (c2FiveSmallMask x η) R S (highOmegaCutoff x) = wMaskedFactorExtractedTruncated M (wUniformCutoff M (x ^ η)) N Q (betaClean β a) (factorConvolution γ (betaLowOmega ζ (highOmegaCutoff x))) γ ζ a (c2FiveSmallMask x η) R S (highOmegaCutoff x)

The exact W which occurs at the accepted C.2 preprocessing endpoint: the first coefficient remains the trimmed convolution, beta remains clean, all five-small conditions survive, and the cutoff is unchanged.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wellFactorable_signedError_sq_le_five_small_extracted_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) * wMaskedFactorExtractedTruncated 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

Original WF error at the constructed canonical-extraction endpoint. All factors are chosen before the changing residue, and no interval structure or estimate of the surviving oscillatory sum is assumed.