Y-uniform phase separation for the damped arctangent kernel

This leaf separates the half-step parameter y from both coefficient sequences. The four coefficient twists below are independent of y, so the selector Y q χ may be chosen separately for every primitive character before one applies the rectangular rank-one mean theorem. No maximal-mean estimate is claimed here.

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

The y-independent cosine coefficient twist.

Equations

• AnalyticNumberTheory.LargeSieve.phaseCosTwist a t m = a m * ↑(Real.cos (t * Real.log ↑m))

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

The y-independent sine coefficient twist.

Equations

• AnalyticNumberTheory.LargeSieve.phaseSinTwist a t m = a m * ↑(Real.sin (t * Real.log ↑m))

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

One rectangular rank-one character product.

Equations

• AnalyticNumberTheory.LargeSieve.phaseRankOneCharacterProduct a b Ma Mb Na Nb q χ = (∑ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), a m * ↑χ ↑m) * ∑ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), b n * ↑χ ↑n

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

The direct positive-frequency logarithmic kernel on a rectangle.

Equations

• AnalyticNumberTheory.LargeSieve.dampedLogRectangularCharacterSum 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) * (↑(Real.sin (t * Real.log (y / ↑(m * n)))) / ↑t)

theorem AnalyticNumberTheory.LargeSieve.damped_log_term_eq_four_rankOne (a b : ℤ → ℂ) {y t : ℝ} {m n : ℤ} {q : ℕ} (χ : PrimitiveCharacter q) (hy : 0 < y) (hm : 0 < m) (hn : 0 < n) (_ht : 0 < t) : a m * b n * ↑χ ↑(m * n) * (↑(Real.sin (t * Real.log (y / ↑(m * n)))) / ↑t) = 1 / ↑t * (↑(Real.sin (t * Real.log y)) * (phaseCosTwist a t m * ↑χ ↑m) * (phaseCosTwist b t n * ↑χ ↑n) - ↑(Real.cos (t * Real.log y)) * (phaseSinTwist a t m * ↑χ ↑m) * (phaseCosTwist b t n * ↑χ ↑n) - ↑(Real.cos (t * Real.log y)) * (phaseCosTwist a t m * ↑χ ↑m) * (phaseSinTwist b t n * ↑χ ↑n) - ↑(Real.sin (t * Real.log y)) * (phaseSinTwist a t m * ↑χ ↑m) * (phaseSinTwist b t n * ↑χ ↑n))

Exact sin (A-B-C) expansion into four rank-one products.

theorem AnalyticNumberTheory.LargeSieve.dampedLogRectangularCharacterSum_eq_four_rankOne (a b : ℤ → ℂ) {y t : ℝ} (hy : 0 < y) (ht : 0 < t) (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) : dampedLogRectangularCharacterSum a b y t Ma Mb Na Nb q χ = 1 / ↑t * (↑(Real.sin (t * Real.log y)) * phaseRankOneCharacterProduct (phaseCosTwist a t) (phaseCosTwist b t) Ma Mb Na Nb q χ - ↑(Real.cos (t * Real.log y)) * phaseRankOneCharacterProduct (phaseSinTwist a t) (phaseCosTwist b t) Ma Mb Na Nb q χ - ↑(Real.cos (t * Real.log y)) * phaseRankOneCharacterProduct (phaseCosTwist a t) (phaseSinTwist b t) Ma Mb Na Nb q χ - ↑(Real.sin (t * Real.log y)) * phaseRankOneCharacterProduct (phaseSinTwist a t) (phaseSinTwist b t) Ma Mb Na Nb q χ)

Exact four-product separation of the whole rectangle.

theorem AnalyticNumberTheory.LargeSieve.norm_dampedLogRectangularCharacterSum_le_four_rankOne (a b : ℤ → ℂ) {y t : ℝ} (hy : 0 < y) (ht : 0 < t) (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) : ‖dampedLogRectangularCharacterSum a b y t Ma Mb Na Nb q χ‖ ≤ 1 / t * (|Real.sin (t * Real.log y)| * ‖phaseRankOneCharacterProduct (phaseCosTwist a t) (phaseCosTwist b t) Ma Mb Na Nb q χ‖ + |Real.cos (t * Real.log y)| * ‖phaseRankOneCharacterProduct (phaseSinTwist a t) (phaseCosTwist b t) Ma Mb Na Nb q χ‖ + |Real.cos (t * Real.log y)| * ‖phaseRankOneCharacterProduct (phaseCosTwist a t) (phaseSinTwist b t) Ma Mb Na Nb q χ‖ + |Real.sin (t * Real.log y)| * ‖phaseRankOneCharacterProduct (phaseSinTwist a t) (phaseSinTwist b t) Ma Mb Na Nb q χ‖)

Pointwise absolute-value control by the four rank-one character products. The y-dependent factors occur only through their absolute values.

theorem AnalyticNumberTheory.LargeSieve.abs_sin_log_halfstep_le {M : ℕ} (hM : 3 ≤ M) {y t : ℝ} (hy0 : 1 / 2 ≤ y) (hyM : y ≤ ↑M + 1 / 2) (ht : 0 < t) : |Real.sin (t * Real.log y)| ≤ min 1 (2 * Real.log ↑M * t)

Uniform half-step sine bound for the separately chosen phase.

theorem AnalyticNumberTheory.LargeSieve.abs_sin_log_int_le {M : ℕ} (hM : 1 ≤ M) {m : ℤ} (hm1 : 1 ≤ m) (hmM : m ≤ ↑M) {t : ℝ} (ht : 0 < t) : |Real.sin (t * Real.log ↑m)| ≤ min 1 (Real.log ↑M * t)

Uniform positive-integer sine bound for either coefficient coordinate.

theorem AnalyticNumberTheory.LargeSieve.abs_cos_phase_le_one (x : ℝ) : |Real.cos x| ≤ 1

Uniform cosine bound, used for y, m, and n.

theorem AnalyticNumberTheory.LargeSieve.norm_dampedLogRectangularCharacterSum_le_four_rankOne_of_selector (a b : ℤ → ℂ) {M : ℕ} (hM : 3 ≤ M) (Y : (q : ℕ) → PrimitiveCharacter q → ℝ) {t : ℝ} (ht : 0 < t) (Ma Mb : ℤ) (Na Nb q : ℕ) (χ : PrimitiveCharacter q) (hY0 : ∀ (q : ℕ) (χ : PrimitiveCharacter q), 1 / 2 ≤ Y q χ) (hYM : ∀ (q : ℕ) (χ : PrimitiveCharacter q), Y q χ ≤ ↑M + 1 / 2) (hm1 : ∀ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), 1 ≤ m) (_hmM : ∀ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), m ≤ ↑M) (hn1 : ∀ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), 1 ≤ n) (_hnM : ∀ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), n ≤ ↑M) : ‖dampedLogRectangularCharacterSum a b (Y q χ) t Ma Mb Na Nb q χ‖ ≤ 1 / t * (min 1 (2 * Real.log ↑M * t) * ‖phaseRankOneCharacterProduct (phaseCosTwist a t) (phaseCosTwist b t) Ma Mb Na Nb q χ‖ + ‖phaseRankOneCharacterProduct (phaseSinTwist a t) (phaseCosTwist b t) Ma Mb Na Nb q χ‖ + ‖phaseRankOneCharacterProduct (phaseCosTwist a t) (phaseSinTwist b t) Ma Mb Na Nb q χ‖ + min 1 (2 * Real.log ↑M * t) * ‖phaseRankOneCharacterProduct (phaseSinTwist a t) (phaseSinTwist b t) Ma Mb Na Nb q χ‖)

Y may select a different half-step for every primitive character. The result is the pointwise interface needed before summing and invoking rankOneRectangularWeightedPrimitiveMean_le separately on the four fixed coefficient pairs.

theorem AnalyticNumberTheory.LargeSieve.sum_norm_sq_phaseSinTwist_Icc_le (a : ℤ → ℂ) (t : ℝ) (Ma : ℤ) (Na M : ℕ) (hM : 1 ≤ M) (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), ‖phaseSinTwist a t m‖ ^ 2 ≤ min 1 (Real.log ↑M * |t|) ^ 2 * ∑ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), ‖a m‖ ^ 2

Coefficient sine twists have the uniform log M energy loss needed by the rank-one mean theorem.

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

Coefficient cosine twists do not enlarge energy.

noncomputable def AnalyticNumberTheory.LargeSieve.selectorDampedLogRectangularWeightedMean (a b : ℤ → ℂ) (Y : (q : ℕ) → PrimitiveCharacter q → ℝ) (t : ℝ) (Ma Mb : ℤ) (Na Nb : ℕ) (S : Finset ℕ) : ℝ

Weighted selector mean. This is not a prefix maximum; it is only the phase-separated finite rectangular quantity to be connected to one later.

Equations

• AnalyticNumberTheory.LargeSieve.selectorDampedLogRectangularWeightedMean a b Y t Ma Mb Na Nb S = ∑ q ∈ S, ↑q / ↑q.totient * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, ‖AnalyticNumberTheory.LargeSieve.dampedLogRectangularCharacterSum a b (Y q χ) t Ma Mb Na Nb q χ‖

theorem AnalyticNumberTheory.LargeSieve.selectorDampedLogRectangularWeightedMean_le_four_rankOne (a b : ℤ → ℂ) {M : ℕ} (hM : 3 ≤ M) (Y : (q : ℕ) → PrimitiveCharacter q → ℝ) {t : ℝ} (ht : 0 < t) (Ma Mb : ℤ) (Na Nb : ℕ) (S : Finset ℕ) (hY0 : ∀ (q : ℕ) (χ : PrimitiveCharacter q), 1 / 2 ≤ Y q χ) (hYM : ∀ (q : ℕ) (χ : PrimitiveCharacter q), Y q χ ≤ ↑M + 1 / 2) (hm1 : ∀ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), 1 ≤ m) (hmM : ∀ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), m ≤ ↑M) (hn1 : ∀ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), 1 ≤ n) (hnM : ∀ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), n ≤ ↑M) : selectorDampedLogRectangularWeightedMean a b Y t Ma Mb Na Nb S ≤ 1 / t * (min 1 (2 * Real.log ↑M * t) * rankOneRectangularWeightedPrimitiveMean (phaseCosTwist a t) (phaseCosTwist b t) Ma Mb Na Nb S + rankOneRectangularWeightedPrimitiveMean (phaseSinTwist a t) (phaseCosTwist b t) Ma Mb Na Nb S + rankOneRectangularWeightedPrimitiveMean (phaseCosTwist a t) (phaseSinTwist b t) Ma Mb Na Nb S + min 1 (2 * Real.log ↑M * t) * rankOneRectangularWeightedPrimitiveMean (phaseSinTwist a t) (phaseSinTwist b t) Ma Mb Na Nb S)

Even when every character chooses its own y, the uniform phase bounds reduce the weighted selector mean to the same four y-independent rank-one means. Each term on the right is directly consumable by rankOneRectangularWeightedPrimitiveMean_le.