PPTComparisonScaleDecay.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The literal Ford comparison prefactor in the PPT range. The number of high and low primes is logarithmic in t; the terminal cutoff has double logarithm at most 2 t^(2/3). All fixed-seed and finite-family costs are retained before applying the proved strict-exponent decay.

def OAI.TotientAsymptotic.pptFullComparisonPrefactor line 19
def OAI.TotientAsymptotic.pptPrefactorConstant line 23
lemma OAI.TotientAsymptotic.ppt_log_prefactor_bound line 26

theorem OAI.TotientAsymptotic.ppt_full_prefactor_bound line 101

Source documentation

The complete positive prefactor is at most the required exponential in t^(2/3) (log t)^2, uniformly in both prime-list lengths.

theorem ppt_full_prefactor_bound {C A t u V M : ℝ} {b D h : ℕ}
    (hC : 0 < C) (hA : 0 ≤ A) (ht : 1 ≤ Real.log t) (ht0 : 0 < t)
    (hb : 1 ≤ b) (hbL : (b : ℝ) ≤ A*Real.log t)
    (hhL : (h : ℝ) ≤ A*Real.log t) (hu : 0 < u)
    (huT : Real.log u ≤ 2*t^(2/3 : ℝ))
    (hV0 : 0 ≤ V) (hV : V ≤ 2*t^(2/3 : ℝ)) :
    pptFullComparisonPrefactor C t b D h u V M ≤
      Real.exp (pptPrefactorConstant C A M D*t^(2/3 : ℝ)*(Real.log t)^2) := by
…

Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.M, OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.pptFullComparisonPrefactor, OAI.TotientAsymptotic.pptPrefactorConstant

theorem OAI.TotientAsymptotic.ppt_full_comparison_decay line 139

Source documentation

The literal prefactor, seed cost, normal-tail cost and finite-family mass are absorbed by the strict inverse-log-cube exponent saving.

theorem ppt_full_comparison_decay {C A γ M : ℝ} (hC : 0 < C) (hA : 0 ≤ A)
    (hγ : 0 < γ) (D : ℕ) (K : ℝ) :
    ∀ᶠ z : ℝ in atTop, ∀ (b h : ℕ) (u V E : ℝ),
      1 ≤ b → (b : ℝ) ≤ A*Real.log (B z) → (h : ℝ) ≤ A*Real.log (B z) →
      0 < u → Real.log u ≤ 2*(B z)^(2/3 : ℝ) →
      0 ≤ V → V ≤ 2*(B z)^(2/3 : ℝ) →
      E ≤ -1-γ/(Real.log (B z))^3 →
      pptFullComparisonPrefactor C (B z) b D h u V M*(Real.log z)^E ≤
        (Real.log z)⁻¹*(B z)^(-K) := by
…

Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.M, OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.pptFullComparisonPrefactor