Balanced Saias transition budget at the canonical row scale
ProvedErdos390.WholePaper.roughCanonicalBalancedSaiasTransitionBudget_leanalytic-number-theoryerdos-390erdos390-source-construction
Write , , , and . Fix natural W and , real , and . Let , , , , , , and . Put , use the source head density and balanced alpha, and take the four physical endpoints , , , and x. The source physical Saias transition budget , using the inverse-log-square endpoint rate at the sharp Saias defect constant, satisfies
Here is the sharp transition-row scale constant.
The three weighted sharp Saias pair budgets have the same uniform scale as the Dickman contribution.
Preamble
import Definitions.Def_erdos390_remaining_analytic_propositions_008 import Mathlib import Definitions.Def_erdos390_source_bank_interface import Definitions.Def_erdos390_dickman_step_function import Theorems.Thm_MediumPNT import Definitions.Def_erdos390_analytic_foundations_001 import Theorems.Thm_Erdos390_Full_DickmanBasic_kernel_product_bound import Theorems.Thm_Erdos390_Full_DickmanBasic_rho_pos_on_zero_five import Theorems.Thm_Erdos390_Full_DickmanBasic_kernel_secondDerivative_first_bound import Definitions.Def_erdos390_analytic_foundations_006 import Definitions.Def_erdos390_analytic_foundations_008 import Definitions.Def_erdos390_analytic_foundations_009
Formal statement
theorem Erdos390.WholePaper.roughCanonicalBalancedSaiasTransitionBudget_le : Erdos390.RemainingAnalyticGoal008_015 := by sorry
Source