Full two-prime valuation tilt with harmonic-rate remainder
ProvedErdos390.Full.FullTiltPairHarmonicRate.exists_uniform_fullTilt_pairPower_paper_bound_of_le_with_harmonic_rate_compactanalytic-number-theoryerdos-390erdos390-source-construction
Write , , , , and . Let denote the Dickman function. Fix a head pattern , , , and integer . There exist a nonnegative sequence with , , and tending to zero, and a uniform threshold . For , distinct band primes coprime to the head modulus, , and coefficients bounded by on the whole prime band, the structured cell is nonempty. Tilt its uniform law by the full band valuation score. Put , and let be the two-local restoration error with actual valuation cutoffs and the prescribed pair fallback constant.
This supplies the actual full-valuation two-prime chamber estimate, with a remainder strong enough for two harmonic losses.
Preamble
import Definitions.Def_erdos390_remaining_analytic_propositions_001
Formal statement
theorem Erdos390.Full.FullTiltPairHarmonicRate.exists_uniform_fullTilt_pairPower_paper_bound_of_le_with_harmonic_rate_compact : Erdos390.RemainingAnalyticGoal001_004 := by sorry
Source