Canonical guard-deleted valuation-prefix covariance rate
ProvedErdos390.Full.PaperCanonicalTiltedPrefixRows.PaperBridgeFit.BridgeData.exists_uniform_canonical_cellMediumLaw_tilted_valuation_prefix_rate_unrestricted_compactWrite , , , 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 universe u_1 u_2
theorem Erdos390.Full.PaperCanonicalTiltedPrefixRows.PaperBridgeFit.BridgeData.exists_uniform_canonical_cellMediumLaw_tilted_valuation_prefix_rate_unrestricted_compact : Erdos390.RemainingAnalyticGoal004_003.{u_1, u_2} := by sorry