The actual coprimality partition back at the original distribution error

Only the triangle inequality between Lemma 7 cells is used. Every cell contains the original signed coefficients, tuple multiplicities, arithmetic phases and remaining filters. This is not an unweighted Weil estimate.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticPrefixSum_eq_coprimeFibers (x : ℝ) (N : Finset ℕ) (S : ℝ) (B : Finset (WExtractedTuple × ℤ)) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) (cap : Fin 5 → ℕ) : wAnalyticPrefixSum B β c₁ γ ζ a cap = ∑ c ∈ Finset.image (wCoprimeLabel x N S) B, wAnalyticPrefixSum (wCoprimeFiber x N S B c) β c₁ γ ζ a cap

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeBlockPrefixMajorant (x : ℝ) (N : Finset ℕ) (S : ℝ) (B : Finset (WExtractedTuple × ℤ)) (j : Fin 5 → ℕ) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeBlockPrefixMajorant x N S B j β c₁ γ ζ a = ∑ c ∈ Finset.image (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeLabel x N S) B, MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticBlockPrefixMax (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeFiber x N S B c) j β c₁ γ ζ a

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeBlockPrefixMajorant_nonneg (x : ℝ) (N : Finset ℕ) (S : ℝ) (B : Finset (WExtractedTuple × ℤ)) (j : Fin 5 → ℕ) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) : 0 ≤ wCoprimeBlockPrefixMajorant x N S B j β c₁ γ ζ a

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticBlockPrefixMax_le_coprime (x : ℝ) (N : Finset ℕ) (S : ℝ) (B : Finset (WExtractedTuple × ℤ)) (j : Fin 5 → ℕ) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) : wAnalyticBlockPrefixMax B j β c₁ γ ζ a ≤ wCoprimeBlockPrefixMajorant x N S B j β c₁ γ ζ a

The attained prefix is split into genuine coprimality cells. Different cells may choose different attaining caps, which only increases this bound.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeKeyPrefixMajorant (x : ℝ) (N : Finset ℕ) (S : ℝ) (U : Finset (WExtractedTuple × ℤ)) (K : WExtractedKey) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeKeyPrefixMajorant x N S U K β c₁ γ ζ a = ∑ j ∈ Finset.image MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticDyadicKey U, MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wBlockAmplitude K j * (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeBlockPrefixMajorant x N S (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticDyadicBlock U j true) j β c₁ γ ζ a + MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeBlockPrefixMajorant x N S (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticDyadicBlock U j false) j β c₁ γ ζ a)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticKeyPrefixMajorant_le_coprime (x : ℝ) (N : Finset ℕ) (S : ℝ) (U : Finset (WExtractedTuple × ℤ)) (K : WExtractedKey) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) : wAnalyticKeyPrefixMajorant U K β c₁ γ ζ a ≤ wCoprimeKeyPrefixMajorant x N S U K β c₁ γ ζ a

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimePrefix_cross_coprime {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {x η R S : ℝ} {b : ℕ} {K : WExtractedKey} {j cap : Fin 5 → ℕ} {positive : Bool} {c : Finset (ℕ × ℕ)} {t u : WExtractedTuple × ℤ} (ht : t ∈ wAnalyticPrefix (wCoprimeFiber x N S (wAnalyticDyadicBlock (wExtractedKeyFiber H N Q a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K) j positive) c) cap) (hu : u ∈ wAnalyticPrefix (wCoprimeFiber x N S (wAnalyticDyadicBlock (wExtractedKeyFiber H N Q a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K) j positive) c) cap) : (wCoprimePair t.1).1.Coprime (wCoprimePair u.1).2 ∧ (wCoprimePair u.1).1.Coprime (wCoprimePair t.1).2

All the arithmetic prefixes used in the new majorant satisfy the cross-coprimality conclusion proved on the original carrier.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.eventually_c2_wCoprimeLabel_count {θ : ℝ} (hθ : 0 < θ) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (a : ℤ) (η ν ε : ℝ) (b : ℕ) (K : WExtractedKey) (j : Fin 5 → ℕ) (positive : Bool), 0 ≤ ε → ε ≤ ν → ν ≤ 1 / 10 → (∀ n ∈ N, 0 < n ∧ ↑n ≤ 2 * x ^ ν) → (∀ q ∈ Q, 0 < q) → have S := x ^ c2SExponent ν ε; have U := wExtractedKeyFiber H N Q a (c2FiveSmallMask x η) (x ^ c2RExponent ν ε) S (highOmegaCutoff x) b K; ↑(Finset.image (wCoprimeLabel x N S) (wAnalyticDyadicBlock U j positive)).card ≤ x ^ θ

Uniform subpolynomial count for the actual C.2 dyadic cells, with no additional size hypothesis on the product coordinate.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wellFactorable_signedError_sq_le_coprime_prefix_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 ^ ν → ∀ (U : Finset ℕ), (∀ m ∈ U, M ≤ ↑m ∧ ↑m ≤ 2 * M) → ∀ (α c : ℕ → ℝ), (∀ m ∈ U, |α m| ≤ ↑((fouvryTau i) m)) → SignedWellFactorable j (x ^ ((5 - 5 * ν) / 9 - ε)) c → have L := x ^ ((5 - 5 * ν) / 9 - ε); have R₀ := x ^ c2RExponent ν ε; have S₀ := x ^ c2SExponent ν ε; have J := Nat.log 2 ⌈L ^ 2 / M * x ^ η⌉₊; R₀ * S₀ = L ∧ ∃ (γ : ℕ → ℝ) (ζ : ℕ → ℝ), factorSupported R₀ γ ∧ factorSupported S₀ ζ ∧ (∀ (r : ℕ), |γ r| ≤ ↑((fouvryTau j) r)) ∧ (∀ (s : ℕ), |ζ s| ≤ ↑((fouvryTau j) s)) ∧ c = factorConvolution γ ζ ∧ ∀ (a : ℤ), a ≠ 0 → |↑a| ≤ x → ∃ b ≤ J, ∃ K ∈ wExtractedKeyBox (x ^ η), signedError U (N z) (Finset.Ioc 0 ⌊L⌋₊) α (β z) c a ^ 2 ≤ (3072 * M * ∑ m ∈ U, α m ^ 2) * ↑(J + 1) * (x ^ η) ^ 7 * wAnalyticVariationConstant (x ^ η) * wCoprimeKeyPrefixMajorant x (N z) S₀ (wExtractedKeyFiber (wFloorCutoff M (x ^ η)) (N z) (Finset.Ioc 0 ⌊L⌋₊) a (c2FiveSmallMask x η) R₀ S₀ (highOmegaCutoff x) b K) K (betaClean (β z) a) (factorConvolution γ (betaLowOmega ζ (highOmegaCutoff x))) γ ζ a + x ^ 2 / Real.log x ^ A

The original signed error is now bounded by prefixes in constructed Lemma 7 cells; all WF/SW quantifiers and the full modulus interval survive.