Prove2Me

From cutoff prime-power estimates to the paper covariance row

Proved
Erdos390.Full.PaperPrimePowerPairAggregation.BoundedValuationLaw.paperBand_row_le_of_cutoff_pointwise

by doctosil · Sep 17, 2026 · Mathlib c5ea003 (Lean v4.30.0)

analytic-number-theoryerdos-390erdos390-source-construction

Write L=log⁡nL=\log n, y=n2/9y=n^{2/9}, Y=⌊y⌋Y=\lfloor y\rfloor, U=9/2U=9/2, and vd=U−log⁡d/log⁡yv_d=U-\log d/\log y. Let ρ\rho denote the Dickman function. Let a bounded-valuation law have physical bound MM, with n>1,W>1n>1,W>1. Let Ip=1p∣mI_p=\mathbf1_{p\mid m}, Vp=vp(m)V_p=v_p(m), Ip,r=1pr∣mI_{p,r}=\mathbf1_{p^r\mid m}, tp=log⁡p/log⁡yt_p=\log p/\log y, and Rp={2,…,valuationCutoff(p,M)}R_p=\{2,\ldots,\mathrm{valuationCutoff}(p,M)\}. Suppose A,ϵ≥0A,\epsilon\ge0. For distinct band primes, assume the mixed, reverse-mixed, and double-high covariances are bounded respectively by (Atptq+ϵ)(r+1)/(prq)(At_pt_q+\epsilon)(r+1)/(p^rq), (Atptq+ϵ)(s+1)/(pqs)(At_pt_q+\epsilon)(s+1)/(pq^s), and (Atptq+ϵ)(r+1)(s+1)/(prqs)(At_pt_q+\epsilon)(r+1)(s+1)/(p^rq^s), plus errors epqrJI,epqsIJ,epqrsJJe^{JI}_{pqr},e^{IJ}_{pqs},e^{JJ}_{pqrs}. Assume EIp,r≤(A+ϵ)(r+1)/pr+eprD\mathbb EI_{p,r}\le(A+\epsilon)(r+1)/p^r+e^D_{pr}. Suppose the summed errors obey

p[∑q≠p(∑RpepqrJI+∑RqepqsIJ+∑Rp,RqepqrsJJ)+3∑r∈Rp(2r−3)eprD]≤R.p\left[\sum_{q\ne p}\left(\sum_{R_p}e^{JI}_{pqr}+\sum_{R_q}e^{IJ}_{pqs}+\sum_{R_p,R_q}e^{JJ}_{pqrs}\right)+3\sum_{r\in R_p}(2r-3)e^D_{pr}\right]\le R.

Let HT=∑W<q≤Ytq/qH_T=\sum_{W<q\le Y}t_q/q, H1=∑W<q≤Y1/qH_1=\sum_{W<q\le Y}1/q, and C∗C_* be the fixed pair-aggregation constant.

p∑W<q≤Yq prime∣Cov⁡(Vp,Vq)−Cov⁡(Ip,Iq)∣≤C∗A(HT+5)W+C∗ϵ(H1+5)W+R.p\sum_{W<q\le Y\atop q\ {\rm prime}}|\operatorname{Cov}(V_p,V_q)-\operatorname{Cov}(I_p,I_q)|\le\frac{C_*A(H_T+5)}W+\frac{C_*\epsilon(H_1+5)}W+R.

This is the explicit interface from the four prime-power displays to the full-valuation covariance row.

Preamble
import Mathlib
import Definitions.Def_erdos390_source_bank_interface
import Definitions.Def_erdos390_dickman_step_function
import Theorems.Thm_MediumPNT
import Definitions.Def_erdos390_analytic_foundations_001
import Theorems.Thm_Erdos390_Full_DickmanBasic_kernel_product_bound
import Theorems.Thm_Erdos390_Full_DickmanBasic_rho_pos_on_zero_five
import Theorems.Thm_Erdos390_Full_DickmanBasic_kernel_secondDerivative_first_bound
import Definitions.Def_erdos390_analytic_foundations_002
import Definitions.Def_erdos390_analytic_foundations_004

universe u_1
Formal statement
theorem Erdos390.Full.PaperPrimePowerPairAggregation.BoundedValuationLaw.paperBand_row_le_of_cutoff_pointwise :
∀ {Omega : Type u_1} [inst : Fintype.{u_1} Omega] {M : Nat}
  (law : Erdos390.Full.PrimePowerCovariance.BoundedValuationLaw.{u_1} Omega M) {n W : Nat},
  LT.lt.{0} (1 : Nat) n →
    LT.lt.{0} (1 : Nat) W →
      ∀ (A epsilon remRow : Real) (eJI eIJ : Nat → Nat → Nat → Real) (eJJ : Nat → Nat → Nat → Nat → Real)
        (eD : Nat → Nat → Real),
        LE.le.{0} (0 : Real) A →
          LE.le.{0} (0 : Real) epsilon →
            (∀ (p : Nat),
                Membership.mem.{0, 0} (Erdos390.Full.ArithmeticModel.primeBand n W) p →
                  ∀ (q : Nat),
                    Membership.mem.{0, 0} (Finset.erase.{0} (Erdos390.Full.ArithmeticModel.primeBand n W) p) q →
                      ∀ (r : Nat),
                        Membership.mem.{0, 0}
                            (Erdos390.Full.ArithmeticModel.highExponents
                              (Erdos390.Full.ValuationCutoff.valuationCutoff p M))
                            r →
                          LE.le.{0}
                            (abs.{0}
                              (Erdos390.Full.FiniteProbability.covariance.{u_1}
                                (Erdos390.Full.PrimePowerCovariance.BoundedValuationLaw.probability.{u_1} law)
                                (Erdos390.Full.PrimePowerCovariance.BoundedValuationLaw.Ip.{u_1} law p r)
                                (Erdos390.Full.PrimePowerCovariance.BoundedValuationLaw.I.{u_1} law q)))
                            (HAdd.hAdd.{0, 0, 0}
                              (HMul.hMul.{0, 0, 0}
                                (HAdd.hAdd.{0, 0, 0}
                                  (HMul.hMul.{0, 0, 0}
                                    (HMul.hMul.{0, 0, 0} A (Erdos390.Full.ArithmeticModel.tPrime n p))
                                    (Erdos390.Full.ArithmeticModel.tPrime n q))
                                  epsilon)
                                (HDiv.hDiv.{0, 0, 0} (HAdd.hAdd.{0, 0, 0} ↑r (1 : Real))
                                  (HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} (↑p) r) ↑q)))
                              (eJI p q r))) →
              (∀ (p : Nat),
                  Membership.mem.{0, 0} (Erdos390.Full.ArithmeticModel.primeBand n W) p →
                    ∀ (q : Nat),
                      Membership.mem.{0, 0} (Finset.erase.{0} (Erdos390.Full.ArithmeticModel.primeBand n W) p) q →
                        ∀ (s : Nat),
                          Membership.mem.{0, 0}
                              (Erdos390.Full.ArithmeticModel.highExponents
                                (Erdos390.Full.ValuationCutoff.valuationCutoff q M))
                              s →
                            LE.le.{0}
                              (abs.{0}
                                (Erdos390.Full.FiniteProbability.covariance.{u_1}
                                  (Erdos390.Full.PrimePowerCovariance.BoundedValuationLaw.probability.{u_1} law)
                                  (Erdos390.Full.PrimePowerCovariance.BoundedValuationLaw.I.{u_1} law p)
                                  (Erdos390.Full.PrimePowerCovariance.BoundedValuationLaw.Ip.{u_1} law q s)))
                              (HAdd.hAdd.{0, 0, 0}
                                (HMul.hMul.{0, 0, 0}
                                  (HAdd.hAdd.{0, 0, 0}
                                    (HMul.hMul.{0, 0, 0}
                                      (HMul.hMul.{0, 0, 0} A (Erdos390.Full.ArithmeticModel.tPrime n p))
                                      (Erdos390.Full.ArithmeticModel.tPrime n q))
                                    epsilon)
                                  (HDiv.hDiv.{0, 0, 0} (HAdd.hAdd.{0, 0, 0} ↑s (1 : Real))
                                    (HMul.hMul.{0, 0, 0} (↑p) (HPow.hPow.{0, 0, 0} (↑q) s))))
                                (eIJ p q s))) →
                (∀ (p : Nat),
                    Membership.mem.{0, 0} (Erdos390.Full.ArithmeticModel.primeBand n W) p →
                      ∀ (q : Nat),
                        Membership.mem.{0, 0} (Finset.erase.{0} (Erdos390.Full.ArithmeticModel.primeBand n W) p) q →
                          ∀ (r : Nat),
                            Membership.mem.{0, 0}
                                (Erdos390.Full.ArithmeticModel.highExponents
                                  (Erdos390.Full.ValuationCutoff.valuationCutoff p M))
                                r →
                              ∀ (s : Nat),
                                Membership.mem.{0, 0}
                                    (Erdos390.Full.ArithmeticModel.highExponents
                                      (Erdos390.Full.ValuationCutoff.valuationCutoff q M))
                                    s →
                                  LE.le.{0}
                                    (abs.{0}
                                      (Erdos390.Full.FiniteProbability.covariance.{u_1}
                                        (Erdos390.Full.PrimePowerCovariance.BoundedValuationLaw.probability.{u_1} law)
                                        (Erdos390.Full.PrimePowerCovariance.BoundedValuationLaw.Ip.{u_1} law p r)
                                        (Erdos390.Full.PrimePowerCovariance.BoundedValuationLaw.Ip.{u_1} law q s)))
                                    (HAdd.hAdd.{0, 0, 0}
                                      (HMul.hMul.{0, 0, 0}
                                        (HAdd.hAdd.{0, 0, 0}
                                          (HMul.hMul.{0, 0, 0}
                                            (HMul.hMul.{0, 0, 0} A (Erdos390.Full.ArithmeticModel.tPrime n p))
                                            (Erdos390.Full.ArithmeticModel.tPrime n q))
                                          epsilon)
                                        (HDiv.hDiv.{0, 0, 0}
                                          (HMul.hMul.{0, 0, 0} (HAdd.hAdd.{0, 0, 0} ↑r (1 : Real))
                                            (HAdd.hAdd.{0, 0, 0} ↑s (1 : Real)))
                                          (HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} (↑p) r)
                                            (HPow.hPow.{0, 0, 0} (↑q) s))))
                                      (eJJ p q r s))) →
                  (∀ (p : Nat),
                      Membership.mem.{0, 0} (Erdos390.Full.ArithmeticModel.primeBand n W) p →
                        ∀ (r : Nat),
                          Membership.mem.{0, 0}
                              (Erdos390.Full.ArithmeticModel.highExponents
                                (Erdos390.Full.ValuationCutoff.valuationCutoff p M))
                              r →
                            LE.le.{0}
                              (Erdos390.Full.FiniteProbability.expect.{u_1}
                                (Erdos390.Full.PrimePowerCovariance.BoundedValuationLaw.probability.{u_1} law)
                                (Erdos390.Full.PrimePowerCovariance.BoundedValuationLaw.Ip.{u_1} law p r))
                              (HAdd.hAdd.{0, 0, 0}
                                (HMul.hMul.{0, 0, 0} (HAdd.hAdd.{0, 0, 0} A epsilon)
                                  (HDiv.hDiv.{0, 0, 0} (HAdd.hAdd.{0, 0, 0} ↑r (1 : Real))
                                    (HPow.hPow.{0, 0, 0} (↑p) r)))
                                (eD p r))) →
                    (∀ (p : Nat),
                        Membership.mem.{0, 0} (Erdos390.Full.ArithmeticModel.primeBand n W) p →
                          LE.le.{0}
                            (HMul.hMul.{0, 0, 0} (↑p)
                              (HAdd.hAdd.{0, 0, 0}
                                (∑ q ∈ Finset.erase.{0} (Erdos390.Full.ArithmeticModel.primeBand n W) p,
                                  HAdd.hAdd.{0, 0, 0}
                                    (HAdd.hAdd.{0, 0, 0}
                                      (∑
                                        r ∈
                                          Erdos390.Full.ArithmeticModel.highExponents
                                            (Erdos390.Full.ValuationCutoff.valuationCutoff p M),
                                        eJI p q r)
                                      (∑
                                        s ∈
                                          Erdos390.Full.ArithmeticModel.highExponents
                                            (Erdos390.Full.ValuationCutoff.valuationCutoff q M),
                                        eIJ p q s))
                                    (∑
                                      r ∈
                                        Erdos390.Full.ArithmeticModel.highExponents
                                          (Erdos390.Full.ValuationCutoff.valuationCutoff p M),
                                      ∑
                                        s ∈
                                          Erdos390.Full.ArithmeticModel.highExponents
                                            (Erdos390.Full.ValuationCutoff.valuationCutoff q M),
                                        eJJ p q r s))
                                (HMul.hMul.{0, 0, 0} (3 : Real)
                                  (∑
                                    r ∈
                                      Erdos390.Full.ArithmeticModel.highExponents
                                        (Erdos390.Full.ValuationCutoff.valuationCutoff p M),
                                    HMul.hMul.{0, 0, 0}
                                      (↑(HSub.hSub.{0, 0, 0} (HMul.hMul.{0, 0, 0} (2 : Nat) r) (3 : Nat))) (eD p r)))))
                            remRow) →
                      ∀ (p : Nat),
                        Membership.mem.{0, 0} (Erdos390.Full.ArithmeticModel.primeBand n W) p →
                          LE.le.{0}
                            (HMul.hMul.{0, 0, 0} (↑p)
                              (∑ q ∈ Erdos390.Full.ArithmeticModel.primeBand n W,
                                abs.{0}
                                  (HSub.hSub.{0, 0, 0}
                                    (Erdos390.Full.PrimePowerCovariance.BoundedValuationLaw.covVV.{u_1} law p q)
                                    (Erdos390.Full.PrimePowerCovariance.BoundedValuationLaw.covII.{u_1} law p q))))
                            (HAdd.hAdd.{0, 0, 0}
                              (HAdd.hAdd.{0, 0, 0}
                                (HMul.hMul.{0, 0, 0}
                                  (HMul.hMul.{0, 0, 0}
                                    (HMul.hMul.{0, 0, 0}
                                      Erdos390.Full.PaperPrimePowerPairAggregation.pairAggregationConstant A)
                                    (HAdd.hAdd.{0, 0, 0} (Erdos390.Full.PrimeSums.bandTReciprocalSum n W) (5 : Real)))
                                  (HDiv.hDiv.{0, 0, 0} (1 : Real) ↑W))
                                (HMul.hMul.{0, 0, 0}
                                  (HMul.hMul.{0, 0, 0}
                                    (HMul.hMul.{0, 0, 0}
                                      Erdos390.Full.PaperPrimePowerPairAggregation.pairAggregationConstant epsilon)
                                    (HAdd.hAdd.{0, 0, 0} (Erdos390.Full.PrimeSums.bandReciprocalSum n W) (5 : Real)))
                                  (HDiv.hDiv.{0, 0, 0} (1 : Real) ↑W)))
                              remRow) := by sorry
Source
https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/lean/Erdos390/Full/PaperPrimePowerPairAggregation.lean#L292-L469

View graph