PPTComparisonBlockDecay.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The finite Ford comparison sum with its actual reciprocal masses. The geometric and normality conditions remain explicit; the logarithmic dimension range and strict exponent saving absorb all the scalar costs.

theorem OAI.TotientAsymptotic.ppt_comparison_mass_decay line 19

Source documentation

The exact comparison-sum expression has an arbitrary inverse-power saving once the local geometric bounds and finite mass bound hold.

theorem ppt_comparison_mass_decay {C A γ M : ℝ} (hC : 0 < C)
    (hA : 0 ≤ A) (hγ : 0 < γ) (d : ℕ) (K : ℝ) :
    ∀ᶠ z : ℝ in atTop, ∀ (b h : ℕ) (W V Rmass Amass Q : ℝ) (Y U : ℕ → ℝ),
      1 ≤ b → (b : ℝ) ≤ A*Real.log (B z) → (h : ℝ) ≤ A*Real.log (B z) →
      1 < Y b → B (Y b) ≤ 2*(B z)^(2/3 : ℝ) →
      0 ≤ B V → B V ≤ 2*(B z)^(2/3 : ℝ) →
      Rmass*Amass ≤ Real.exp (M*(Real.log (B z))^2) →
      -2+(∑ j ∈ Finset.Icc 1 (b-1), a j*(B (Y j)/B z))+
        comparisonError b z W Y U ≤ -1-γ/(Real.log (B z))^3 →
      Q ≤ z/(d : ℝ)*pptComparisonScale C b z W Y U*
        ((b+1 : ℝ)^d.primeFactorsList.length*
          Real.exp (4*(h : ℝ)*B V*Real.log (b+1)))*Rmass*Amass →
…

Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.M, OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.comparisonError, OAI.TotientAsymptotic.pptComparisonScale

theorem OAI.TotientAsymptotic.ppt_normal_tail_block_decay line 80

Source documentation

The actual finite family of normal-tail comparison blocks satisfies the saved bound. In particular no estimate for those blocks is assumed in this application theorem.

theorem ppt_normal_tail_block_decay (d : ℕ) (hd : 0 < d)
    {A γ M : ℝ} (hA : 0 ≤ A) (hγ : 0 < γ) (K : ℝ) :
    ∀ᶠ z : ℝ in atTop, ∀ (b h : ℕ) (W V : ℝ) (Y U : ℕ → ℝ)
      (R Tails : Finset ℕ) (T : ℕ → ℕ → Finset ℕ)
      (tail : ℕ → Fin h → ℕ) (t : ℕ → ℕ → ℕ → ShiftedPair b),
      1 ≤ b → (b : ℝ) ≤ A*Real.log (B z) → (h : ℝ) ≤ A*Real.log (B z) →
      1 < W → 0 ≤ B W → W ≤ V → 1 < Y b →
      B (Y b) ≤ 2*(B z)^(2/3 : ℝ) → 0 ≤ B V → B V ≤ 2*(B z)^(2/3 : ℝ) →
      (∑ c ∈ R, 1/(c.totient : ℝ))*(∑ a ∈ Tails, 1/(a.totient : ℝ)) ≤
        Real.exp (M*(Real.log (B z))^2) →
      -2+(∑ j ∈ Finset.Icc 1 (b-1), a j*(B (Y j)/B z))+
        comparisonError b z W Y U ≤ -1-γ/(Real.log (B z))^3 →
…

Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.M, OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.ShiftedPair, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.comparisonError