Documentation

MathlibNt.AnalyticNumberTheory.Chen1973.Chen1973Lemma6Equation17BromwichSum

Chen 1973, Lemma 6, equation (17): finite Bromwich sums #

This module closes the finite-sum part of the passage to (17). It proves that Chen's actual finite Φ is a Bochner integral over the full real Bromwich line, exchanges that integral with the finite von-Mangoldt, prime-pair, and primitive character sums, and then records the resulting exact conductor-block identity. No equation-(17) majorization or contour-deformation conclusion is assumed.

source
theorem AnalyticNumberTheory.LargeSieve.integrable_chen1973BromwichIntegrand {x y : ℝ} (hx : 1 < x) (hy : 0 < y) :
MeasureTheory.Integrable (fun (t : ℝ) => chen1973BromwichIntegrand x y t) MeasureTheory.volume

The Bromwich integrand is Bochner integrable for every positive argument.

source
noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6BromwichVonMangoldtIntegrand (x d : ℕ) (χ : PrimitiveCharacter d) (pp : ℕ × ℕ) (t : ℝ) :
ℂ

The literal finite von-Mangoldt/character integrand whose full-line integral is chen1973Lemma6ActualPhi. The normalization 1/(2π) is inside the integrand, so the result is a single Bochner integral.

Equations
Instances For
    source
    theorem AnalyticNumberTheory.LargeSieve.integrable_chen1973Lemma6BromwichVonMangoldtTerm {x d n : ℕ} {pp : ℕ × ℕ} (χ : PrimitiveCharacter d) (hx : 1 < x) (hp₁ : 0 < pp.1) (hp₂ : 0 < pp.2) :
    MeasureTheory.Integrable (fun (t : ℝ) => ↑(ArithmeticFunction.vonMangoldt n) * (↑(1 / (2 * Real.pi)) * chen1973BromwichIntegrand (↑x) (↑x / (↑pp.1 * ↑pp.2 * ↑n)) t) * ↑χ ↑n) MeasureTheory.volume

    Every summand in the finite von-Mangoldt Bromwich sum is Bochner integrable. The n=0 term vanishes; positive n use the closed Mellin integrability theorem.

    source
    theorem AnalyticNumberTheory.LargeSieve.integrable_chen1973Lemma6BromwichVonMangoldtIntegrand {x d : ℕ} {pp : ℕ × ℕ} (χ : PrimitiveCharacter d) (hx : 1 < x) (hp₁ : 0 < pp.1) (hp₂ : 0 < pp.2) :
    MeasureTheory.Integrable (chen1973Lemma6BromwichVonMangoldtIntegrand x d χ pp) MeasureTheory.volume

    The complete finite von-Mangoldt Bromwich integrand is Bochner integrable.

    source
    theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6ActualPhi_eq_integral_bromwichSum {x d : ℕ} {pp : ℕ × ℕ} (χ : PrimitiveCharacter d) (hx : 1 < x) (hp₁ : 0 < pp.1) (hp₂ : 0 < pp.2) :
    chen1973Lemma6ActualPhi x d χ pp = ∫ (t : ℝ), chen1973Lemma6BromwichVonMangoldtIntegrand x d χ pp t

    chen1973Lemma6ActualPhi is exactly the full real-line integral of its finite von-Mangoldt twisted sum.

    source
    theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimePairShell_pos {x B k m : ℕ} {pp : ℕ × ℕ} (hpp : pp ∈ chen1973Lemma6PrimePairShell x B k m) :
    0 < pp.1 ∧ 0 < pp.2

    Membership in a source prime-pair shell forces both coordinates positive.

    source
    noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6BromwichPrimePairIntegrand (x d B k m : ℕ) (χ : PrimitiveCharacter d) (t : ℝ) :
    ℂ

    The prime-pair sum after moving its finite sum inside the Bromwich integral.

    Equations
    Instances For
      source
      theorem AnalyticNumberTheory.LargeSieve.integrable_chen1973Lemma6BromwichPrimePairIntegrand {x d B k m : ℕ} (χ : PrimitiveCharacter d) (hx : 1 < x) :
      MeasureTheory.Integrable (chen1973Lemma6BromwichPrimePairIntegrand x d B k m χ) MeasureTheory.volume

      Every prime-pair integrand is Bochner integrable.

      source
      theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimePairSum_eq_integral_bromwichSum {x d B k m : ℕ} (χ : PrimitiveCharacter d) (hx : 1 < x) :
      ∑ pp ∈ chen1973Lemma6PrimePairShell x B k m, ↑(Real.log (↑x / (↑pp.1 * ↑pp.2)))⁻¹ * chen1973Lemma6ActualPhi x d χ pp * ↑χ ↑(pp.1 * pp.2) = ∫ (t : ℝ), chen1973Lemma6BromwichPrimePairIntegrand x d B k m χ t

      Exact finite prime-pair/integral exchange.

      source
      noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6BromwichCharacterIntegrand (x d B k m : ℕ) (t : ℝ) :
      ℂ

      The complete primitive-character integrand for one conductor.

      Equations
      Instances For
        source
        theorem AnalyticNumberTheory.LargeSieve.integrable_chen1973Lemma6BromwichCharacterIntegrand {x d B k m : ℕ} (hx : 1 < x) :
        MeasureTheory.Integrable (chen1973Lemma6BromwichCharacterIntegrand x d B k m) MeasureTheory.volume

        The finite primitive-character integrand is Bochner integrable.

        source
        theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6CharacterSum_eq_integral_bromwichSum {x d B k m : ℕ} (hx : 1 < x) :
        ∑ χ : PrimitiveCharacter d, star (↑χ ↑x) * ∑ pp ∈ chen1973Lemma6PrimePairShell x B k m, ↑(Real.log (↑x / (↑pp.1 * ↑pp.2)))⁻¹ * chen1973Lemma6ActualPhi x d χ pp * ↑χ ↑(pp.1 * pp.2) = ∫ (t : ℝ), chen1973Lemma6BromwichCharacterIntegrand x d B k m t

        Exact exchange of the primitive-character sum with the full-line Bromwich integral.

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

        The exact conductor-block expression after all finite sums have been moved inside their full-line Bromwich integrals. The conductor sum and norm remain outside, exactly as in the definition of N_m.

        Equations
        Instances For
          source
          theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6NmBlockActual_eq_bromwich {x L level B k m : ℕ} (hx : 1 < x) :
          chen1973Lemma6NmBlockActual x L level B k m = chen1973Lemma6NmBlockBromwich x L level B k m

          Exact conductor-block lift of the finite Bromwich identity. This is the finite-sum closure needed before any contour deformation toward equation (17), and it has no equation-(17) conclusion premise.