The complete Pan source cell after Perron truncation

Both short and long polynomials are retained. The common half-step represents the exact integer hyperbola, so there is no omitted boundary divisor term.

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.perron_polynomial_eq (S : Finset ℕ) (A : ℕ → ℂ) (hS : ∀ n ∈ S, 0 < n) {q : ℕ} (χ : PrimitiveCharacter q) (s : ℂ) : MathlibNt.SieveTheory.LiuWeight.liuPanPerronDirichletPolynomial S A (↑χ) s = polynomial S A χ s

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.full_prime_polynomial_split {q : ℕ} (m H M : ℕ) (hHM : H ≤ M) (χ : PrimitiveCharacter q) (s : ℂ) : polynomial (Finset.Icc 1 M) (panSourceD m) χ s = panShortF₁ m H χ s + polynomial (Finset.Ioc H M) (panSourceD m) χ s

noncomputable def AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.halfStepLongKernel {q : ℕ} (f : ℕ → ℂ) (m H y A₁ A₂ k : ℕ) (χ : PrimitiveCharacter q) (T : ℝ) (s : ℂ) : ℂ

Equations

• AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.halfStepLongKernel f m H y A₁ A₂ k χ T s = AnalyticNumberTheory.LargeSieve.panDyadicG f m A₁ A₂ k χ s * AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.longF₂ m H T χ s * ↑(MathlibNt.SieveTheory.LiuWeight.liuPanPerronHalfStep y) ^ s / s

noncomputable def AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.halfStepLongIntegral {q : ℕ} (f : ℕ → ℂ) (m H y A₁ A₂ k : ℕ) (χ : PrimitiveCharacter q) (σ T : ℝ) : ℂ

Equations

• AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.halfStepLongIntegral f m H y A₁ A₂ k χ σ T = (↑(2 * Real.pi))⁻¹ * ∫ (t : ℝ) in -T..T, AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.halfStepLongKernel f m H y A₁ A₂ k χ T (MathlibNt.SieveTheory.LiuWeight.liuPanPerronLine σ t)

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.longF₂_differentiable {q : ℕ} (m H : ℕ) (T : ℝ) (χ : PrimitiveCharacter q) : Differentiable ℂ (longF₂ m H T χ)

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.halfStepLongKernel_line_continuous {q : ℕ} (f : ℕ → ℂ) (m H y A₁ A₂ k : ℕ) (χ : PrimitiveCharacter q) (T σ : ℝ) (hσ : 0 < σ) : Continuous fun (t : ℝ) => halfStepLongKernel f m H y A₁ A₂ k χ T (MathlibNt.SieveTheory.LiuWeight.liuPanPerronLine σ t)

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.perron_integral_eq_short_add_long {q : ℕ} (f : ℕ → ℂ) (m H y A₁ A₂ k : ℕ) (χ : PrimitiveCharacter q) {σ T : ℝ} (hσ : 1 / 2 ≤ σ) (hT : 0 ≤ T) (hH : H ≤ ⌊T⌋₊) : MathlibNt.SieveTheory.LiuWeight.liuPanTruncatedPerronIntegral (Finset.Ioc (2 ^ k * A₁) (min (2 ^ (k + 1) * A₁) A₂)) (Finset.Icc 1 ⌊T⌋₊) (panSourceG f m) (panSourceD m) (↑χ) σ T y = halfStepShortIntegral f m H y A₁ A₂ k χ σ T + halfStepLongIntegral f m H y A₁ A₂ k χ σ T

Exact passage from the exponential-form Perron integral to both of the paper's finite complex-power polynomials.

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.source_cell_perron_shift {q x y : ℕ} (f : ℕ → ℂ) (hf : ∀ (n : ℕ), ‖f n‖ ≤ 1) (m H A₁ A₂ k : ℕ) (χ : PrimitiveCharacter q) (hx : 4 ≤ Real.log ↑x) (hy : 1 ≤ y) (hyx : y ≤ x) (hAy : A₂ ≤ y) (hHx : H ≤ x) : ‖panSourceCharacterAmplitude (panSourceG f m) (panSourceD m) y (2 ^ k * A₁) (min (2 ^ (k + 1) * A₁) A₂) χ - (halfStepShortIntegral f m H y A₁ A₂ k χ (1 / 2) (panSourceHeight x) + halfStepLongIntegral f m H y A₁ A₂ k χ (panSourceSigma x) (panSourceHeight x))‖ ≤ 388 / ↑x ^ 2

The actual complete source cell, after shifting only the short integral. The long integral has not been discarded or replaced by a rowwise bound.

noncomputable def AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.sourceCell (f : ℕ → ℂ) (m y A₁ A₂ k : ℕ) (R : ℝ) : ℝ

Equations

• AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.sourceCell f m y A₁ A₂ k R = ∑ q ∈ AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.conductorCell R, (↑q.totient)⁻¹ * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, ‖AnalyticNumberTheory.LargeSieve.panSourceCharacterAmplitude (AnalyticNumberTheory.LargeSieve.panSourceG f m) (AnalyticNumberTheory.LargeSieve.panSourceD m) y (2 ^ k * A₁) (min (2 ^ (k + 1) * A₁) A₂) χ‖

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.primitive_cell_constant_le {R E : ℝ} (hR : 1 ≤ R) (hE : 0 ≤ E) : ∑ q ∈ conductorCell R, (↑q.totient)⁻¹ * ∑ _χ : PrimitiveCharacter q, E ≤ 2 * R * E

The reciprocal-totient primitive mass pays the number of conductors, not the sum of their sizes.

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.source_cell_le_integral_means {x y : ℕ} {R : ℝ} (f : ℕ → ℂ) (hf : ∀ (n : ℕ), ‖f n‖ ≤ 1) (m A₁ A₂ k : ℕ) (hx : 4 ≤ Real.log ↑x) (hy : 1 ≤ y) (hyx : y ≤ x) (hAy : A₂ ≤ y) (hR : 1 ≤ R) (hH : shortCutoff R ≤ x) : sourceCell f m y A₁ A₂ k R ≤ ∑ q ∈ conductorCell R, (↑q.totient)⁻¹ * ∑ χ : PrimitiveCharacter q, ‖halfStepShortIntegral f m (shortCutoff R) y A₁ A₂ k χ (1 / 2) (panSourceHeight x)‖ + ∑ q ∈ conductorCell R, (↑q.totient)⁻¹ * ∑ χ : PrimitiveCharacter q, ‖halfStepLongIntegral f m (shortCutoff R) y A₁ A₂ k χ (panSourceSigma x) (panSourceHeight x)‖ + 2 * R * (388 / ↑x ^ 2)

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.source_cell_bound_of_means {x y : ℕ} {R M₁ M₂ : ℝ} (f : ℕ → ℂ) (hf : ∀ (n : ℕ), ‖f n‖ ≤ 1) (m A₁ A₂ k : ℕ) (hx : 4 ≤ Real.log ↑x) (hy : 1 ≤ y) (hyx : y ≤ x) (hAy : A₂ ≤ y) (hR : 1 ≤ R) (hH : shortCutoff R ≤ x) (hM₁ : 0 ≤ M₁) (hM₂ : 0 ≤ M₂) (hs : ∀ (s : ℂ), 1 / 2 ≤ s.re → shortMean f m A₁ A₂ k R s ≤ M₁) (hl : ∀ (s : ℂ), 1 ≤ s.re → longMean f m A₁ A₂ k R (panSourceHeight x) s ≤ M₂) : sourceCell f m y A₁ A₂ k R ≤ 6 * MathlibNt.SieveTheory.LiuWeight.liuPanPerronHalfStep y ^ (1 / 2) * M₁ * Real.log (1 + panSourceHeight x) + 6 * MathlibNt.SieveTheory.LiuWeight.liuPanPerronHalfStep y ^ panSourceSigma x * M₂ * Real.log (1 + panSourceHeight x) + 2 * R * (388 / ↑x ^ 2)

A finite-height bound for the genuine cell. Both primitive means are analytic inputs to this integration lemma and are discharged below.

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.chosen_source_cell_uniform : ∃ (C₁ : ℝ) (C₂ : ℝ), 0 < C₁ ∧ 0 < C₂ ∧ ∀ (B ε : ℝ), 0 ≤ B → 0 < ε → ∃ (X₀ : ℕ), ∀ (x : ℕ), X₀ ≤ x → ∀ (y j m A₁ A₂ k : ℕ) (f : ℕ → ℂ), 1 ≤ Real.log ↑y → y ≤ x → A₂ ≤ y → conductorRadius x B j ≤ upperConductor x B → ↑A₂ ≤ ↑x ^ (1 - ε) → Real.log ↑y ^ (2 * B) ≤ ↑A₁ → (∀ (n : ℕ), ‖f n‖ ≤ 1) → sourceCell f m y A₁ A₂ k (conductorRadius x B j) ≤ 6 * MathlibNt.SieveTheory.LiuWeight.liuPanPerronHalfStep y ^ (1 / 2) * (C₁ * √↑x * Real.log ↑x ^ (1 - B)) * Real.log (1 + panSourceHeight x) + 6 * MathlibNt.SieveTheory.LiuWeight.liuPanPerronHalfStep y ^ panSourceSigma x * (C₂ * Real.log ↑x ^ 2 / Real.log ↑y ^ B) * Real.log (1 + panSourceHeight x) + 776 / ↑x

The genuine source-cell bound with both polynomial means discharged. The constants precede all source functions, parameters, and spectral heights.

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.log_source_height_le {x : ℕ} (hx : 1 ≤ Real.log ↑x) : Real.log (1 + panSourceHeight x) ≤ 3 * Real.log ↑x ^ 2

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.halfStep_source_power_le_linear {x y : ℕ} (hx : 4 ≤ Real.log ↑x) (hy : 1 ≤ y) (hyx : y ≤ x) : MathlibNt.SieveTheory.LiuWeight.liuPanPerronHalfStep y ^ panSourceSigma x ≤ 2 * Real.exp 2 * ↑y

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.chosen_source_cell_log_saving : ∃ (C : ℝ), 0 < C ∧ ∀ (B ε : ℝ), 0 ≤ B → 0 < ε → ∃ (X₀ : ℕ), ∀ (x : ℕ), X₀ ≤ x → ∀ (j m A₁ A₂ k : ℕ) (f : ℕ → ℂ), A₂ ≤ x → conductorRadius x B j ≤ upperConductor x B → ↑A₂ ≤ ↑x ^ (1 - ε) → Real.log ↑x ^ (2 * B) ≤ ↑A₁ → (∀ (n : ℕ), ‖f n‖ ≤ 1) → sourceCell f m x A₁ A₂ k (conductorRadius x B j) ≤ C * ↑x * Real.log ↑x ^ (4 - B) + 776 / ↑x

At the full source endpoint, each real conductor/source cell has an arbitrary logarithmic saving. This is an unconditional analytic producer, not the weighted aggregate over induced conductors.