Canonical valuation mean bound and pairwise agreement rate
ProvedErdos390.Full.PaperCanonicalTiltedValuationMeanRows.PaperBridgeFit.BridgeData.exists_uniform_canonical_cellMediumLaw_valuation_mean_profiles_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 common threshold with , such that eventually, for every band prime and cells ,
A single reciprocal first-moment constant and a vanishing mean-agreement rate work for every later bridge and admissible parameter.
import Definitions.Def_erdos390_remaining_analytic_propositions_004 universe u_1 u_2
theorem Erdos390.Full.PaperCanonicalTiltedValuationMeanRows.PaperBridgeFit.BridgeData.exists_uniform_canonical_cellMediumLaw_valuation_mean_profiles_rate_unrestricted_compact : Erdos390.RemainingAnalyticGoal004_004.{u_1, u_2} := by sorry