PPTRelativeHead.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The head of each local dyadic suffix is large relative to that suffix's value scale.

theorem OAI.TotientAsymptotic.ppt_local_suffix_head line 16

Source documentation

The actual inverse-cube coordinate gap makes every suffix tail a small power of its dyadic value endpoint. The first prime therefore satisfies the large-head hypothesis in the comparison theorem.

theorem ppt_local_suffix_head (d : ℕ) {A : ℝ} (hA : 0 < A) :
    ∀ᶠ z : ℝ in atTop, ∀ (N H : ℕ) (p : Fin N → ℕ) (ω : ℝ),
      ∀ hN : 0 < N,
      (∀ i, (p i).Prime) → (∀ i, 3 ≤ p i) →
      1 ≤ H → N ≤ H → (H : ℝ) ≤ A*Real.log (B z) →
      1/(10*(H : ℝ)^3) ≤ ω → ω ≤ 1 →
      (∀ i : Fin N, 0 < i.val → B (p i) ≤ B (p ⟨0,hN⟩)/(1+ω)) →
      (p ⟨0,hN⟩-1 : ℕ) ≤ z →
      z/2 < ((d*(∏ i, p i).totient : ℕ) : ℝ) →
      z^(9/10 : ℝ) < p ⟨0,hN⟩ := by
…

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

theorem OAI.TotientAsymptotic.ppt_geometric_suffix_head line 96

Source documentation

Direct specialization to any suffix of the constructed geometric prime family. Its actual first coordinate controls the local dimension and supplies the required contraction.

theorem ppt_geometric_suffix_head (d : ℕ) {c : ℝ} (hc : 0 < c) :
    ∀ᶠ z : ℝ in atTop, ∀ (m n : ℕ) (budget : ℝ) (p : Fin n → ℕ),
      n ≤ m → (∀ j, (p j).Prime) → (∀ j, 3 ≤ p j) →
      primePrefixCoord p ∈ relaxedGeometricFamily m n budget c →
      ∀ i : Fin n, (p i-1 : ℕ) ≤ z →
        z/2 < ((d*(∏ j, primeFinal p i.val j).totient : ℕ) : ℝ) →
        z^(9/10 : ℝ) < p i := by
…

Mentions: OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.primePrefixCoord, OAI.TotientAsymptotic.relaxedGeometricFamily, OAI.TotientAsymptotic.primeFinal