PPTHeadSelectedGrid.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The original-head grid keeps only the surviving nonleading primes inside the geometric tail. The head itself is handled by the top row.

def OAI.TotientAsymptotic.pptRemoveHeadEmbedding line 15
Source documentation
Delete the leading coordinate from an ordered embedding fixing zero.
```
def pptRemoveHeadEmbedding {b N : ℕ} (e : Fin b ↪o Fin N)
    (hb : 0 < b) (_hN : 0 < N) (he : (e ⟨0,hb⟩).val=0) : Fin (b-1) ↪o Fin (N-1) :=
…
```
Mentions: OAI.TotientAsymptotic.N
lemma OAI.TotientAsymptotic.ppt_remove_head_embedding_succ line 36

theorem OAI.TotientAsymptotic.ppt_head_selected_grid_data line 46

Source documentation

Finite comparison labels for a head outside the geometric vector.

theorem ppt_head_selected_grid_data (d : ℕ) (hd : 0 < d) {A : ℝ} (hA : 0 < A) :
    ∀ᶠ z : ℝ in atTop,
    ∀ (m n N Q J H E r j : ℕ) (p : Fin N → ℕ) (q : Fin Q → ℕ)
      (v : Fin n → ℝ) (ι : Fin (N-1) ↪o Fin n) (budget g S L U V : ℝ),
      ∀ hJ : 0 < J, ∀ hJN : J ≤ N, ∀ hJQ : J ≤ Q,
      n ≤ m → N ≤ H → j ≤ H → (H : ℝ) ≤ A*Real.log (B z) →
      m+1 ≤ H → budget ≤ B z+1 →
      v ∈ relaxedGeometricFamily m n budget g →
      (∀ i : Fin (N-1),v (ι i)=B (p ⟨i.val+1,by omega⟩)) →
      (∀ i k : Fin N,i < k → B (p k) ≤ B (p i)/(1+1/(10*(H:ℝ)^3))) →
      Real.exp (Real.exp 1) ≤ S → B S ≤ (H : ℝ)^4 →
      V=Real.exp (Real.exp ((L+U)/2)) → S ≤ V → V ≤ z →
…

Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.g, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.relaxedGeometricFamily