Documentation

MathlibNt.AnalyticNumberTheory.Chen1973.Chen1973Lemma6Equation20CorrectedFinal

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

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

Equations
Instances For
    source
    noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Equation20HReal (x level k : ℕ) (ε : ℝ) :
    ℝ

    Chen's displayed complementary-cell cutoff before rounding.

    Equations
    Instances For
      source
      noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Equation20H (x level k : ℕ) (ε : ℝ) :
      ℕ

      The natural cutoff used in the complementary cell.

      Equations
      Instances For
        source
        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 ε)
        source
        theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6Equation20H_second_le (x level k : ℕ) (ε : ℝ) :
        ↑x ^ (1 / 2 - ε) ≤ ↑(chen1973Lemma6Equation20H x level k ε)
        source
        noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20CorrectedFirstIntegral (x L level B k m H : ℕ) :
        ℝ

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

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

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

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

            Corrected-source contour majorization for the complementary cell.

            Equations
            Instances For
              source
              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
              Instances For
                source
                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
                Instances For
                  source
                  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
                  source
                  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
                  source
                  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