def AnalyticNumberTheory.LargeSieve.rawFiniteZeroFreeInput (x L : ℕ) : Prop

Only literal nonvanishing on the enlarged finite rectangle.

Equations

• AnalyticNumberTheory.LargeSieve.rawFiniteZeroFreeInput x L = ∀ d ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma6ConductorBlock x L 0, ∀ (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter d) (s : ℂ), 1 - 2 / √(Real.log ↑x) ≤ s.re → s.re ≤ 2 → |s.im| ≤ Real.log ↑x ^ 2 + 1 → AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimitiveLValue d s χ ≠ 0

theorem AnalyticNumberTheory.LargeSieve.finite_sigma_geometry {x : ℕ} (hu : 64 ≤ Real.log ↑x) : 1 / 2 ≤ chen1973Lemma6Eq21Sigma x ∧ chen1973Lemma6Alpha x ≤ 2

theorem AnalyticNumberTheory.LargeSieve.finite_power_gap {x : ℕ} {y : ℝ} (hu : 64 ≤ Real.log ↑x) (hy : 1 < y) (hyx : y ≤ ↑x) : y ^ chen1973Lemma6Alpha x ≤ y ^ chen1973Lemma6Eq21Sigma x * Real.exp (1 + √(Real.log ↑x))

theorem AnalyticNumberTheory.LargeSieve.finite_star_payment {x : ℕ} {y : ℝ} (hu : 64 ≤ Real.log ↑x) (hy : 1 < y) (hyx : y ≤ ↑x) (hly : Real.log ↑x / 3 ≤ Real.log y) (hleft : ∀ (σ : ℝ), 1 / 2 ≤ σ → eq21FiniteScalarMbar (Real.log ↑x) * (σ⁻¹ + Real.log (Real.log ↑x ^ 2)) ≤ Real.log ↑x / 3) (htail : 8 * Real.exp (1 + √(Real.log ↑x)) * (chen1973PerronScale ↑x / Real.log ↑x ^ 2) ^ (chen1973PerronOrder ↑x + 1) * Real.log ↑x ^ 2 ≤ 1) : have u := Real.log ↑x; have σ := chen1973Lemma6Eq21Sigma x; have α := chen1973Lemma6Alpha x; have M := eq21FiniteScalarMbar u; have N := chen1973PerronOrder ↑x + 1; y ^ σ * M * (σ⁻¹ + Real.log (u ^ 2)) / (Real.pi * Real.log y) + y ^ α / (Real.pi * Real.log y) * (chen1973PerronScale ↑x / u ^ 2) ^ N * (6 * u ^ 2 / ↑N + (α - σ) * M / u ^ 2) ≤ 2 * y ^ σ

Both finite-contour pieces are paid, retaining the actual smoothing floor.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_actualTerm_two_eventually_of_finiteZeroFree : ∃ (X₀ : ℕ), ∀ x ≥ X₀, ∀ (L B k m l₂ : ℕ), Chen1973Lemma6Eq21SourceParameters x L B k m l₂ → rawFiniteZeroFreeInput x L → ∀ d ∈ chen1973Lemma6ConductorBlock x L 0, ∀ (χ : PrimitiveCharacter d), ∀ pp ∈ chen1973Lemma6PrimePairShell x B k m, ‖chen1973Lemma6ActualPhi x d χ pp * ↑χ ↑(pp.1 * pp.2)‖ / Real.log (↑x / (↑pp.1 * ↑pp.2)) ≤ 2 * (↑x / (↑pp.1 * ↑pp.2)) ^ chen1973Lemma6Eq21Sigma x

Uniform actual-term estimate, derived only from finite raw nonvanishing.

theorem AnalyticNumberTheory.LargeSieve.finite_actual_Nm_le_four {x L B k m l₂ : ℕ} (P : Chen1973Lemma6Eq21SourceParameters x L B k m l₂) (hterm : ∀ d ∈ chen1973Lemma6ConductorBlock x L 0, ∀ (χ : PrimitiveCharacter d), ∀ pp ∈ chen1973Lemma6PrimePairShell x B k m, ‖chen1973Lemma6ActualPhi x d χ pp * ↑χ ↑(pp.1 * pp.2)‖ / Real.log (↑x / (↑pp.1 * ↑pp.2)) ≤ 2 * (↑x / (↑pp.1 * ↑pp.2)) ^ chen1973Lemma6Eq21Sigma x) : chen1973Lemma6NmBlockActual x L 0 B k m ≤ 4 * Real.log ↑x ^ 200 * chen1973Lemma6Eq21PrimeSum x

Actual finite character and prime-pair sums; no shifted whole-line object.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation21_levelZero_eventually_of_finiteZeroFree : ∃ (X₀ : ℕ), ∀ x ≥ X₀, ∀ (L B k m l₂ : ℕ), Chen1973Lemma6Eq21SourceParameters x L B k m l₂ → rawFiniteZeroFreeInput x L → chen1973Lemma6NmBlockActual x L 0 B k m ≤ ↑x / Real.log ↑x ^ 20

Equation (21) for actual Nm under only the finite nonvanishing rectangle.

theorem AnalyticNumberTheory.LargeSieve.finite_rawInput_of_fixedSiegel (c : ℝ) (hc : 0 < c) : ∃ (X₀ : ℕ), ∀ x ≥ X₀, ∀ (L B k m l₂ : ℕ), Chen1973Lemma6Eq21SourceParameters x L B k m l₂ → (∀ d ∈ chen1973Lemma6ConductorBlock x L 0, ∀ (χ : PrimitiveCharacter d), ↑χ ^ 2 = 1 → c * ↑d ^ (-(1 / 10000)) ≤ (chen1973Lemma6PrimitiveLValue d 1 χ).re) → rawFiniteZeroFreeInput x L

Fixed-c quadratic L(1) data produce the finite rectangle. No Siegel lower bound itself is asserted, and c is fixed before the threshold.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation21_levelZero_eventually_of_fixedSiegel (c : ℝ) (hc : 0 < c) : ∃ (X₀ : ℕ), ∀ x ≥ X₀, ∀ (L B k m l₂ : ℕ), Chen1973Lemma6Eq21SourceParameters x L B k m l₂ → (∀ d ∈ chen1973Lemma6ConductorBlock x L 0, ∀ (χ : PrimitiveCharacter d), ↑χ ^ 2 = 1 → c * ↑d ^ (-(1 / 10000)) ≤ (chen1973Lemma6PrimitiveLValue d 1 χ).re) → chen1973Lemma6NmBlockActual x L 0 B k m ≤ ↑x / Real.log ↑x ^ 20

Final actual Nm bound, conditional solely on fixed-c raw quadratic L(1) lower bounds. All analytic finite-contour and nonquadratic inputs are derived.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation21_levelZero_eventually_of_rawQuadraticL1 (c : ℝ) (hc : 0 < c) : ∃ (X₀ : ℕ), ∀ x ≥ X₀, ∀ (L B k m l₂ : ℕ), Chen1973Lemma6Eq21SourceParameters x L B k m l₂ → (∀ (d : ℕ) (hd : d ∈ chen1973Lemma6ConductorBlock x L 0), have this := ⋯; ∀ (χ : PrimitiveCharacter d), ↑χ ^ 2 = 1 → c * ↑d ^ (-(1 / 10000)) ≤ (DirichletCharacter.LFunction (↑χ) 1).re) → chen1973Lemma6NmBlockActual x L 0 B k m ≤ ↑x / Real.log ↑x ^ 20

Literal Dirichlet L-function formulation of the fixed-c terminal. The local NeZero instance is derived from actual block membership, not assumed.