Explicit raw valuation-prefix covariance bound
ProvedErdos390.Full.PaperRawPrefixValuationRow.exists_uniform_rawCell_valuation_prefix_bound_compactanalytic-number-theoryerdos-390erdos390-source-construction
Write , , , and . For a head pattern , let be the positive -smooth integers in having exactly the valuations prescribed by . Fix , with , and containing every head prime. There exist and such that for , , , and any nonempty with uniform law ,
Here is the source prime-power cutoff scale (cutoffScale).
The estimate exposes the beyond-four-prime-power tail separately from the principal reciprocal row bound.
Preamble
import Definitions.Def_erdos390_remaining_analytic_propositions_004
Formal statement
theorem Erdos390.Full.PaperRawPrefixValuationRow.exists_uniform_rawCell_valuation_prefix_bound_compact : Erdos390.RemainingAnalyticGoal004_006 := by sorry
Source