PPTGeometricGrid.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Prime-coordinate contraction supplies the two geometric hypotheses of the actual residual-grid theorem, including its singleton case.

lemma OAI.TotientAsymptotic.ppt_terminal_first_cutoff_loss line 13

lemma OAI.TotientAsymptotic.ppt_geometric_embedded_contraction line 44

Source documentation

Passing to an ordered sublist retains one common inverse-cube contraction, measured by the remaining length at its first coordinate.

lemma ppt_geometric_embedded_contraction {m n b H : ℕ} {budget c : ℝ}
    {v : Fin n → ℝ} (hv : v ∈ relaxedGeometricFamily m n budget c)
    (hnm : n ≤ m) (ι : Fin b ↪o Fin n) (hb : 0 < b)
    (hH : m-(ι ⟨0,hb⟩).val ≤ H) :
    1/(10*(H : ℝ)^3) ≤ 1 ∧
      ∀ i j : Fin b, i < j →
        v (ι j) ≤ v (ι i)/(1+1/(10*(H : ℝ)^3)) := by
…

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

theorem OAI.TotientAsymptotic.ppt_geometric_pair_grid line 91

Source documentation

An actual prime row gives both the first-cutoff loss and all paired grid gaps. No coordinate separation is assumed after taking largest factors: those errors are supplied by normality and the doubled mesh.

theorem ppt_geometric_pair_grid {A : ℝ} (hA : 0 < A) :
    ∀ᶠ z : ℝ in atTop,
    ∀ (b H : ℕ) (S L U ω : ℝ) (p : ShiftedPair b), ∀ _hb : 0 < b,
      b ≤ H → (H : ℝ) ≤ A*Real.log (B z) →
      1 < S → 0 ≤ B S → S ≤ z →
      (∀ i, IsNormalPrime S (p.left i)) →
      (∀ i, 3 ≤ p.left i) →
      (∀ i, (p.left i-1 : ℕ) ≤ z) →
      1/(10*(H : ℝ)^3) ≤ ω → ω ≤ 1 →
      (∀ i : Fin b, (B z)^(2/3 : ℝ) ≤ B (p.left i)) →
      (∀ i : Fin b, ∀ hi : i.val+1 < b,
        B (p.left ⟨i.val+1,hi⟩) ≤ B (p.left i)/(1+ω)) →
…

Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.ShiftedPair, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.IsNormalPrime