Uniform prime-power transfer for a fixed finite family of tilted cells
ProvedErdos390.Full.FixedFiniteMixtureFullUniform.exists_boxIndependent_fixedFiniteMixture_primePower_transferFor a finite bounded valuation law, write , , , and . Write and let all prime sums range over the moving band . The five prime-power transfer estimates with constants mean: the sums of absolute covariances of , , and over higher exponents have bounds , , and , respectively; also and . Higher exponents run from to the valuation cutoff determined by the value bound . Fix finitely many head patterns and real endpoints with . The source constant , called the box-independent prime-power constant, is positive. For every containing all head primes, and every coefficient bound , there exist a nonnegative error sequence and a threshold such that
For every and every tilt coefficient function on the moving prime band, the structured cells with head , physical endpoints , and smoothness cutoff are nonempty. Tilt their uniform laws by the valuation score normalized by , and place their values under the common bound associated to . Every probability mixture of these laws satisfies the five transfer estimates with . The constant is selected before and ; the error and threshold may depend on them. The moving prime band is .
import Definitions.Def_erdos390_remaining_analytic_propositions_001 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_004 universe u_1
theorem Erdos390.Full.FixedFiniteMixtureFullUniform.exists_boxIndependent_fixedFiniteMixture_primePower_transfer : Erdos390.RemainingAnalyticGoal001_001.{u_1} := by sorry