Finite rank-one separation of the damped arctangent kernel

This leaf contains only the finite algebra behind the later mean estimate. It splits the nonzero-frequency truncated Perron integrand into two rank-one rectangular terms and records the coefficient-energy bounds needed to feed rankOneRectangularWeightedPrimitiveMean_le. It makes no final mean claim.

This module is intentionally not imported by a canonical facade.

theorem AnalyticNumberTheory.LargeSieve.log_div_int_mul_eq_sub_log_sub_log {y : ℝ} {m n : ℤ} (hy : 0 < y) (hm : 0 < m) (hn : 0 < n) : Real.log (y / ↑(m * n)) = Real.log y - Real.log ↑m - Real.log ↑n

The logarithm in the product kernel separates into its two rectangular coordinates. Positivity hypotheses are explicit because this is the form used on positive integer rectangles.

noncomputable def AnalyticNumberTheory.LargeSieve.leftSinTwist (a : ℤ → ℂ) (y t : ℝ) (m : ℤ) : ℂ

Sine twist in the left rectangle.

Equations

• AnalyticNumberTheory.LargeSieve.leftSinTwist a y t m = a m * ↑(Real.sin (t * (Real.log y - Real.log ↑m)))

noncomputable def AnalyticNumberTheory.LargeSieve.leftCosTwist (a : ℤ → ℂ) (y t : ℝ) (m : ℤ) : ℂ

Cosine twist in the left rectangle.

Equations

• AnalyticNumberTheory.LargeSieve.leftCosTwist a y t m = a m * ↑(Real.cos (t * (Real.log y - Real.log ↑m)))

noncomputable def AnalyticNumberTheory.LargeSieve.rightSinTwist (b : ℤ → ℂ) (t : ℝ) (n : ℤ) : ℂ

Sine twist in the right rectangle.

Equations

• AnalyticNumberTheory.LargeSieve.rightSinTwist b t n = b n * ↑(Real.sin (t * Real.log ↑n))

noncomputable def AnalyticNumberTheory.LargeSieve.rightCosTwist (b : ℤ → ℂ) (t : ℝ) (n : ℤ) : ℂ

Cosine twist in the right rectangle.

Equations

• AnalyticNumberTheory.LargeSieve.rightCosTwist b t n = b n * ↑(Real.cos (t * Real.log ↑n))

theorem AnalyticNumberTheory.LargeSieve.truncatedPerronIntegrand_log_div_int_mul_eq_rankOne {y t : ℝ} {m n : ℤ} (hy : 0 < y) (hm : 0 < m) (hn : 0 < n) (ht : t ≠ 0) : ↑(truncatedPerronIntegrand (Real.log (y / ↑(m * n))) t) = 1 / ↑t * (↑(Real.sin (t * (Real.log y - Real.log ↑m))) * ↑(Real.cos (t * Real.log ↑n)) - ↑(Real.cos (t * (Real.log y - Real.log ↑m))) * ↑(Real.sin (t * Real.log ↑n)))

Exact pointwise rank-one separation at a nonzero frequency. The common factor 1/t is deliberately outside the four coefficient twists.

noncomputable def AnalyticNumberTheory.LargeSieve.rectangularKernelCharacterSum (a b : ℤ → ℂ) (y t : ℝ) (Ma Mb : ℤ) (Na Nb q : ℕ) (χ : PrimitiveCharacter q) : ℂ

The original rectangular double sum with the truncated Perron integrand.

Equations

• AnalyticNumberTheory.LargeSieve.rectangularKernelCharacterSum a b y t Ma Mb Na Nb q χ = ∑ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), ∑ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), a m * b n * ↑χ ↑(m * n) * ↑(AnalyticNumberTheory.LargeSieve.truncatedPerronIntegrand (Real.log (y / ↑(m * n))) t)

theorem AnalyticNumberTheory.LargeSieve.rectangularKernelCharacterSum_eq_rankOne (a b : ℤ → ℂ) {y t : ℝ} (hy : 0 < y) (ht : t ≠ 0) (Ma Mb : ℤ) (Na Nb q : ℕ) (χ : PrimitiveCharacter q) (hm : ∀ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), 0 < m) (hn : ∀ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), 0 < n) : rectangularKernelCharacterSum a b y t Ma Mb Na Nb q χ = 1 / ↑t * ((∑ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), leftSinTwist a y t m * ↑χ ↑m) * ∑ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), rightCosTwist b t n * ↑χ ↑n - (∑ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), leftCosTwist a y t m * ↑χ ↑m) * ∑ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), rightSinTwist b t n * ↑χ ↑n)

Four one-dimensional rectangular Dirichlet sums reproduce the original kernel-weighted double sum exactly. Its quantifier order and interval format match rankOneRectangularWeightedPrimitiveMean_le directly.

theorem AnalyticNumberTheory.LargeSieve.sum_norm_sq_leftSinTwist_le (a : ℤ → ℂ) (y t L : ℝ) (s : Finset ℤ) (hL : 0 ≤ L) (hlog : ∀ m ∈ s, |Real.log y - Real.log ↑m| ≤ L) : ∑ m ∈ s, ‖leftSinTwist a y t m‖ ^ 2 ≤ min 1 (L * |t|) ^ 2 * ∑ m ∈ s, ‖a m‖ ^ 2

A sine twist costs the square of min 1 (L*|t|) when the logarithmic coordinate has absolute value at most L.

theorem AnalyticNumberTheory.LargeSieve.sum_norm_sq_leftSinTwist_le_of_nonneg (a : ℤ → ℂ) (y t L : ℝ) (s : Finset ℤ) (ht : 0 ≤ t) (hL : 0 ≤ L) (hlog : ∀ m ∈ s, |Real.log y - Real.log ↑m| ≤ L) : ∑ m ∈ s, ‖leftSinTwist a y t m‖ ^ 2 ≤ min 1 (L * t) ^ 2 * ∑ m ∈ s, ‖a m‖ ^ 2

Nonnegative-frequency form with the literal damping factor min 1 (L*t).

theorem AnalyticNumberTheory.LargeSieve.sum_norm_sq_leftCosTwist_le (a : ℤ → ℂ) (y t : ℝ) (s : Finset ℤ) : ∑ m ∈ s, ‖leftCosTwist a y t m‖ ^ 2 ≤ ∑ m ∈ s, ‖a m‖ ^ 2

A cosine twist never enlarges coefficient energy.

theorem AnalyticNumberTheory.LargeSieve.sum_norm_sq_rightSinTwist_le (b : ℤ → ℂ) (t L : ℝ) (s : Finset ℤ) (hL : 0 ≤ L) (hlog : ∀ n ∈ s, |Real.log ↑n| ≤ L) : ∑ n ∈ s, ‖rightSinTwist b t n‖ ^ 2 ≤ min 1 (L * |t|) ^ 2 * ∑ n ∈ s, ‖b n‖ ^ 2

Right sine energy bound.

theorem AnalyticNumberTheory.LargeSieve.sum_norm_sq_rightSinTwist_le_of_nonneg (b : ℤ → ℂ) (t L : ℝ) (s : Finset ℤ) (ht : 0 ≤ t) (hL : 0 ≤ L) (hlog : ∀ n ∈ s, |Real.log ↑n| ≤ L) : ∑ n ∈ s, ‖rightSinTwist b t n‖ ^ 2 ≤ min 1 (L * t) ^ 2 * ∑ n ∈ s, ‖b n‖ ^ 2

Nonnegative-frequency right sine-energy form.

theorem AnalyticNumberTheory.LargeSieve.sum_norm_sq_rightCosTwist_le (b : ℤ → ℂ) (t : ℝ) (s : Finset ℤ) : ∑ n ∈ s, ‖rightCosTwist b t n‖ ^ 2 ≤ ∑ n ∈ s, ‖b n‖ ^ 2

Right cosine energy bound.

theorem AnalyticNumberTheory.LargeSieve.abs_log_int_le_log {M : ℕ} (_hM : 1 ≤ M) {n : ℤ} (hn1 : 1 ≤ n) (hnM : n ≤ ↑M) : |Real.log ↑n| ≤ Real.log ↑M

On positive integer support n ≤ M, the right logarithmic coordinate is bounded by log M.

theorem AnalyticNumberTheory.LargeSieve.abs_log_div_int_le_two_log {M : ℕ} (hM : 3 ≤ M) {y : ℝ} (hy0 : 1 / 2 ≤ y) (hyM : y ≤ ↑M + 1 / 2) {m : ℤ} (hm1 : 1 ≤ m) (hmM : m ≤ ↑M) : |Real.log y - Real.log ↑m| ≤ 2 * Real.log ↑M

Half-step geometry bound for the left logarithmic coordinate. The lower half-step hypothesis is necessary: an upper bound on y alone cannot control |log y|.

theorem AnalyticNumberTheory.LargeSieve.sum_norm_sq_leftSinTwist_Icc_le_of_halfstep (a : ℤ → ℂ) (y t : ℝ) (Ma : ℤ) (Na M : ℕ) (hM : 3 ≤ M) (hy0 : 1 / 2 ≤ y) (hyM : y ≤ ↑M + 1 / 2) (hm1 : ∀ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), 1 ≤ m) (hmM : ∀ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), m ≤ ↑M) : ∑ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), ‖leftSinTwist a y t m‖ ^ 2 ≤ min 1 (2 * Real.log ↑M * |t|) ^ 2 * ∑ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), ‖a m‖ ^ 2

Half-step specialization of the left sine-energy estimate on a rectangle. This is in exactly the Icc (start+1) (start+length) format consumed by the rank-one primitive mean theorem.

theorem AnalyticNumberTheory.LargeSieve.sum_norm_sq_rightSinTwist_Icc_le (b : ℤ → ℂ) (t : ℝ) (Mb : ℤ) (Nb M : ℕ) (hM : 1 ≤ M) (hn1 : ∀ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), 1 ≤ n) (hnM : ∀ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), n ≤ ↑M) : ∑ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), ‖rightSinTwist b t n‖ ^ 2 ≤ min 1 (Real.log ↑M * |t|) ^ 2 * ∑ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), ‖b n‖ ^ 2

Positive-support specialization of the right sine-energy estimate on the same rectangle format.