Prove2Me

Reference marked-row estimate from coefficient ledgers

Proved
Erdos390.Full.PaperBridgeFit.BridgeData.referenceMarkedRow_le

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

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

Write Ln=log⁡nL_n=\log n, yn=n2/9y_n=n^{2/9}, Yn=⌊yn⌋Y_n=\lfloor y_n\rfloor, and Pn,W={p prime:W<p≤Yn}\mathcal P_{n,W}=\{p\text{ prime}:W<p\le Y_n\}. Let BB be a bridge with finite head and band sets, and write tp=log⁡p/log⁡ynt_p=\log p/\log y_n, hih_i for harmonic band masses, αi\alpha_i for band centers, and j(p)j(p) for the band of pp. Let RprR_{pr} be its squarefree Poisson–Dickman reference entry, Ip=1p∣mI_p=\mathbf1_{p\mid m}, and μξ\mu_\xi its tilted law. For a raw band-gauge vector qq, let ara_r be its actual compensated prime coefficients. Suppose CF,CK≥0C_F,C_K\ge0, ∣ar∣≤Csup⁡w|a_r|\le C_{\sup}w, ∑r∣ar∣/r≤C1w\sum_r|a_r|/r\le C_1w, ∣F(tr)∣≤CF|F(t_r)|\le C_F, and ∣K(tr,ts)∣≤CK|K(t_r,t_s)|\le C_K for all band primes, where FF and KK are the Dickman diagonal function and covariance kernel. Then

∣∑rarRpr∣≤(CKC1+CFCsup⁡)wp(p∈Pn,W).\left|\sum_r a_rR_{pr}\right|\le(C_KC_1+C_FC_{\sup})\frac w p\qquad(p\in\mathcal P_{n,W}).

The same coefficient ledgers that describe a compensated vector control its reference marked 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_003
import Definitions.Def_erdos390_analytic_foundations_004
import Definitions.Def_erdos390_analytic_foundations_005

universe u_1 u_2
Formal statement
theorem Erdos390.Full.PaperBridgeFit.BridgeData.referenceMarkedRow_le :
∀ {Head : Type u_1} {Band : Type u_2} [inst : Fintype.{u_1} Head] [inst_1 : DecidableEq.{u_1 + 1} Head]
  [inst_2 : Fintype.{u_2} Band] [inst_3 : DecidableEq.{u_2 + 1} Band]
  (B : Erdos390.Full.PaperBridgeFit.BridgeData.{u_1, u_2} Head Band)
  (q : ↥(Erdos390.Full.PaperBridgeFit.BridgeData.RawBandGauge.{u_1, u_2} B)) {CF CKernel Csup CL1 w : Real},
  LE.le.{0} (0 : Real) CF →
    LE.le.{0} (0 : Real) CKernel →
      (∀ (r : Nat),
          Membership.mem.{0, 0}
              (Erdos390.Full.ArithmeticModel.primeBand
                (Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{u_1}
                  (Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{u_1, u_2} B))
                (Erdos390.Full.PaperBridgeFit.StructuredSampleData.W.{u_1}
                  (Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{u_1, u_2} B)))
              r →
            LE.le.{0}
              (abs.{0} (Erdos390.Full.PaperBridgeFit.BridgeData.actualCompensatedNatCoefficient.{u_1, u_2} B q r))
              (HMul.hMul.{0, 0, 0} Csup w)) →
        LE.le.{0}
            (∑
              r ∈
                Erdos390.Full.ArithmeticModel.primeBand
                  (Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{u_1}
                    (Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{u_1, u_2} B))
                  (Erdos390.Full.PaperBridgeFit.StructuredSampleData.W.{u_1}
                    (Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{u_1, u_2} B)),
              HMul.hMul.{0, 0, 0}
                (abs.{0} (Erdos390.Full.PaperBridgeFit.BridgeData.actualCompensatedNatCoefficient.{u_1, u_2} B q r))
                (HDiv.hDiv.{0, 0, 0} (1 : Real) ↑r))
            (HMul.hMul.{0, 0, 0} CL1 w) →
          (∀
              (r :
                Erdos390.Full.ArithmeticBandGeometry.BandPrime
                  (Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{u_1}
                    (Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{u_1, u_2} B))
                  (Erdos390.Full.PaperBridgeFit.StructuredSampleData.W.{u_1}
                    (Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{u_1, u_2} B))),
              LE.le.{0}
                (abs.{0}
                  (Erdos390.Full.DickmanBasic.F
                    (Erdos390.Full.ArithmeticModel.tPrime
                      (Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{u_1}
                        (Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{u_1, u_2} B))
                      ↑r)))
                CF) →
            (∀
                (r s :
                  Erdos390.Full.ArithmeticBandGeometry.BandPrime
                    (Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{u_1}
                      (Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{u_1, u_2} B))
                    (Erdos390.Full.PaperBridgeFit.StructuredSampleData.W.{u_1}
                      (Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{u_1, u_2} B))),
                LE.le.{0}
                  (abs.{0}
                    (Erdos390.Full.ConditionedPoissonLimit.covarianceKernel
                      (Erdos390.Full.ArithmeticModel.tPrime
                        (Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{u_1}
                          (Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{u_1, u_2} B))
                        ↑r)
                      (Erdos390.Full.ArithmeticModel.tPrime
                        (Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{u_1}
                          (Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{u_1, u_2} B))
                        ↑s)))
                  CKernel) →
              ∀ {p : Nat},
                Membership.mem.{0, 0}
                    (Erdos390.Full.ArithmeticModel.primeBand
                      (Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{u_1}
                        (Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{u_1, u_2} B))
                      (Erdos390.Full.PaperBridgeFit.StructuredSampleData.W.{u_1}
                        (Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{u_1, u_2} B)))
                    p →
                  LE.le.{0}
                    (abs.{0}
                      (∑
                        r ∈
                          Erdos390.Full.ArithmeticModel.primeBand
                            (Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{u_1}
                              (Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{u_1, u_2} B))
                            (Erdos390.Full.PaperBridgeFit.StructuredSampleData.W.{u_1}
                              (Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{u_1, u_2} B)),
                        HMul.hMul.{0, 0, 0}
                          (Erdos390.Full.PaperBridgeFit.BridgeData.actualCompensatedNatCoefficient.{u_1, u_2} B q r)
                          (Erdos390.Full.SquarefreeCovarianceReference.squarefreeReferenceEntry
                            (Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{u_1}
                              (Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{u_1, u_2} B))
                            p r)))
                    (HMul.hMul.{0, 0, 0}
                      (HMul.hMul.{0, 0, 0}
                        (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} CKernel CL1) (HMul.hMul.{0, 0, 0} CF Csup)) w)
                      (HDiv.hDiv.{0, 0, 0} (1 : Real) ↑p)) := by sorry
Source
https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/lean/Erdos390/Full/PaperActualSquarefreeMarkedRow.lean#L165-L298

View graph