Canonical guard-deleted valuation-prefix covariance rate
ProvedErdos390.Full.PaperCanonicalTiltedPrefixRows.PaperBridgeFit.BridgeData.exists_uniform_canonical_cellMediumLaw_tilted_valuation_prefix_rate_unrestrictedWrite , , , and . Fix a finite nonempty head index set, patterns , physical intervals , guard constants and a ledger at each . Fix with all head primes at most , and . Consider any finite band set and bridge with sample size , cutoff , separated physical intervals, and nonempty cells after deleting the ledger guards; require its sample data to equal the canonical sample data for these choices. Let be any parameter whose effective prime coefficients have absolute value at most , and let be its medium law on cell . There exist a nonnegative sequence and a threshold independent of the later bridge and parameter, with , such that eventually, for every band prime , cell , and integer ,
This is the canonical all-prefix estimate after guard deletion, uniform over subsequent bridge choices.
import Definitions.Def_erdos390_remaining_analytic_propositions_004 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_2
theorem Erdos390.Full.PaperCanonicalTiltedPrefixRows.PaperBridgeFit.BridgeData.exists_uniform_canonical_cellMediumLaw_tilted_valuation_prefix_rate_unrestricted : Erdos390.RemainingAnalyticGoal004_003.{u_1, u_2} := by sorry