Cutoff-before-mesh reference sharp inverse
ProvedErdos390.Full.PaperBridgeFit.BridgeData.exists_cutoff_before_mesh_eventually_referenceSharp_primeGraph_inverseanalytic-number-theoryerdos-390erdos390-source-construction
Write , , , and . There exist a mesh tolerance , an inverse constant , and a cutoff . For every , every finite head set, and every regular relative mesh with and , choose a nonempty set of positive cells with lower endpoints greater than , upper endpoints at most , and half their total width at least . For all sufficiently large , every bridge with sample size , cutoff , and the canonical partition of this mesh has an interval certificate and an invertible projected arithmetic reference sharp operator on its sharp gauge space satisfying
The cutoff and inverse constant precede the mesh quantifiers, so the bound is independent of the number of cells and the moving low-band center.
Preamble
import Definitions.Def_erdos390_remaining_analytic_propositions_001 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
Formal statement
theorem Erdos390.Full.PaperBridgeFit.BridgeData.exists_cutoff_before_mesh_eventually_referenceSharp_primeGraph_inverse : Erdos390.RemainingAnalyticGoal001_013.{u_1} := by sorry
Source