Ordinary inverse for the canonical endpoint arithmetic operator
ProvedErdos390.Full.RegularMeshPrimeCutoffs.Mesh.exists_fineMesh_cutoff_eventually_canonical_ordinaryProjectedRaw_inverse_compactanalytic-number-theoryerdos-390erdos390-source-construction
There exist Cref>0, meshTol>0 and W₀ such that for W≥W₀ and any relative mesh M with δ>0 and δ+M.ratio≤meshTol, eventually n>1 and scale separation hold. For the canonical prime partition P and its endpoint certificate, let T be the projected raw map formed from the endpoint arithmetic diagonal and kernel, with weights P.mass and centers P.center. Every q in its raw gauge satisfies the bound below. The constants are chosen before the mesh, and the norm is the ordinary supremum norm.
Preamble
import Definitions.Def_erdos390_analytic_compact_goals_006
Formal statement
theorem Erdos390.Full.RegularMeshPrimeCutoffs.Mesh.exists_fineMesh_cutoff_eventually_canonical_ordinaryProjectedRaw_inverse_compact : Erdos390.AnalyticCompactBatch006Goal001 := by sorry
Source