Balanced raw smooth-row discrepancy has the required scale
ProvedErdos390.WholePaper.BankPaperRealization.bankPaperCanonicalBalancedRawSmoothRowDiscrepancy_isBigO_compactanalytic-number-theoryerdos-390erdos390-source-construction
Write , , , , , and . Fix , , and any real . Let be the canonical balanced raw weight. The complete-label-one raw row discrepancy satisfies
This gives the raw smooth-mass estimate used in the initial selector construction.
Preamble
import Definitions.Def_erdos390_remaining_analytic_propositions_004
Formal statement
theorem Erdos390.WholePaper.BankPaperRealization.bankPaperCanonicalBalancedRawSmoothRowDiscrepancy_isBigO_compact : Erdos390.RemainingAnalyticGoal004_010 := by sorry
Source