PPTTerminalSelection.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A finite terminal-window label with enough room for alignment and grid errors.

theorem OAI.TotientAsymptotic.ppt_select_terminal_window line 15

Source documentation

The terminal cutoff is selected from N+1 explicit windows. The entire normality and paired-grid budget fits inside a quarter of the chosen vacant interval.

theorem ppt_select_terminal_window {A : ℝ} (hA : 0 < A) :
    ∀ᶠ t : ℝ in atTop, ∀ (N H : ℕ) (x : Fin N → ℝ) (s : ℝ),
      ∀ hN : 0 < N,
      Antitone x → N ≤ H → 1 ≤ H → (H : ℝ) ≤ A*Real.log t →
      0 ≤ s → s ≤ (H : ℝ)^4 → 2*t^(2/3 : ℝ) < x ⟨0,hN⟩ →
      ∃ j : Fin (N+1), ∃ J : ℕ,
        let L := t^(2/3 : ℝ)+2*(j.val : ℝ)*(t^(2/3 : ℝ)/(2*((N : ℝ)+1)))
…

Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.L