Documentation

MathlibNt.SieveTheory.Liu.Weights.LiuWeightROuter

Liu's eqn-r distribution majorant #

This module formalizes the finite distribution majorant displayed in Liu (2022), eqn-r, for an arbitrary main-term model. The source expression is a sum of termwise absolute inner errors, not the absolute value of a signed outer sum. The coprime estimate remains an explicit analytic proposition; the non-coprime endpoint is supplied by the genuine logarithmic-integral development.

No Selberg remainder R, Pan Type I/II estimate, or signed-main-term estimate is asserted here.

Main-parametric inner sums #

source
noncomputable def MathlibNt.SieveTheory.LiuWeight.liuMainFullSum (main : ℝ → ℝ) (Y X d l : ℕ) (f : ℕ → ℝ) :
ℝ

The unrestricted finite inner distribution sum for an arbitrary main-term model.

Equations
Instances For
    source
    noncomputable def MathlibNt.SieveTheory.LiuWeight.liuMainCoprimeSum (main : ℝ → ℝ) (Y X d l : ℕ) (f : ℕ → ℝ) :
    ℝ

    The coprime finite inner distribution sum for an arbitrary main-term model.

    Equations
    Instances For
      source
      theorem MathlibNt.SieveTheory.LiuWeight.liuMainFullSum_eq_coprime_add_noncoprime (main : ℝ → ℝ) (Y X d l : ℕ) (f : ℕ → ℝ) :
      liuMainFullSum main Y X d l f = liuMainCoprimeSum main Y X d l f + liuMainNoncoprimeSum main Y X d l f

      Exact finite partition of the unrestricted sum into its coprime and non-coprime parts.

      source
      theorem MathlibNt.SieveTheory.LiuWeight.liuMainFullSum_proxy (Y X d l : ℕ) (f : ℕ → ℝ) :
      liuMainFullSum AnalyticNumberTheory.Sieve.logarithmicIntegral Y X d l f = AnalyticNumberTheory.Sieve.panDistributionFullSum Y X d l f

      Proxy compatibility. The unrestricted main-parametric sum specializes to ANT's historical x / log x Pan object. This is not a true-li claim.

      source
      theorem MathlibNt.SieveTheory.LiuWeight.liuMainCoprimeSum_proxy (Y X d l : ℕ) (f : ℕ → ℝ) :
      liuMainCoprimeSum AnalyticNumberTheory.Sieve.logarithmicIntegral Y X d l f = AnalyticNumberTheory.Sieve.panDistributionSum Y X d l f

      Proxy compatibility. The coprime main-parametric sum specializes to ANT's historical x / log x Pan object. This is not a true-li claim.

      Neutral signed weighted sums #

      source
      noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPaperQSourceFullSignedWeightedSum (main : ℝ → ℝ) (N : ℕ) (ε : ℝ) :
      ℝ

      The full signed weighted sum with the auxiliary cutoff D₂. It is a finite algebraic object and is not Liu's Selberg remainder R.

      Equations
      Instances For
        source
        noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPaperQSourceCoprimeSignedWeightedSum (main : ℝ → ℝ) (N : ℕ) (ε : ℝ) :
        ℝ

        The coprime signed weighted sum with the auxiliary cutoff D₂.

        Equations
        Instances For
          source
          noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPaperQSourceNoncoprimeSignedWeightedSum (main : ℝ → ℝ) (N : ℕ) (ε : ℝ) :
          ℝ

          The non-coprime signed weighted sum with the auxiliary cutoff D₂.

          Equations
          Instances For
            source
            theorem MathlibNt.SieveTheory.LiuWeight.liuPaperQSourceFullSignedWeightedSum_eq_coprime_add_noncoprime (main : ℝ → ℝ) (N : ℕ) (ε : ℝ) :
            liuPaperQSourceFullSignedWeightedSum main N ε = liuPaperQSourceCoprimeSignedWeightedSum main N ε + liuPaperQSourceNoncoprimeSignedWeightedSum main N ε

            Exact partition of the neutral signed weighted sum.

            source
            theorem MathlibNt.SieveTheory.LiuWeight.abs_liuPaperQSourceNoncoprimeSignedWeightedSum_le_majorant (main : ℝ → ℝ) (N : ℕ) (ε : ℝ) :
            |liuPaperQSourceNoncoprimeSignedWeightedSum main N ε| ≤ liuPaperQSourceR1Majorant main N ε

            The neutral non-coprime signed weighted sum is bounded by the existing termwise R₁ majorant.

            The source eqn-r absolute majorants #

            source
            noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSourceDEpsilon (N : ℕ) (ε : ℝ) :
            ℕ

            Liu's source divisor cutoff ⌊N^(1/2-ε)⌋ from eqn-r.

            Equations
            Instances For
              source
              theorem MathlibNt.SieveTheory.LiuWeight.liuSourceDEpsilon_le_liuSourceD2 (N : ℕ) (ε : ℝ) (hN : 1 ≤ N) (hε : 0 ≤ ε) :
              liuSourceDEpsilon N ε ≤ liuSourceD2 N

              For nonnegative ε, the source cutoff Dε is no larger than the auxiliary cutoff D₂ = ⌊N^(1/2)⌋.

              source
              noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPaperQSourceFullDistributionMajorant (main : ℝ → ℝ) (N : ℕ) (ε : ℝ) :
              ℝ

              The exact full distribution majorant on the left side of Liu's eqn-r: the weight 3^ω(d) multiplies the absolute value of each inner full error.

              Equations
              Instances For
                source
                noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPaperQSourceCoprimeDistributionMajorant (main : ℝ → ℝ) (N : ℕ) (ε : ℝ) :
                ℝ

                The corresponding termwise absolute coprime distribution majorant.

                Equations
                Instances For
                  source
                  theorem MathlibNt.SieveTheory.LiuWeight.liuPaperQSourceFullDistributionMajorant_le_coprime_add_r1 (main : ℝ → ℝ) (N : ℕ) (ε : ℝ) (hN : 1 ≤ N) (hε : 0 ≤ ε) :
                  liuPaperQSourceFullDistributionMajorant main N ε ≤ liuPaperQSourceCoprimeDistributionMajorant main N ε + liuPaperQSourceR1Majorant main N ε

                  Termwise triangle inequality followed by the nonnegative extension from Dε to D₂ bounds the exact full eqn-r distribution majorant by its coprime part and the established non-coprime majorant.

                  Conditional coprime input and genuine-integral endpoint #

                  source
                  def MathlibNt.SieveTheory.LiuWeight.LiuPaperQCoprimeRBound (main : ℝ → ℝ) (N : ℕ) (ε A C : ℝ) :
                  Prop

                  The remaining coprime Pan estimate for Liu's exact eqn-r absolute majorant. This proposition transparently contains the inverse-log inequality used by the outer bound.

                  Equations
                  Instances For
                    source
                    theorem MathlibNt.SieveTheory.LiuWeight.liuPaperQSourceFullDistributionMajorant_liuLogarithmicIntegral_le (κ : ℝ) (N : ℕ) (ε A Cpan : ℝ) (hN : 8 ≤ N) (hε : 0 ≤ ε) (hpan : LiuPaperQCoprimeRBound (liuLogarithmicIntegral κ) N ε A Cpan) :
                    liuPaperQSourceFullDistributionMajorant (liuLogarithmicIntegral κ) N ε ≤ Cpan * ↑N / Real.log ↑N ^ A + 15 * liuLogarithmicIntegralUpperConstant κ * liuSourceR1P₂ReciprocalBound * paperQStyleDivisorWeightLogConstant * ↑N ^ (9 / 10) * Real.log ↑N ^ 2

                    Liu's exact eqn-r distribution majorant for the genuine normalized logarithmic integral, conditional only on the explicitly retained coprime inverse-log estimate. The N^(9/10) log(N)^2 term is not absorbed.