Uniform agreement of tilted valuation means across finitely many raw cells
ProvedErdos390.Full.PaperRawTiltedValuationMeanRows.exists_uniform_fixedFinite_rawCell_tilted_valuation_mean_agreement_rate_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 . For coefficients , the tilted cell law assigns mass proportional to . Fix a finite cell index set, patterns , and real endpoints with . Fix containing every head prime, and any coefficient bound . There are a nonnegative sequence and such that and, for , all , all on this band, and all nonempty cells, their tilted laws satisfy
The rate is uniform over the finite family and the full coefficient box, with no relation imposed between the box size and the cutoff.
Preamble
import Definitions.Def_erdos390_remaining_analytic_propositions_004 universe u_1
Formal statement
theorem Erdos390.Full.PaperRawTiltedValuationMeanRows.exists_uniform_fixedFinite_rawCell_tilted_valuation_mean_agreement_rate_compact : Erdos390.RemainingAnalyticGoal004_008.{u_1} := by sorrySource