Delayed decomposition of the second modulus coefficient

Fouvry (1987), p. 627, §III.5, decomposes only the second coefficient, after all arithmetic restrictions and the frequency truncation are fixed. The finite identities below retain signed coefficients, the original mask, and the original modulus-dependent cutoff. No factorability of the low-omega convolution, or interval structure of an arithmetic fiber, is used. The further canonical Δ, Δ' extraction and Fourier estimates are not asserted here.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.factorConvolution_eq_sum_box {R S : ℝ} {γ ζ : ℕ → ℝ} (hγ : factorSupported R γ) (hζ : factorSupported S ζ) (q : ℕ) : factorConvolution γ ζ q = ∑ r ∈ Finset.Ioc 0 ⌊R⌋₊, ∑ s ∈ Finset.Ioc 0 ⌊S⌋₊, if r * s = q then γ r * ζ s else 0

Closed positive factor supports turn the divisor antidiagonal into an exact rectangular sum, including at modulus zero.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_factorConvolution_eq_box_fibers {ι : Type u_1} {R S : ℝ} {γ ζ : ℕ → ℝ} (hγ : factorSupported R γ) (hζ : factorSupported S ζ) (T : Finset ι) (q : ι → ℕ) (F : ι → ℝ) : ∑ t ∈ T, factorConvolution γ ζ (q t) * F t = ∑ r ∈ Finset.Ioc 0 ⌊R⌋₊, ∑ s ∈ Finset.Ioc 0 ⌊S⌋₊, ∑ t ∈ T with q t = r * s, γ r * ζ s * F t

Reindex before taking absolute values: factors are the outer variables, and the remaining finite set is the exact product fiber.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_factorConvolution_lowOmega_eq_box_fibers {ι : Type u_1} {R S : ℝ} {γ ζ : ℕ → ℝ} (hγ : factorSupported R γ) (hζ : factorSupported S ζ) (ξ : ℝ) (T : Finset ι) (q : ι → ℕ) (F : ι → ℝ) : ∑ t ∈ T, factorConvolution γ (betaLowOmega ζ ξ) (q t) * F t = ∑ r ∈ Finset.Ioc 0 ⌊R⌋₊, ∑ s ∈ Finset.Ioc 0 ⌊S⌋₊ with ↑s.primeFactors.card ≤ ξ, ∑ t ∈ T with q t = r * s, γ r * ζ s * F t

The same rectangular reindexing with low omega on the second factor, not on the product modulus and not on the first factor.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wDelayedTuples (N Q : Finset ℕ) (a : ℤ) (P : WOriginalTuple → Prop) (r s : ℕ) : Finset (ℕ × ℕ × ℕ)

The surviving variables are (q₁,n₁,n₂); the second modulus is r*s. All original reduced-modulus, beta-support, compatibility, and mask tests are retained. This finite set is not asserted to be an interval.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wDelayedTuples N Q a P r s = {u ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q a ×ˢ N ×ˢ N | 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)}

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mem_wDelayedTuples_iff {N Q : Finset ℕ} {a : ℤ} {P : WOriginalTuple → Prop} {r s : ℕ} {u : ℕ × ℕ × ℕ} : u ∈ wDelayedTuples N Q a P r s ↔ ((u.1, r * s), u.2) ∈ wMaskedTuples N Q a P

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wDelayedTuples_spec {N Q : Finset ℕ} {a : ℤ} {P : WOriginalTuple → Prop} {r s : ℕ} {u : ℕ × ℕ × ℕ} (hu : u ∈ wDelayedTuples N Q a P r s) : u.1 ∈ reducedModuli Q a ∧ r * s ∈ reducedModuli Q a ∧ u.2.1 ∈ N ∧ u.2.2 ∈ N ∧ WCompatible u.1 (r * s) u.2.1 u.2.2 ∧ P ((u.1, r * s), u.2)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_wMaskedTuples_productFiber {A : Type u_1} [AddCommMonoid A] (N Q : Finset ℕ) (a : ℤ) (P : WOriginalTuple → Prop) (r s : ℕ) (F : WOriginalTuple → A) : ∑ t ∈ wMaskedTuples N Q a P with t.1.2 = r * s, F t = ∑ u ∈ wDelayedTuples N Q a P r s, F ((u.1, r * s), u.2)

Eliminate the second modulus from its exact product fiber.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wSecondModulusKernel (M : ℝ) (H : ℕ → ℕ → ℕ) (β c₁ : ℕ → ℝ) (a : ℤ) (t : WOriginalTuple) : ℝ

The first modulus coefficient and the original frequency cutoff remain inside the kernel; only the second modulus coefficient is removed.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wSecondModulusKernel M H β c₁ a t = c₁ t.1.1 * β t.2.1 * β t.2.2 * (∑ h ∈ Finset.Icc (-↑(H t.1.1 t.1.2)) ↑(H t.1.1 t.1.2), MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wPoissonFrequency M a t.1.1 t.1.2 t.2.1 t.2.2 h).re

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

The actual factored retained-frequency sum. The outer factor supports are closed and positive, low omega is imposed only on s, and q₂ has been eliminated. The first coefficient is the arbitrary signed c₁.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedFactoredTruncated M H N Q β c₁ γ ζ a P R S ξ = ∑ r ∈ Finset.Ioc 0 ⌊R⌋₊, ∑ s ∈ Finset.Ioc 0 ⌊S⌋₊ with ↑s.primeFactors.card ≤ ξ, ∑ u ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wDelayedTuples N Q a P r s, γ r * ζ s * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wSecondModulusKernel M H β c₁ a ((u.1, r * s), u.2)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_secondModulusConvolution_eq_factored {R S : ℝ} {γ ζ : ℕ → ℝ} (hγ : factorSupported R γ) (hζ : factorSupported S ζ) (M : ℝ) (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c₁ : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) (ξ : ℝ) : ∑ t ∈ wMaskedTuples N Q a P, factorConvolution γ (betaLowOmega ζ ξ) t.1.2 * wSecondModulusKernel M H β c₁ a t = wMaskedFactoredTruncated M H N Q β c₁ γ ζ a P R S ξ

A general signed first coefficient is untouched by delayed expansion.

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

Exact delayed expansion of the actual wMaskedTruncated, decomposing only its second coefficient. No sign, positivity-of-scale, or support conditions beyond the two factor supports are needed for this identity.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedTruncated_eq_factored_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 = wMaskedFactoredTruncated M H N Q β c γ ζ a P R S ξ