Documentation

MathlibNt.SieveTheory.Liu.LogarithmicIntegral.LiuTrueLiPanSigned

Source-faithful signed Pan assembly for arbitrary distribution mains #

This is the finite Vaughan/Chebyshev decomposition used by the Liu eqn-r lane, with the distribution main left as an explicit parameter. In particular, the genuine logarithmic integral is never identified with ANT's historical x / log x compatibility function.

Exact signed kernels #

source
noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanSignedMainKernel (distMain : ℝ → ℝ) (y a q l u v : ℕ) :
ℝ

The exact source-faithful signed residual after the aggregate Type I and Type II kernels have been removed.

Equations
Instances For
    source
    noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanSignedCorrectionKernel (y a q l : ℕ) :
    ℝ

    The prime-power correction in the exact ψ / log to π conversion.

    Equations
    Instances For
      source
      noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanSignedMainSum (distMain : ℝ → ℝ) (y X q l : ℕ) (f : ℕ → ℝ) (u v : ℕ) :
      ℝ

      Coprime signed main residual. The coprimality condition is deliberately displayed here rather than hidden in the kernel.

      Equations
      Instances For
        source
        noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanSignedCorrectionSum (y X q l : ℕ) (f : ℕ → ℝ) :
        ℝ

        Coprime signed prime-power correction.

        Equations
        Instances For
          source
          noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanSignedCorrectionBound (y X q l : ℕ) (f : ℕ → ℝ) :
          ℝ

          Nonnegative termwise majorant for the prime-power correction.

          Equations
          Instances For
            source
            theorem MathlibNt.SieveTheory.LiuWeight.liuPanSignedCorrectionBound_nonneg (y X q l : ℕ) (f : ℕ → ℝ) :
            0 ≤ liuPanSignedCorrectionBound y X q l f
            source
            theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanCoprimeSum_eq_sourceFaithfulSigned (distMain : ℝ → ℝ) (y X q l : ℕ) (f : ℕ → ℝ) (u v : ℕ) (hf0 : f 0 = 0) :
            liuMainPanCoprimeSum distMain y X q l f = ((AnalyticNumberTheory.Sieve.panPieceSum y X q l f fun (y q l : ℕ) => AnalyticNumberTheory.Sieve.apV1 y q l u / Real.log ↑y) + AnalyticNumberTheory.Sieve.panPieceSum y X q l f fun (y q l : ℕ) => AnalyticNumberTheory.Sieve.apV3 y q l u v / Real.log ↑y) + liuPanSignedMainSum distMain y X q l f u v - liuPanSignedCorrectionSum y X q l f

            Exact finite identity for the arbitrary-main coprime Pan sum. It is constructed from the live Vaughan and Chebyshev identities, not an assumed pointwise split.

            source
            theorem MathlibNt.SieveTheory.LiuWeight.abs_liuPanSignedCorrectionSum_le (y X q l : ℕ) (f : ℕ → ℝ) :
            |liuPanSignedCorrectionSum y X q l f| ≤ liuPanSignedCorrectionBound y X q l f
            source
            theorem MathlibNt.SieveTheory.LiuWeight.abs_liuMainPanCoprimeSum_le_sourceFaithfulSigned (distMain : ℝ → ℝ) (y X q l : ℕ) (f : ℕ → ℝ) (u v : ℕ) (hf0 : f 0 = 0) :
            |liuMainPanCoprimeSum distMain y X q l f| ≤ |AnalyticNumberTheory.Sieve.panPieceSum y X q l f fun (y q l : ℕ) => AnalyticNumberTheory.Sieve.apV1 y q l u / Real.log ↑y| + |AnalyticNumberTheory.Sieve.panPieceSum y X q l f fun (y q l : ℕ) => AnalyticNumberTheory.Sieve.apV3 y q l u v / Real.log ↑y| + (|liuPanSignedMainSum distMain y X q l f u v| + liuPanSignedCorrectionBound y X q l f)

            Pointwise absolute-value form of the exact arbitrary-main decomposition.

            Canonical residue and source-parameter maxima #

            source
            noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanSignedResidualMaxY (distMain : ℝ → ℝ) (X q x : ℕ) (f : ℕ → ℝ) (u v : ℕ) :
            ℝ

            The double maximum of the concrete signed residual and its separate prime-power correction. For q = 1, its canonical residue is 0.

            Equations
            Instances For
              source
              theorem MathlibNt.SieveTheory.LiuWeight.liuPanSignedResidualMaxY_one (distMain : ℝ → ℝ) (X x : ℕ) (f : ℕ → ℝ) (u v : ℕ) :
              liuPanSignedResidualMaxY distMain X 1 x f u v = (Finset.image (fun (y : ℕ) => |liuPanSignedMainSum distMain y X 1 0 f u v| + liuPanSignedCorrectionBound y X 1 0 f) (Finset.range (x + 1))).max' ⋯
              source
              theorem MathlibNt.SieveTheory.LiuWeight.liuPanSignedResidualMaxY_nonneg (distMain : ℝ → ℝ) (X q x : ℕ) (f : ℕ → ℝ) (u v : ℕ) :
              0 ≤ liuPanSignedResidualMaxY distMain X q x f u v
              source
              theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanMaxY_le_sourceFaithfulSigned (distMain : ℝ → ℝ) (X q x : ℕ) (f : ℕ → ℝ) (u v : ℕ) (hf0 : f 0 = 0) :
              liuMainPanMaxY distMain X q x f ≤ ((AnalyticNumberTheory.Sieve.panPieceMaxY X q x f fun (y q l : ℕ) => AnalyticNumberTheory.Sieve.apV1 y q l u / Real.log ↑y) + AnalyticNumberTheory.Sieve.panPieceMaxY X q x f fun (y q l : ℕ) => AnalyticNumberTheory.Sieve.apV3 y q l u v / Real.log ↑y) + liuPanSignedResidualMaxY distMain X q x f u v

              Maximal pointwise signed decomposition for the arbitrary distribution main.

              Uniform source-faithful assembly #

              source
              def MathlibNt.SieveTheory.LiuWeight.LiuMainPanSourceFaithfulSignedMainBound (distMain : ℝ → ℝ) (x f : ℕ → ℝ) (u v : ℕ) :
              Prop

              The exact inverse-log weighted bound for the concrete arbitrary-main signed residual.

              Equations
              Instances For
                source
                def MathlibNt.SieveTheory.LiuWeight.LiuMainPanMeanValueUniform (distMain : ℝ → ℝ) (x f : ℕ → ℝ) :
                Prop

                The main-parametric analogue of ANT's global Pan mean-value predicate.

                Equations
                Instances For
                  source
                  theorem MathlibNt.SieveTheory.LiuWeight.LiuMainPanMeanValueUniform.of_sourceFaithfulSignedInputs {distMain : ℝ → ℝ} {x f : ℕ → ℝ} {u v : ℕ} (hI : AnalyticNumberTheory.Sieve.PanTypeICharacterMeanValue x f u) (hII : AnalyticNumberTheory.Sieve.PanTypeIICharacterMeanValue x f u v) (hM : LiuMainPanSourceFaithfulSignedMainBound distMain x f u v) (hfin : AnalyticNumberTheory.Sieve.PanLogEventuallyLarge x) (hf0 : f 0 = 0) :
                  LiuMainPanMeanValueUniform distMain x f

                  Fixed-source transparent inputs and the Liu endpoint #

                  source
                  def MathlibNt.SieveTheory.LiuWeight.LiuMainPanTypeIPieceBoundAt (N : ℕ) (f : ℕ → ℝ) (A B C : ℝ) (u : ℕ) :
                  Prop

                  Exact weighted Type I finite input at the source parameter N.

                  Equations
                  Instances For
                    source
                    def MathlibNt.SieveTheory.LiuWeight.LiuMainPanTypeIIPieceBoundAt (N : ℕ) (f : ℕ → ℝ) (A B C : ℝ) (u v : ℕ) :
                    Prop

                    Exact weighted Type II finite input at the source parameter N.

                    Equations
                    Instances For
                      source
                      def MathlibNt.SieveTheory.LiuWeight.LiuMainPanSignedResidualBoundAt (distMain : ℝ → ℝ) (N : ℕ) (f : ℕ → ℝ) (A B C : ℝ) (u v : ℕ) :
                      Prop

                      Exact weighted finite input for the concrete signed main and prime-power residual at the source parameter N.

                      Equations
                      Instances For
                        source
                        theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanMeanValueAt_of_concreteSignedInputs (distMain : ℝ → ℝ) (N : ℕ) (f : ℕ → ℝ) (A B C1 C2 C3 : ℝ) (u v : ℕ) (hf0 : f 0 = 0) (hI : LiuMainPanTypeIPieceBoundAt N f A B C1 u) (hII : LiuMainPanTypeIIPieceBoundAt N f A B C2 u v) (hM : LiuMainPanSignedResidualBoundAt distMain N f A B C3 u v) :
                        LiuMainPanMeanValueAt distMain N f A B (C1 + C2 + C3)

                        The three explicit source-faithful finite inputs produce the fixed-N main-parametric Pan inequality. This does not take a LiuMainPanMeanValueAt witness as an assumption.

                        source
                        def MathlibNt.SieveTheory.LiuWeight.LiuMainPanSourceFamilyInputs (distMain : ℝ → ℝ) (A B C1 C2 C3 : ℝ) (u v : ℕ) :
                        Prop

                        An eventual family of explicit Type I, Type II, and concrete signed residual inputs for Liu's source-varying weight.

                        Equations
                        Instances For
                          source
                          theorem MathlibNt.SieveTheory.LiuWeight.eventually_liuPaperQSourceFullDistributionMajorant_liuLogarithmicIntegral_le_of_sourceFaithfulSignedInputs (κ ε A B C1 C2 C3 : ℝ) (u v : ℕ) (hε : 0 < ε) (hB : 0 ≤ B) (hsource : LiuMainPanSourceFamilyInputs (liuLogarithmicIntegral κ) A B C1 C2 C3 u v) :
                          ∀ᶠ (N : ℕ) in Filter.atTop, liuPaperQSourceFullDistributionMajorant (liuLogarithmicIntegral κ) N ε ≤ (C1 + C2 + C3) * ↑N / Real.log ↑N ^ A + 15 * liuLogarithmicIntegralUpperConstant κ * liuSourceR1P₂ReciprocalBound * paperQStyleDivisorWeightLogConstant * ↑N ^ (9 / 10) * Real.log ↑N ^ 2