Common marked profiles imply the finite-mixture prime-power estimates
ProvedErdos390.Full.FixedFiniteMixtureLemma75.sigmaMixture_primePowerTransferBounds_of_common_profilesFor 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 . Let a finite family of bounded valuation laws have arbitrary probability mixture weights. Suppose ; all constants are nonnegative; and the four-mark profile satisfies for , . In every component assume one- and two-prime divisibility expectations differ from the common paper main term by at most and whenever the divisor is at most , where is the source's restored probability scale . Assume also for every positive . The resulting outside-chamber residuals must satisfy the linear, quadratic, diagonal, and row budgets of the finite aggregation theorem, and . Then
where and is the fixed paper prime-power constant. Thus the five estimates include the full between-component covariance. Explicitly, ; the generic remainder 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 u_2
theorem Erdos390.Full.FixedFiniteMixtureLemma75.sigmaMixture_primePowerTransferBounds_of_common_profiles : Erdos390.RemainingAnalyticGoal001_002.{u_1, u_2} := by sorry