PPTTerminalGap.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A vacant terminal window is chosen from the actual finite list of left prime heights. Its width remains larger than the local normality error, so the comparison's last upper cutoff can be placed inside that window.

lemma OAI.TotientAsymptotic.ppt_empty_separated_window line 18

Source documentation

Among n+1 disjoint closed windows, one misses all n coordinates.

lemma ppt_empty_separated_window {n : ℕ} (x : Fin n → ℝ) {T δ : ℝ}
    (hδ : 0 < δ) :
    ∃ j : Fin (n+1), ∀ i : Fin n,
      ¬(T+2*(j.val : ℝ)*δ ≤ x i ∧ x i ≤ T+(2*(j.val : ℝ)+1)*δ) := by
…

lemma OAI.TotientAsymptotic.ppt_antitone_split_at_empty_window line 51

Source documentation

An empty height window splits a decreasing list into a high prefix and a low suffix; equality at either endpoint is excluded.

lemma ppt_antitone_split_at_empty_window {n : ℕ} (x : Fin n → ℝ)
    (hx : Antitone x) {L U : ℝ}
    (hempty : ∀ i, ¬(L ≤ x i ∧ x i ≤ U)) :
    ∃ J : ℕ, J ≤ n ∧
      (∀ i : Fin n, i.val < J → U < x i) ∧
      (∀ i : Fin n, J ≤ i.val → x i < L) := by
…

Mentions: OAI.TotientAsymptotic.L

theorem OAI.TotientAsymptotic.ppt_terminal_gap line 78

Source documentation

The terminal split has an explicit width even when the number of left primes is smaller than the ambient dimension bound.

theorem ppt_terminal_gap {n H : ℕ} (x : Fin n → ℝ) (hx : Antitone x)
    {T : ℝ} (hT : 0 < T) (hn : n ≤ H) :
    ∃ L U : ℝ, ∃ J : ℕ,
      T ≤ L ∧ U ≤ 2*T ∧ L < U ∧
      T/(2*((H : ℝ)+1)) ≤ U-L ∧ J ≤ n ∧
      (∀ i : Fin n, i.val < J → U < x i) ∧
      (∀ i : Fin n, J ≤ i.val → x i < L) := by
…

Mentions: OAI.TotientAsymptotic.L

theorem OAI.TotientAsymptotic.ppt_terminal_normality_budget line 114

Source documentation

Normality errors fit inside a reciprocal-dimension fraction of the terminal height range. This is stronger than a fixed-fraction gap.

theorem ppt_terminal_normality_budget {A η : ℝ} (_hA : 0 < A) (hη : 0 < η) :
    ∀ᶠ t : ℝ in atTop, ∀ (H J : ℕ) (s X : ℝ),
      1 ≤ H → J ≤ H → (H : ℝ) ≤ A*Real.log t →
      0 ≤ s → s ≤ (H : ℝ)^4 → 0 ≤ X → X ≤ t →
      (2*(J : ℝ)+1)*Real.sqrt (s*X)+s < η*t^(2/3 : ℝ)/((H : ℝ)+1) := by
…

Mentions: OAI.TotientAsymptotic.A