PPTResidualSmallness.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Small common factors and small left tails in the residual comparison.

theorem OAI.TotientAsymptotic.ppt_prime_product_subpower_of_gap line 17

Source documentation

A logarithmic number of primes below the strict first-coordinate gap has an arbitrarily small fixed power of the local value scale.

theorem ppt_prime_product_subpower_of_gap {A γ ε : ℝ}
    (hA : 0 ≤ A) (hγ : 0 < γ) (hε : 0 < ε) :
    ∀ᶠ z : ℝ in atTop, ∀ (n : ℕ) (p : Fin n → ℕ),
      (∀ i, (p i).Prime) → (n : ℝ) ≤ A*Real.log (B z) →
      (∀ i, B (p i) ≤ B z-γ*B z/(Real.log (B z))^3) →
      ((∏ i, p i : ℕ) : ℝ) ≤ z^ε := by
…

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

theorem OAI.TotientAsymptotic.ppt_seed_totient_subpower_of_gap line 63

Source documentation

The same strict coordinate gap makes the seed-multiplied totient small, for the fixed seed and any prescribed positive power.

theorem ppt_seed_totient_subpower_of_gap (d : ℕ) {A γ ε : ℝ}
    (hA : 0 ≤ A) (hγ : 0 < γ) (hε : 0 < ε) :
    ∀ᶠ z : ℝ in atTop, ∀ (n : ℕ) (p : Fin n → ℕ),
      (∀ i, (p i).Prime) → (n : ℝ) ≤ A*Real.log (B z) →
      (∀ i, B (p i) ≤ B z-γ*B z/(Real.log (B z))^3) →
      ((d*(∏ i, p i).totient : ℕ) : ℝ) ≤ z^ε := by
…

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

lemma OAI.TotientAsymptotic.ppt_normal_smooth_prime_coordinate line 82
Source documentation
A normal prime whose predecessor is smooth at V has double logarithm at most 6 B(V). No bound on the prime itself is assumed.
```
lemma ppt_normal_smooth_prime_coordinate {p : ℕ} {S V : ℝ}
    (hp : IsNormalPrime S p) (hp3 : 3 ≤ p) (hS : 1 < S)
    (hBS : 0 ≤ B S) (hSV : S ≤ V) (hBV : 1 ≤ B V)
    (hsmooth : (largestPrimeFactor (p-1) : ℝ) ≤ V) : B p ≤ 6*B V := by
…
```
Mentions: OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.largestPrimeFactor
theorem OAI.TotientAsymptotic.ppt_smooth_height_half_scale line 104
Source documentation
The smooth-tail coordinate scale is eventually below half of the comparison double logarithm.
```
theorem ppt_smooth_height_half_scale : ∀ᶠ t : ℝ in atTop,
    ∀ V : ℝ, B V ≤ 2*t^(2/3 : ℝ) → 6*B V ≤ t/2 := by
…
```
Mentions: OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.B
lemma OAI.TotientAsymptotic.ppt_half_scale_below_gap line 118

theorem OAI.TotientAsymptotic.ppt_normal_small_tail_subpower line 134

Source documentation

A normal small left tail supplies the actual D=d*φ(a) power restriction in Ford's comparison parameters.

theorem ppt_normal_small_tail_subpower (d : ℕ) {A ε : ℝ}
    (hA : 0 ≤ A) (hε : 0 < ε) :
    ∀ᶠ z : ℝ in atTop, ∀ (n : ℕ) (p : Fin n → ℕ) (S V : ℝ),
      (n : ℝ) ≤ A*Real.log (B z) → 1 < S → 0 ≤ B S → S ≤ V →
      1 ≤ B V → B V ≤ 2*(B z)^(2/3 : ℝ) →
      (∀ i, IsNormalPrime S (p i)) → (∀ i, 3 ≤ p i) →
      (∀ i, (largestPrimeFactor (p i-1) : ℝ) ≤ V) →
      ((d*(∏ i, p i).totient : ℕ) : ℝ) ≤ z^ε := by
…

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

theorem OAI.TotientAsymptotic.ppt_prime_gap_of_factor_gap line 155
Source documentation
A gap for largest predecessor factors is a gap for the actual primes, after halving its fixed constant. This supplies smallness of the common canceled prime product.
```
theorem ppt_prime_gap_of_factor_gap {γ : ℝ} (hγ : 0 < γ) :
    ∀ᶠ z : ℝ in atTop, ∀ (p : ℕ) (S : ℝ),
      3 ≤ p → 1 < S → 0 ≤ B S → S ≤ z → IsNormalPrime S p → (p-1 : ℕ) ≤ z →
      B (largestPrimeFactor (p-1))/B z ≤ 1-γ/(Real.log (B z))^3 →
      B p ≤ B z-(γ/2)*B z/(Real.log (B z))^3 := by
…
```
Mentions: OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.largestPrimeFactor