theorem AnalyticNumberTheory.LargeSieve.eq20Alpha_source_geometry {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq20ComplementarySourceParameters x L B lastD level k) : chen1973Lemma6Eq20SourceQ L level = 2 * chen1973Lemma6Eq20SourceD L level ∧ B * 2 ^ k ≤ chen1973Lemma6Eq20SourceQ L level ∧ ↑(chen1973Lemma6Eq20SourceQ L level) ≤ eq19AlphaQ0 x level ∧ eq19AlphaQ0 x level ≤ 2 * ↑(chen1973Lemma6Eq20SourceQ L level)

theorem AnalyticNumberTheory.LargeSieve.eq20Alpha_Q0_log {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq20ComplementarySourceParameters x L B lastD level k) (hcap : ↑(chen1973Lemma6Eq20SourceQ L level) ≤ 2 * ↑x ^ (1 / 2)) : Real.log (eq19AlphaQ0 x level) ≤ 4 * Real.log ↑x

theorem AnalyticNumberTheory.LargeSieve.eq20Alpha_I_log90_pair {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq20ComplementarySourceParameters x L B lastD level k) (hcap : ↑(chen1973Lemma6Eq20SourceQ L level) ≤ 2 * ↑x ^ (1 / 2)) (hu : 5400 ^ 2 ≤ Real.log ↑x) (htt : 60 ≤ Real.log (Real.log (eq19AlphaQ0 x level))) : chen1973Lemma6Equation20Ilx x level * Real.log ↑x ^ 90 ≤ 2 * ↑(B * 2 ^ k)

theorem AnalyticNumberTheory.LargeSieve.eq20Alpha_first_height_identity (x level k B : ℕ) (hx : 0 < x) (hB : 0 < B) : 2 ^ (2 * ↑level - ↑k) * ↑x ^ (-13 / 30) * Real.log ↑x ^ 400 * chen1973Lemma6Equation20Ilx x level = eq19AlphaQ0 x level ^ 2 * Real.log ↑x ^ 200 * chen1973Lemma6Equation20Ilx x level * ↑B / (↑(B * 2 ^ k) * ↑x ^ (13 / 30))

theorem AnalyticNumberTheory.LargeSieve.eq20Alpha_height_weight {x L B lastD level k : ℕ} {ε : ℝ} (P : Chen1973Lemma6Eq20ComplementarySourceParameters x L B lastD level k) (hu : 2 ≤ Real.log ↑x) (hW : chen1973Lemma6Eq19I x L level ^ 2 ≤ chen1973Lemma6Equation20Ilx x level) : ↑(chen1973Lemma6Eq20SourceQ L level) ^ 2 / ↑(B * 2 ^ k) * Real.log ↑x ^ 100 * chen1973Lemma6Eq19I x L level ^ 2 ≤ ↑(chen1973Lemma6Equation20H x level k ε)

theorem AnalyticNumberTheory.LargeSieve.eq20Alpha_height_logs {x L B lastD level k : ℕ} {ε : ℝ} (P : Chen1973Lemma6Eq20ComplementarySourceParameters x L B lastD level k) (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1 / 10) (hcap : ↑(chen1973Lemma6Eq20SourceQ L level) ≤ 2 * ↑x ^ (1 / 2)) (htt : 60 ≤ Real.log (Real.log (eq19AlphaQ0 x level))) : 2 ≤ chen1973Lemma6Equation20H x level k ε ∧ 1 + Real.log ↑(chen1973Lemma6Equation20H x level k ε + 1) ≤ 120 * Real.log ↑x ∧ Real.log ↑(chen1973Lemma6Eq20SourceQ L level) ≤ 4 * Real.log ↑x

noncomputable def AnalyticNumberTheory.LargeSieve.eq20AlphaEffectiveWeight (x L level B k : ℕ) : ℝ

Equations

• AnalyticNumberTheory.LargeSieve.eq20AlphaEffectiveWeight x L level B k = AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19I x L level * √(↑(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20SourceQ L level) / ↑(B * 2 ^ k))

theorem AnalyticNumberTheory.LargeSieve.eq20Alpha_effective_square (x L level B k : ℕ) : eq20AlphaEffectiveWeight x L level B k ^ 2 = chen1973Lemma6Eq19I x L level ^ 2 * (↑(chen1973Lemma6Eq20SourceQ L level) / ↑(B * 2 ^ k))

theorem AnalyticNumberTheory.LargeSieve.eq20Alpha_effective_one {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq20ComplementarySourceParameters x L B lastD level k) : 1 ≤ eq20AlphaEffectiveWeight x L level B k

theorem AnalyticNumberTheory.LargeSieve.eq20Alpha_source_weight_budget : ∃ (X₀ : ℝ), ∀ (x : ℕ), X₀ ≤ ↑x → ∀ (L B lastD level k : ℕ) (ε : ℝ), 0 ≤ ε → ε ≤ 1 / 10 → Chen1973Lemma6Eq20ComplementarySourceParameters x L B lastD level k → ↑(chen1973Lemma6Eq20SourceQ L level) ≤ 2 * ↑x ^ (1 / 2) → eq20AlphaEffectiveWeight x L level B k ^ 2 * Real.log ↑x ^ 90 ≤ 2 * ↑(chen1973Lemma6Eq20SourceQ L level) ∧ ↑(chen1973Lemma6Eq20SourceQ L level) * Real.log ↑x ^ 100 * eq20AlphaEffectiveWeight x L level B k ^ 2 ≤ ↑(chen1973Lemma6Equation20H x level k ε) ∧ 2 ≤ chen1973Lemma6Equation20H x level k ε ∧ 1 + Real.log ↑(chen1973Lemma6Equation20H x level k ε + 1) ≤ 120 * Real.log ↑x ∧ Real.log ↑(chen1973Lemma6Eq20SourceQ L level) ≤ 4 * Real.log ↑x

Uniform effective-weight ledger for the literal complementary maximum/ceiling.

theorem AnalyticNumberTheory.LargeSieve.eq20Alpha_pair_shape {Q Y D σ : ℝ} (hQY : Y ≤ Q) (hY : 1 ≤ Y) (hD : 1 ≤ D) (hσ : 1 ≤ σ) : (Q + Y / D) * Y ^ (1 - 2 * σ) ≤ 3 * (Q / Y)

theorem AnalyticNumberTheory.LargeSieve.eq20Alpha_actual_numerator_small : ∃ (X₀ : ℝ), ∀ (x : ℕ), X₀ ≤ ↑x → ∀ (L B lastD level k m : ℕ) (ε : ℝ), 0 ≤ ε → ε ≤ 1 / 10 → Chen1973Lemma6Eq20ComplementarySourceParameters x L B lastD level k → ↑(chen1973Lemma6Eq20SourceQ L level) ≤ 2 * ↑x ^ (1 / 2) → ∀ (v : ℝ), 0 ≤ v → chen1973Lemma6A x L level B k m (chen1973Lemma6Equation20H x level k ε) (↑(chen1973Lemma6Alpha x) + ↑v * Complex.I) ≤ eq19AlphaNumeratorConstant / Real.log ↑x ^ 40 * (1 + v)

Actual complementary alpha numerator, at the true equation-(20) height.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq20_alpha_integrable_and_small : ∃ (C : ℝ), 0 < C ∧ ∃ (X₀ : ℝ), ∀ (x : ℕ), X₀ ≤ ↑x → ∀ (L B lastD level k m : ℕ) (ε : ℝ), 0 ≤ ε → ε ≤ 1 / 10 → Chen1973Lemma6Eq20ComplementarySourceParameters x L B lastD level k → ↑(chen1973Lemma6Eq20SourceQ L level) ≤ 2 * ↑x ^ (1 / 2) → MeasureTheory.IntegrableOn (fun (v : ℝ) => chen1973Lemma6A x L level B k m (chen1973Lemma6Equation20H x level k ε) (↑(chen1973Lemma6Alpha x) + ↑v * Complex.I) / chen1973Lemma6Eq17CorrectedKernel x (↑(chen1973Lemma6Alpha x) + ↑v * Complex.I)) (Set.Ioi 0) MeasureTheory.volume ∧ chen1973Lemma6Eq20CorrectedFirstIntegral x L level B k m (chen1973Lemma6Equation20H x level k ε) ≤ C / Real.log ↑x ^ 22

The actual corrected alpha integral at the original equation-(20) height is uniformly small. The cutoff and constant precede all cell parameters and epsilon.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq20_alpha_contribution_small : ∃ (C : ℝ), 0 < C ∧ ∃ (X₀ : ℝ), ∀ (x : ℕ), X₀ ≤ ↑x → ∀ (L B lastD level k m : ℕ) (ε : ℝ), 0 ≤ ε → ε ≤ 1 / 10 → Chen1973Lemma6Eq20ComplementarySourceParameters x L B lastD level k → ↑(chen1973Lemma6Eq20SourceQ L level) ≤ 2 * ↑x ^ (1 / 2) → 12 * ↑x * Real.log ↑x ^ 2 * chen1973Lemma6Eq20CorrectedFirstIntegral x L level B k m (chen1973Lemma6Equation20H x level k ε) ≤ C * ↑x / Real.log ↑x ^ 20

Including the literal outside factor 12*x*log(x)^2.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation20_small_alpha_actual_beta : ∃ (C : ℝ), 0 < C ∧ ∃ (X₀ : ℝ), ∀ (x : ℕ), X₀ ≤ ↑x → ∀ (L B lastD level k m : ℕ) (ε : ℝ), 0 ≤ ε → ε ≤ 1 / 10 → Chen1973Lemma6Eq20ComplementarySourceParameters x L B lastD level k → ↑(chen1973Lemma6Eq20SourceQ L level) ≤ 2 * ↑x ^ (1 / 2) → chen1973Lemma6NmBlockActual x L level B k m ≤ C * ↑x / Real.log ↑x ^ 20 + 2 * ↑x ^ (1 / 2) * chen1973Lemma6Eq20CorrectedSecondIntegral x L level B k m (chen1973Lemma6Equation20H x level k ε)

Actual corrected contour wiring: only the genuine beta integral is unpaid.