noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Equation20Ilx (x level : ℕ) : ℝ

The squarefree-conductor loss denoted I_{l,x} between (18) and (19).

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Equation20Ilx x level = Real.exp (6 * Real.log (2 ^ ↑level * Real.log ↑x ^ 100) / Real.log (Real.log (2 ^ ↑level * Real.log ↑x ^ 100)))

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Equation20HReal (x level k : ℕ) (ε : ℝ) : ℝ

Chen's displayed complementary-cell cutoff before rounding.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Equation20HReal x level k ε = max (2 ^ (2 * ↑level - ↑k) * ↑x ^ (-13 / 30) * Real.log ↑x ^ 400 * AnalyticNumberTheory.LargeSieve.chen1973Lemma6Equation20Ilx x level) (↑x ^ (1 / 2 - ε))

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Equation20H (x level k : ℕ) (ε : ℝ) : ℕ

The natural cutoff used in the complementary cell.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Equation20H x level k ε = ⌈AnalyticNumberTheory.LargeSieve.chen1973Lemma6Equation20HReal x level k ε⌉₊

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6Equation20H_first_le (x level k : ℕ) (ε : ℝ) : 2 ^ (2 * ↑level - ↑k) * ↑x ^ (-13 / 30) * Real.log ↑x ^ 400 * chen1973Lemma6Equation20Ilx x level ≤ ↑(chen1973Lemma6Equation20H x level k ε)

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6Equation20H_second_le (x level k : ℕ) (ε : ℝ) : ↑x ^ (1 / 2 - ε) ≤ ↑(chen1973Lemma6Equation20H x level k ε)

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20CorrectedFirstIntegral (x L level B k m H : ℕ) : ℝ

Corrected-source first half-line integral on the alpha line.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20CorrectedFirstIntegral x L level B k m H = ∫ (v : ℝ) in Set.Ioi 0, AnalyticNumberTheory.LargeSieve.chen1973Lemma6A x L level B k m H (↑(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Alpha x) + ↑v * Complex.I) / AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17CorrectedKernel x (↑(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Alpha x) + ↑v * Complex.I)

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20CorrectedSecondIntegral (x L level B k m H : ℕ) : ℝ

Corrected-source second half-line integral on the beta line.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20CorrectedSecondIntegral x L level B k m H = ∫ (v : ℝ) in Set.Ioi 0, AnalyticNumberTheory.LargeSieve.chen1973Lemma6B x L level B k m H (↑(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Beta x) + ↑v * Complex.I) / AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17CorrectedKernel x (↑(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Beta x) + ↑v * Complex.I)

def AnalyticNumberTheory.LargeSieve.Chen1973Equation20CorrectedContourMajorization (x L level B k m H : ℕ) : Prop

Corrected-source contour majorization for the complementary cell.

Equations

• AnalyticNumberTheory.LargeSieve.Chen1973Equation20CorrectedContourMajorization x L level B k m H = (AnalyticNumberTheory.LargeSieve.chen1973Lemma6NmBlockActual x L level B k m ≤ 2 * ↑x * Real.log ↑x ^ 2 * AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20CorrectedFirstIntegral x L level B k m H + 2 * ↑x ^ (1 / 2) * AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20CorrectedSecondIntegral x L level B k m H)

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20CorrectedFirstPointwiseEnvelope (x L level B k m H D Q : ℕ) (v : ℝ) : ℝ

Explicit scalar envelope for the alpha-line numerator after the fixed pair moment and the v-windowed uniform equation-(14) bound.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20CorrectedFirstPointwiseEnvelope x L level B k m H D Q v = √(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19PairSecondMoment x L level B k m (↑(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Alpha x) + ↑v * Complex.I)) * √(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19I x L level * (2 * AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19SharpConstant * (↑Q + ↑(H * H) / ↑D) * (1 + Real.log ↑(H * H)) ^ 4 + 2 * ↑Q * AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19OneSubUniformEnvelope H Q (AnalyticNumberTheory.LargeSieve.chen1973Lemma6Alpha x) v))

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20CorrectedSecondPointwiseEnvelope (x L level B k m H D Q : ℕ) (r v : ℝ) : ℝ

Explicit scalar envelope for the beta-line numerator after the fixed pair moment and the genuine multiplicative 2,4,4 Hölder reduction.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20CorrectedSecondPointwiseEnvelope x L level B k m H D Q r v = √(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19PairSecondMoment x L level B k m (↑(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Beta x) + ↑v * Complex.I)) * √(√(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19I x L level * ↑Q * ((AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19CircleFourthEnvelopeUniform Q (AnalyticNumberTheory.LargeSieve.chen1973Lemma6Beta x) v r + 1) / r) ^ 4) * √(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19I x L level * (AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19SharpConstant * (↑Q + ↑(H * H) / ↑D) * (1 + Real.log ↑(H * H)) ^ 4)))

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq20_first_le_pointwiseEnvelope (x L level B k m H D Q : ℕ) (v : ℝ) (hx : 2 ≤ x) (hH : 0 < H) (hD : 0 < D) (hDQ : D < Q) (hcell : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Ioc D Q) (hv : 0 ≤ v) : chen1973Lemma6A x L level B k m H (↑(chen1973Lemma6Alpha x) + ↑v * Complex.I) ≤ chen1973Lemma6Eq20CorrectedFirstPointwiseEnvelope x L level B k m H D Q v

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq20_second_le_pointwiseEnvelope (x L level B k m H D Q : ℕ) (r v : ℝ) (hD : 0 < D) (hQ : 2 ≤ Q) (hr : 0 < r) (hcellIoc : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Ioc D Q) (hcellIcc : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Icc 2 Q) (hdom : ∀ t ∈ Set.Icc (-v) v, Chen1973Lemma3Domain (↑(chen1973Lemma6Beta x) + ↑t * Complex.I) (chen1973Lemma6Beta x) t) (hspheres : ∀ t ∈ Set.Icc (-v) v, ∀ z ∈ Metric.sphere (↑(chen1973Lemma6Beta x) + ↑t * Complex.I) r, Chen1973Lemma3Domain z z.re z.im) (hv : 0 ≤ v) : chen1973Lemma6B x L level B k m H (↑(chen1973Lemma6Beta x) + ↑v * Complex.I) ≤ chen1973Lemma6Eq20CorrectedSecondPointwiseEnvelope x L level B k m H D Q r v

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation20_corrected_complementary_cell {x L level B D k m Q : ℕ} {ε C₁ C₂ G₁ G₂ r : ℝ} (_hcell20 : chen1973Lemma6Eq20Cell x L B D level k) (hx : 3 ≤ x) (hD : 0 < D) (hDQ : D < Q) (hQ : 2 ≤ Q) (hr : 0 < r) (horder21 : 3 ≤ chen1973PerronOrder ↑x + 1) (horder4 : 4 ≤ chen1973PerronOrder ↑x + 1) (hcellIoc : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Ioc D Q) (hcellIcc : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Icc 2 Q) (hcontA : ContinuousOn (fun (v : ℝ) => chen1973Lemma6A x L level B k m (chen1973Lemma6Equation20H x level k ε) (↑(chen1973Lemma6Alpha x) + ↑v * Complex.I)) (Set.Ici 0)) (hcontB : ContinuousOn (fun (v : ℝ) => chen1973Lemma6B x L level B k m (chen1973Lemma6Equation20H x level k ε) (↑(chen1973Lemma6Beta x) + ↑v * Complex.I)) (Set.Ici 0)) (hdomB : ∀ (t : ℝ), Chen1973Lemma3Domain (↑(chen1973Lemma6Beta x) + ↑t * Complex.I) (chen1973Lemma6Beta x) t) (hspheres : ∀ (t : ℝ), ∀ z ∈ Metric.sphere (↑(chen1973Lemma6Beta x) + ↑t * Complex.I) r, Chen1973Lemma3Domain z z.re z.im) (hgrowth₁ : ∀ v ∈ Set.Ioi 0, chen1973Lemma6Eq20CorrectedFirstPointwiseEnvelope x L level B k m (chen1973Lemma6Equation20H x level k ε) D Q v ≤ G₁ * (1 + v)) (hgrowth₂ : ∀ v ∈ Set.Ioi 0, chen1973Lemma6Eq20CorrectedSecondPointwiseEnvelope x L level B k m (chen1973Lemma6Equation20H x level k ε) D Q r v ≤ G₂ * (1 + v) ^ 2) (hpay₁ : 2 * Real.log ↑x ^ (231 / 100) / chen1973Lemma6Alpha x * G₁ * ∫ (v : ℝ) in Set.Ioi 0, AnalyticNumberTheory.LargeSieve.eq20CorrectedLinearDecayWeight✝ v ≤ C₁ / Real.log ↑x ^ 22) (hpay₂ : 2 * Real.log ↑x ^ (22 / 5) / chen1973Lemma6Beta x * G₂ * ∫ (v : ℝ) in Set.Ioi 0, AnalyticNumberTheory.LargeSieve.eq20CorrectedQuadraticDecayWeight✝ v ≤ C₂ * ↑x ^ (1 / 2) / Real.log ↑x ^ 20) (hcontour : Chen1973Equation20CorrectedContourMajorization x L level B k m (chen1973Lemma6Equation20H x level k ε)) : chen1973Lemma6NmBlockActual x L level B k m ≤ 2 * (C₁ + C₂) * ↑x / Real.log ↑x ^ 20