Removing the Fourier transform from a finite W sum

This is the analytic integral-to-maximum step underlying Fouvry (1987), p. 627, (3.10)--(3.12), before the modulus and frequency decompositions. Mathlib's Fourier transform has kernel e(-x h / lcm(q,r)); the CRT factor is the positive character fourier h (productCRTResidue / lcm). Thus the frequency is the integer already used by wPoissonFrequency; no extra factor a is inserted into its Fourier kernel. The source's subsequent phase coordinates require a separate arithmetic identification.

The finite exponential sum retains all signed coefficients and all CRT phases. The maximum is constructed on the actual support interval, rather than postulated as an analytic hypothesis. No distribution estimate is proved.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicCutoffMass_eq_integral : dyadicCutoffMass = ∫ (x : ℝ), dyadicCutoff x

The previously defined Fourier mass is the real integral of the cutoff.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoff_integral {M : ℝ} (hM : 0 < M) : ∫ (x : ℝ), scaledDyadicCutoff M x = M * dyadicCutoffMass

Exact mass after dilation in the original real variable.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicCutoffMass_nonneg : 0 ≤ dyadicCutoffMass

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicCutoffMass_le_three : dyadicCutoffMass ≤ 3

A numerical mass bound, obtained from the cutoff's actual support and pointwise bound, with no Fourier or distribution estimate.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoff_integral_le_three_mul {M : ℝ} (hM : 0 < M) : ∫ (x : ℝ), scaledDyadicCutoff M x ≤ 3 * M

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoff_mul_integrable {M : ℝ} (hM : 0 < M) {F : ℝ → ℂ} (hF : Continuous F) : MeasureTheory.Integrable (fun (x : ℝ) => ↑(scaledDyadicCutoff M x) * F x) MeasureTheory.volume

Continuous exponential sums can be integrated against the scaled cutoff.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wFourierExponential (a : ℤ) (q r n₁ n₂ : ℕ) (h : ℤ) (x : ℝ) : ℂ

The reciprocal modulus and actual CRT phase, with the negative Fourier kernel at the original real variable. There is no triangle inequality here.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wFourierExponential a q r n₁ n₂ h x = ↑(↑(q.lcm r))⁻¹ * ↑(Real.fourierChar (-(x * (↑h / ↑(q.lcm r))))) * (fourier h) ↑(↑(MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.productCRTResidue q r n₁ n₂ a) / ↑(q.lcm r))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wFourierExponential_continuous (a : ℤ) (q r n₁ n₂ : ℕ) (h : ℤ) : Continuous (wFourierExponential a q r n₁ n₂ h)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wPoissonFrequency_eq_integral {M : ℝ} (hM : 0 < M) (a : ℤ) (q r n₁ n₂ : ℕ) {h : ℤ} (hh : h ≠ 0) : wPoissonFrequency M a q r n₁ n₂ h = ∫ (x : ℝ), ↑(scaledDyadicCutoff M x) * wFourierExponential a q r n₁ n₂ h x

Exact real integral formula for each nonzero Poisson frequency. It even holds for zero moduli under Lean's totalized reciprocal convention.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wFourierExponentialSum {ι : Type u_1} (T : Finset ι) (A : ι → ℝ) (a : ℤ) (q r n₁ n₂ : ι → ℕ) (h : ι → ℤ) (x : ℝ) : ℂ

A finite exponential sum with its real signed coefficients still inside.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wFourierExponentialSum T A a q r n₁ n₂ h x = ∑ i ∈ T, ↑(A i) * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wFourierExponential a (q i) (r i) (n₁ i) (n₂ i) (h i) x

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wFourierExponentialSum_continuous {ι : Type u_1} (T : Finset ι) (A : ι → ℝ) (a : ℤ) (q r n₁ n₂ : ι → ℕ) (h : ι → ℤ) : Continuous (wFourierExponentialSum T A a q r n₁ n₂ h)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_wPoissonFrequency_eq_integral {ι : Type u_1} {M : ℝ} (hM : 0 < M) (T : Finset ι) (A : ι → ℝ) (a : ℤ) (q r n₁ n₂ : ι → ℕ) (h : ι → ℤ) (hh : ∀ i ∈ T, h i ≠ 0) : ∑ i ∈ T, ↑(A i) * wPoissonFrequency M a (q i) (r i) (n₁ i) (n₂ i) (h i) = ∫ (x : ℝ), ↑(scaledDyadicCutoff M x) * wFourierExponentialSum T A a q r n₁ n₂ h x

Exact finite-sum integral identity, not a sum of termwise absolute values.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.norm_scaledDyadicCutoff_integral_le {M : ℝ} (hM : 0 < M) (F : ℝ → ℂ) (B : ℝ) (hB : ∀ x ∈ Set.Icc (M / 2) (3 * M), ‖F x‖ ≤ B) : ‖∫ (x : ℝ), ↑(scaledDyadicCutoff M x) * F x‖ ≤ M * dyadicCutoffMass * B

Integral majorization only uses a bound on the actual cutoff support. The function need not have constant sign, or even be continuous.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.norm_sum_wPoissonFrequency_le {ι : Type u_1} {M : ℝ} (hM : 0 < M) (T : Finset ι) (A : ι → ℝ) (a : ℤ) (q r n₁ n₂ : ι → ℕ) (h : ι → ℤ) (hh : ∀ i ∈ T, h i ≠ 0) (B : ℝ) (hB : ∀ x ∈ Set.Icc (M / 2) (3 * M), ‖wFourierExponentialSum T A a q r n₁ n₂ h x‖ ≤ B) : ‖∑ i ∈ T, ↑(A i) * wPoissonFrequency M a (q i) (r i) (n₁ i) (n₂ i) (h i)‖ ≤ M * dyadicCutoffMass * B

A pointwise exponential-sum bound may be inserted without destroying cancellation among the real signed coefficients.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wFourierExponentialSup {ι : Type u_1} (M : ℝ) (T : Finset ι) (A : ι → ℝ) (a : ℤ) (q r n₁ n₂ : ι → ℕ) (h : ι → ℤ) : ℝ

The actual supremum of the explicit exponential sum on the support interval. Its finiteness and attainment are proved below.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wFourierExponentialSup M T A a q r n₁ n₂ h = sSup ((fun (x : ℝ) => ‖MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wFourierExponentialSum T A a q r n₁ n₂ h x‖) '' Set.Icc (M / 2) (3 * M))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wFourierExponentialSum_le_sup {ι : Type u_1} (M : ℝ) (T : Finset ι) (A : ι → ℝ) (a : ℤ) (q r n₁ n₂ : ι → ℕ) (h : ι → ℤ) {x : ℝ} (hx : x ∈ Set.Icc (M / 2) (3 * M)) : ‖wFourierExponentialSum T A a q r n₁ n₂ h x‖ ≤ wFourierExponentialSup M T A a q r n₁ n₂ h

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wFourierExponentialSup_attained {ι : Type u_1} {M : ℝ} (hM : 0 < M) (T : Finset ι) (A : ι → ℝ) (a : ℤ) (q r n₁ n₂ : ι → ℕ) (h : ι → ℤ) : ∃ x ∈ Set.Icc (M / 2) (3 * M), wFourierExponentialSup M T A a q r n₁ n₂ h = ‖wFourierExponentialSum T A a q r n₁ n₂ h x‖

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.norm_sum_wPoissonFrequency_le_sup {ι : Type u_1} {M : ℝ} (hM : 0 < M) (T : Finset ι) (A : ι → ℝ) (a : ℤ) (q r n₁ n₂ : ι → ℕ) (h : ι → ℤ) (hh : ∀ i ∈ T, h i ≠ 0) : ‖∑ i ∈ T, ↑(A i) * wPoissonFrequency M a (q i) (r i) (n₁ i) (n₂ i) (h i)‖ ≤ M * dyadicCutoffMass * wFourierExponentialSup M T A a q r n₁ n₂ h

Unconditional analytic maximum bound for every finite signed W sum. Arithmetic reindexing, dyadic aggregation, and distribution estimates remain separate consumers of this theorem.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.norm_sum_wPoissonFrequency_le_three_mul_max {ι : Type u_1} {M : ℝ} (hM : 0 < M) (T : Finset ι) (A : ι → ℝ) (a : ℤ) (q r n₁ n₂ : ι → ℕ) (h : ι → ℤ) (hh : ∀ i ∈ T, h i ≠ 0) : ∃ y ∈ Set.Icc (1 / 2) 3, (∀ z ∈ Set.Icc (1 / 2) 3, ‖wFourierExponentialSum T A a q r n₁ n₂ h (M * z)‖ ≤ ‖wFourierExponentialSum T A a q r n₁ n₂ h (M * y)‖) ∧ ‖∑ i ∈ T, ↑(A i) * wPoissonFrequency M a (q i) (r i) (n₁ i) (n₂ i) (h i)‖ ≤ 3 * M * ‖wFourierExponentialSum T A a q r n₁ n₂ h (M * y)‖

The bound with numerical loss 3 * M and an actual maximizing point in the fixed normalized interval. The exponential sum is evaluated at M*y, so its Fourier kernel is e(-M*y*h/lcm), retaining every signed coefficient.