Documentation

MathlibNt.AnalyticNumberTheory.Chen1973.Chen1973Lemma6Equation17CorrectedAssembly

source
noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17CorrectedRadialKernel (x _level : ℕ) (s : ℂ) :
ℝ

Assembly-facing alias for the rigorous corrected-source kernel. The conductor level is retained only to keep the equation-(17) integral API aligned with the surrounding block notation.

Equations
Instances For
    source
    noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17CorrectedRadialFirstIntegral (x L level B k m H : ℕ) :
    ℝ
    Equations
    Instances For
      source
      noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17CorrectedRadialSecondIntegral (x L level B k m H : ℕ) :
      ℝ
      Equations
      Instances For
        source
        noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17CorrectedRadialFirstFullIntegral (x L level B k m H : ℕ) :
        ℝ
        Equations
        Instances For
          source
          noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17CorrectedRadialSecondFullIntegral (x L level B k m H : ℕ) :
          ℝ
          Equations
          Instances For
            source
            theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17CorrectedRadialFirstFullIntegral_eq_two_mul_half {x L level B k m H : ℕ} (hlevel : 1 ≤ level) (hx : 1 < x) :
            chen1973Lemma6Eq17CorrectedRadialFirstFullIntegral x L level B k m H = 2 * chen1973Lemma6Eq17CorrectedRadialFirstIntegral x L level B k m H
            source
            theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17CorrectedRadialSecondFullIntegral_eq_two_mul_half {x L level B k m H : ℕ} (hlevel : 1 ≤ level) (hx : 1 < x) :
            chen1973Lemma6Eq17CorrectedRadialSecondFullIntegral x L level B k m H = 2 * chen1973Lemma6Eq17CorrectedRadialSecondIntegral x L level B k m H
            source
            noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Equation17CorrectedRadialRHS (x L level B k m H : ℕ) :
            ℝ
            Equations
            Instances For
              source
              def AnalyticNumberTheory.LargeSieve.Chen1973Equation17CorrectedRadialContourMajorization (x L level B k m H : ℕ) :
              Prop
              Equations
              Instances For
                source
                def AnalyticNumberTheory.LargeSieve.Chen1973Equation17AlphaLogDerivativePayment (x L level : ℕ) :
                Prop

                The pointwise alpha-line logarithmic-derivative estimate paid by the external (log x)^2 factor in the corrected equation-(17) assembly. The explicit absolute constant 6 comes from the absolute twisted von Mangoldt series; the current source quantity A remains free of L'/L.

                Equations
                Instances For
                  source
                  theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_scaledKernel_beta_le_source {x level : ℕ} (hx : 3 ≤ x) (t : ℝ) :
                  ‖↑(1 / (2 * Real.pi)) * ↑x ^ (↑(chen1973Lemma6Beta x) + ↑t * Complex.I) * chen1973MellinKernel (↑x) (↑(chen1973Lemma6Beta x) + ↑t * Complex.I)‖ ≤ ↑x ^ (1 / 2) / chen1973Lemma6Eq17CorrectedRadialKernel x level (↑(chen1973Lemma6Beta x) + ↑t * Complex.I)

                  The original beta-line prefactor is sqrt x (Chen p.121).

                  source
                  theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_alphaLogDerivative_le_six_mul_log_sq {x d : ℕ} [NeZero d] (χ : PrimitiveCharacter d) (hd : 1 < d) (hx : 3 ≤ x) (t : ℝ) :
                  ‖chen1973PrimitiveLDeriv d (↑(chen1973Lemma6Alpha x) + ↑t * Complex.I) χ / chen1973Lemma6PrimitiveLValue d (↑(chen1973Lemma6Alpha x) + ↑t * Complex.I) χ‖ ≤ 6 * Real.log ↑x ^ 2

                  On Chen's alpha line, the absolute twisted von Mangoldt series pays the logarithmic derivative with the explicit universal constant 6.

                  source
                  theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_corrected_radial_contourMajorization {x L level B k m H : ℕ} (hx : 3 ≤ x) (hlevel : 1 ≤ level) (hAlpha : Chen1973Equation17AlphaLogDerivativePayment x L level) :
                  Chen1973Equation17CorrectedRadialContourMajorization x L level B k m H
                  source
                  theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation17_corrected_radial {x L level B k m H : ℕ} (hx : 3 ≤ x) (hlevel : 1 ≤ level) (hAlpha : Chen1973Equation17AlphaLogDerivativePayment x L level) :
                  chen1973Lemma6NmBlockActual x L level B k m ≤ 12 * ↑x * Real.log ↑x ^ 2 * chen1973Lemma6Eq17CorrectedRadialFirstIntegral x L level B k m H + 2 * ↑x ^ (1 / 2) * chen1973Lemma6Eq17CorrectedRadialSecondIntegral x L level B k m H
                  source
                  theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation17_alphaLogDerivativePayment_unconditional {x L level : ℕ} (hx : 3 ≤ x) (hlevel : 1 ≤ level) :
                  Chen1973Equation17AlphaLogDerivativePayment x L level

                  The alpha-line payment is unconditional: absolute convergence of the -L'/L von Mangoldt series supplies the explicit coefficient 6.

                  source
                  theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation17_corrected_radial_unconditional {x L level B k m H : ℕ} (hx : 3 ≤ x) (hlevel : 1 ≤ level) :
                  chen1973Lemma6NmBlockActual x L level B k m ≤ 12 * ↑x * Real.log ↑x ^ 2 * chen1973Lemma6Eq17CorrectedRadialFirstIntegral x L level B k m H + 2 * ↑x ^ (1 / 2) * chen1973Lemma6Eq17CorrectedRadialSecondIntegral x L level B k m H

                  Unconditional corrected equation-(17) assembly. The source A remains unchanged; the absolute alpha-line logarithmic derivative is paid only in the first displayed coefficient.