The fast gauge of a Schur solution satisfies the projected band equation

Proved

Erdos390.Full.PaperBridgeFit.BridgeData.actualBandSchur_fastGauge_eq_projectedTarget

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

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

Let $B$ be bridge data with nonempty finite head and band index sets, $\xi$ a parameter, and $\gamma>0$ such that the nuisance covariance operator satisfies $\langle z,N_\xi z\rangle\ge\gamma\|z\|^2$ . Let $e$ be a linear automorphism of the raw band gauge equal to the actual band Schur map. For a band target $\Delta$ , suppose a main vector $u$ solves the exact Schur equation $S_\xi u=\operatorname{main}(\operatorname{normalizedTarget}(\Delta))$ . If $q_f$ is the fast gauge obtained from $u$ using the actual band regression, then

e(q_f)=\operatorname{projectedNormalizedTargetBand}(\Delta).

This is an exact identification of the fast equation, before any inverse norm bound is applied.

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.actualBandSchur_fastGauge_eq_projectedTarget :
∀ {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) [inst_4 : Nonempty.{u_1 + 1} Head]
  [inst_5 : Nonempty.{u_2 + 1} Band] (xi : Erdos390.Full.PaperBridgeFit.BridgeData.ParamSpace.{u_1, u_2} B)
  {gamma : Real} (hgamma : LT.lt.{0} (0 : Real) gamma)
  (hgap :
    ∀ (z : Erdos390.Full.PaperBridgeFit.BridgeData.NuisanceSpace.{u_1, u_2} B),
      LE.le.{0} (HMul.hMul.{0, 0, 0} gamma (HPow.hPow.{0, 0, 0} (Norm.norm.{u_1} z) (2 : Nat)))
        (Inner.inner.{0, u_1} Real z
          ((Erdos390.Full.PaperBridgeFit.BridgeData.nuisanceCovarianceOperator.{u_1, u_2} B xi) z)))
  (e :
    LinearEquiv.{0, 0, u_2, u_2} (RingHom.id.{0} Real)
      ↥(Erdos390.Full.PaperBridgeFit.BridgeData.RawBandGauge.{u_1, u_2} B)
      ↥(Erdos390.Full.PaperBridgeFit.BridgeData.RawBandGauge.{u_1, u_2} B)),
  (∀ (q : ↥(Erdos390.Full.PaperBridgeFit.BridgeData.RawBandGauge.{u_1, u_2} B)),
      Eq.{u_2 + 1} (e q)
        ((Erdos390.Full.PaperBridgeFit.BridgeData.actualBandSchurLinearMap.{u_1, u_2} B xi hgamma hgap) q)) →
    ∀ (Delta : Band → Real) (u : Erdos390.Full.PaperBridgeFit.BridgeData.MainSpace.{u_1, u_2} B),
      Eq.{u_2 + 1}
          ((Erdos390.Full.PaperBridgeFit.BridgeData.exactSchurCovarianceOperator.{u_1, u_2} B xi hgamma hgap) u)
          (Erdos390.Full.PaperBridgeFit.BridgeData.mainPart.{u_1, u_2} B
            (Erdos390.Full.PaperBridgeFit.BridgeData.normalizedTarget.{u_1, u_2} B Delta)) →
        Eq.{u_2 + 1}
          ((Erdos390.Full.PaperBridgeFit.BridgeData.actualBandSchurLinearMap.{u_1, u_2} B xi hgamma hgap)
            (Erdos390.Full.PaperBridgeFit.BridgeData.fastGaugeOfMain.{u_1, u_2} B xi hgamma hgap e u))
          (Erdos390.Full.PaperBridgeFit.BridgeData.projectedNormalizedTargetBand.{u_1, u_2} B Delta) := by sorry

Source

https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/lean/Erdos390/Full/PaperExactTwoStageTargetSolve.lean#L284-L389

View graph