Uniform signed profiles for the full actual bridge component laws
ProvedErdos390.Full.PaperBridgeFit.BridgeData.exists_boxIndependent_actual_component_signed_profilesFor a divisor , let denote the common paper divisibility main term; write and . Fix a nonempty finite head set with patterns , two fixed physical intervals , a common upper bound , and guard ledgers with fixed promotion and bank parameters. Fix containing all head primes and a nonnegative effective prime-coefficient bound . Assume each lower interval endpoint is at least one and every upper endpoint is at most . Fix also a nonnegative bound on the physical parameter. There exist a nonnegative sequence and , independent of the later choice of band index set and bridge data, such that and . For any such bridge at whose head patterns, physical endpoints, guard set, and cutoff are exactly the prescribed ones, and whose effective prime coefficients are bounded by , all component laws satisfy
for distinct moving-band primes . Here is the full actual component valuation law, and the bridge parameter must also satisfy . Thus the common profile includes the valuation tilt, guard deletion, and physical tilt, while retaining the rate needed for sharp rows. The moving prime band is .
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_004 import Definitions.Def_erdos390_analytic_foundations_005 universe u_1 u_3
theorem Erdos390.Full.PaperBridgeFit.BridgeData.exists_boxIndependent_actual_component_signed_profiles : Erdos390.RemainingAnalyticGoal001_010.{u_1, u_3} := by sorry