Balanced raw correction densities have the uniform squared-logarithmic rate
ProvedErdos390.WholePaper.BankPaperRealization.eventually_roughCanonicalUniformRawRowCorrectionDensityBound_compactanalytic-number-theoryerdos-390erdos390-source-construction
Write , , , and . Fix natural numbers , real , and . Let be the upper-tail length associated to , and choose the canonical balanced coefficient for width , multiplicity , coefficient , and logarithmic scale . Then, for all sufficiently large and every attained active nonexceptional rough label ,
Here is the source's explicit uniform raw-row correction density constant, independent of and . The conclusion is a simultaneous bound over all active correction rows.
Preamble
import Definitions.Def_erdos390_remaining_analytic_propositions_004
Formal statement
theorem Erdos390.WholePaper.BankPaperRealization.eventually_roughCanonicalUniformRawRowCorrectionDensityBound_compact : Erdos390.RemainingAnalyticGoal004_018 := by sorry
Source