PPTTerminalPreimage.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Convert the chosen vacant height window into the actual preimage prefix.

theorem OAI.TotientAsymptotic.ppt_terminal_window_preimage line 15

Source documentation

A vacant prime-height window with its proved error budget supplies all cutoffs for the actual unequal-list preimage truncation.

theorem ppt_terminal_window_preimage : ∀ᶠ z : ℝ in atTop,
    ∀ (N H J d F : ℕ) (p : Fin N → ℕ) (S L U : ℝ),
      ∀ hJ : 0 < J, ∀ hJN : J ≤ N,
      0 < d → 0 < F → N ≤ H → 2 ≤ S → 0 ≤ B S →
      (∀ i, IsNormalPrime S (p i)) → (∀ i, 3 ≤ p i) → StrictAnti p →
      F.totient = d*(∏ i, p i).totient →
      (largestPrimeFactor d : ℝ) ≤ S → SquarefreeAbove F S →
      (∀ q : ℕ, q.Prime → q ∣ F → IsNormalPrime S q) →
      largestPrimeFactor F ≠ p ⟨0,by omega⟩ →
      (∀ i : Fin N, (p i-1 : ℕ) ≤ z) → (F.totient : ℝ) ≤ z →
      (B z)^(2/3 : ℝ) ≤ L → U ≤ 2*(B z)^(2/3 : ℝ) → L < U →
      2*(B z)^(2/3 : ℝ) ≤ B z →
…

Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.largestPrimeFactor, OAI.TotientAsymptotic.SquarefreeAbove