PrimePrefixSize.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem337.PrimePrefixSize.log_prefix_lower line 10

Source documentation

Crossing the square-root cutoff forces a large prefix if the next prime is small.

lemma log_prefix_lower {d p Y v : ℝ}
    (hd : 0 < d) (hp : 0 < p) (hY : 0 < Y)
    (hYlog : v / 2 ≤ Real.log Y)
    (hcross : Real.sqrt Y < d * p)
    (hplog : Real.log p < v ^ (15 / 16 : ℝ))
    (hsmall : v ^ (15 / 16 : ℝ) ≤ v / 20) :
    v / 5 < Real.log d := by
…

Mentions: OAI.Problem337.v

lemma OAI.Problem337.PrimePrefixSize.exp_prefix_lower line 21
lemma OAI.Problem337.PrimePrefixSize.eventually_fifteen_sixteenths_small line 33
lemma OAI.Problem337.PrimePrefixSize.eventually_uniform_lower_scale line 47
Source documentation
The manuscript's lower scale tends uniformly beyond every fixed threshold.
```
lemma eventually_uniform_lower_scale (V : ℝ) :
    ∀ᶠ S : ℝ in atTop, ∀ v : ℝ, S / (2 * Real.log S) ≤ v → V ≤ v := by
…
```
Mentions: OAI.Problem337.v

theorem OAI.Problem337.PrimePrefixSize.eventually_uniform_prefix_large line 67

Source documentation

Uniform prefix-size conclusion over all admissible divisor-moment scales.

theorem eventually_uniform_prefix_large :
    ∀ᶠ S : ℝ in atTop, ∀ v d p Y : ℝ,
      S / (2 * Real.log S) ≤ v →
      0 < d → 0 < p → 0 < Y → v / 2 ≤ Real.log Y →
      Real.sqrt Y < d * p → Real.log p < v ^ (15 / 16 : ℝ) →
      Real.exp (v / 5) < d := by
…

Mentions: OAI.Problem337.v