PPTIndexGap.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The local normality error is smaller than every fixed fraction of the two-thirds-power cutoff height. This gives both the right-index existence gap and the separation needed for the right-tail smoothness argument, with no normality transfer between different cutoffs.

theorem OAI.TotientAsymptotic.ppt_local_normality_interval_budget line 19

theorem OAI.TotientAsymptotic.ppt_local_right_index_gap line 81

Source documentation

This is the strict gap required by ppt_ordered_right_index when a retained left coordinate has height at least t^(2/3).

theorem ppt_local_right_index_gap {A : ℝ} (hA : 0 < A) :
    ∀ᶠ z : ℝ in atTop, ∀ (H J : ℕ) (S T : ℝ),
      1 ≤ H → J ≤ H → (H : ℝ) ≤ A*Real.log (B z) →
      0 ≤ B S → B S ≤ (H : ℝ)^4 →
      (B z)^(2/3 : ℝ) ≤ B T → B T ≤ B z →
      (2*(J : ℝ)+1)*Real.sqrt (B S*B T) < B T-B S := by
…

Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.B

theorem OAI.TotientAsymptotic.ppt_local_right_tail_gap line 97

Source documentation

A fixed positive gap between two terminal cutoff heights dominates the same normality error used in the right-tail smoothing argument.

theorem ppt_local_right_tail_gap {A η : ℝ} (hA : 0 < A) (hη : 0 < η) :
    ∀ᶠ z : ℝ in atTop, ∀ (H J : ℕ) (S U V : ℝ),
      1 ≤ H → J ≤ H → (H : ℝ) ≤ A*Real.log (B z) →
      0 ≤ B S → B S ≤ (H : ℝ)^4 →
      η*(B z)^(2/3 : ℝ) ≤ B V-B U →
      (2*(J : ℝ)+1)*Real.sqrt (B S*B z) < B V-B U := by
…

Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.B