PPTGridSeparation.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The grid separation used in the residual comparison follows from the actual contraction of candidate prime coordinates. Normality changes a prime coordinate to its largest-predecessor-factor coordinate by at most the doubled mesh. The inverse-cube contraction still dominates all paired-grid padding in the logarithmic local dimension range.

theorem OAI.TotientAsymptotic.ppt_normal_factor_loss_mesh line 22

Source documentation

Uniform replacement of a normal prime by the largest factor of its predecessor, on the local comparison scale.

theorem ppt_normal_factor_loss_mesh : ∀ᶠ z : ℝ in atTop,
    ∀ (p : ℕ) (S : ℝ), 3 ≤ p → 1 < S → 0 ≤ B S → S ≤ z →
      IsNormalPrime S p → (p-1 : ℕ) ≤ z →
      B p/B z-2*((Real.log (B z))^5/Real.sqrt (B z)) ≤
        B (largestPrimeFactor (p-1))/B z ∧
      B (largestPrimeFactor (p-1))/B z ≤ B p/B z := by
…

Mentions: OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.largestPrimeFactor

lemma OAI.TotientAsymptotic.ppt_contracted_factor_gap line 62

Source documentation

A geometric contraction of prime coordinates gives a quantitative gap after replacing them by predecessor-factor coordinates.

lemma ppt_contracted_factor_gap {t u u' v v' ω δ : ℝ} {H : ℕ}
    (ht : 0 < t) (hH : 1 ≤ H)
    (hlower : 1/t^(1/3 : ℝ) ≤ u)
    (hω : 1/(10*(H : ℝ)^3) ≤ ω) (hω1 : ω ≤ 1)
    (hcontract : u' ≤ u/(1+ω))
    (hfactor : u-δ ≤ v) (hfactor' : v' ≤ u') :
    1/(20*(H : ℝ)^3*t^(1/3 : ℝ))-δ ≤ v-v' := by
…

lemma OAI.TotientAsymptotic.ppt_paired_gap_of_inverse_cube line 84

Source documentation

The same gap pays for both normality alignment errors and the larger padding that also gives the published adjacent-cutoff gap.

lemma ppt_paired_gap_of_inverse_cube {u u' v v' δ G : ℝ} {H j : ℕ}
    (hδ : 0 ≤ δ) (hG : 0 < G) (hj : j ≤ H)
    (hsmall : (8*(H : ℝ)+20)*δ < G)
    (hgap : 2*G-δ ≤ u-u')
    (halign : |u-v| ≤ (2*(j : ℝ)+1)*δ)
    (halign' : |u'-v'| ≤ (2*(j : ℝ)+3)*δ) :
    max u' v'+(2*(j : ℝ)+8)*δ < min u v := by
…

Mentions: OAI.TotientAsymptotic.G

theorem OAI.TotientAsymptotic.ppt_local_contracted_grid_separation line 101

Source documentation

Uniform geometric and normality estimates imply the actual paired grid separation for every retained adjacent coordinate.

theorem ppt_local_contracted_grid_separation {A : ℝ} (hA : 0 < A) :
    ∀ᶠ t : ℝ in atTop, ∀ (H j : ℕ) (u u' v v' ω : ℝ),
      1 ≤ H → (H : ℝ) ≤ A*Real.log t → j ≤ H →
      1/t^(1/3 : ℝ) ≤ u →
      1/(10*(H : ℝ)^3) ≤ ω → ω ≤ 1 → u' ≤ u/(1+ω) →
      u-2*((Real.log t)^5/Real.sqrt t) ≤ v → v' ≤ u' →
      ∀ (w w' : ℝ),
        |v-w| ≤ (2*(j : ℝ)+1)*(2*((Real.log t)^5/Real.sqrt t)) →
        |v'-w'| ≤ (2*(j : ℝ)+3)*(2*((Real.log t)^5/Real.sqrt t)) →
        max v' w'+(2*(j : ℝ)+8)*(2*((Real.log t)^5/Real.sqrt t)) < min v w := by
…

Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.w

theorem OAI.TotientAsymptotic.ppt_local_contracted_first_loss line 133

Source documentation

The first rounded coordinate keeps a fixed inverse-log-cube loss from one. This feeds both the published first-cutoff power restriction and the common adaptive head endpoint.

theorem ppt_local_contracted_first_loss {A : ℝ} (hA : 0 < A) :
    ∀ᶠ t : ℝ in atTop, ∀ (H : ℕ) (ω u ν : ℝ),
      1 ≤ H → (H : ℝ) ≤ A*Real.log t →
      1/(10*(H : ℝ)^3) ≤ ω → ω ≤ 1 →
      u ≤ (1+1/t)/(1+ω) →
      ν ≤ u+(2*(H : ℝ)+3)*(2*((Real.log t)^5/Real.sqrt t)) →
      ν ≤ 1-(1/(80*A^3))/(Real.log t)^3 := by
…

Mentions: OAI.TotientAsymptotic.A