Source indexedlemma · leanprover/lean4:v4.32.0

Eθ.classicalBound.hasPrimeInInterval

PrimeNumberTheoremAnd.IEANTN.PrimeInInterval · PrimeNumberTheoremAnd/IEANTN/PrimeInInterval.lean:184 to 203

Mathematical statement

Exact Lean statement

@[blueprint
  "etheta-classical-pi"
  (title := "Classical bound on Etheta implies prime in short interval")
  (statement := /--
  If $E_\theta(x)$ enjoys a classical bound for all $x \geq x_0$, $x \geq \exp( R (2B/C)^2 )$
  and $(2x+h) A \left(\frac{\log x}{R}\right)^B
  \exp\left(-C \left(\frac{\log x}{R}\right)^{1/2}\right) < h$,
  then there is a prime in $(x, x+h]$. -/)
  (proof := /-- Apply Lemma \ref{etheta-num-pi} and Lemma \ref{classical-to-numeric}. -/)
  (latexEnv := "lemma")
  (discussion := 909)]
lemma Eθ.classicalBound.hasPrimeInInterval {x₀ x h A B C R : ℝ}
    (hEθ : Eθ.classicalBound A B C R x₀) (hA : 0 < A) (hB : 0 < B) (hC : 0 < C) (hR : 0 < R)
    (hh : 0 < h) (hx : x₀ ≤ x) (hx' : x ≥ exp (R * (2 * B / C) ^ 2))
    (hb : (2 * x + h) * (admissible_bound A B C R x) < h) :
    HasPrimeInInterval x h

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "etheta-classical-pi"  (title := "Classical bound on Etheta implies prime in short interval")  (statement := /--  If $E_\theta(x)$ enjoys a classical bound for all $x \geq x_0$, $x \geq \exp( R (2B/C)^2 )$  and $(2x+h) A \left(\frac{\log x}{R}\right)^B  \exp\left(-C \left(\frac{\log x}{R}\right)^{1/2}\right) < h$,  then there is a prime in $(x, x+h]$. -/)  (proof := /-- Apply Lemma \ref{etheta-num-pi} and Lemma \ref{classical-to-numeric}. -/)  (latexEnv := "lemma")  (discussion := 909)]lemma Eθ.classicalBound.hasPrimeInInterval {x₀ x h A B C R : ℝ}    (hEθ : Eθ.classicalBound A B C R x₀) (hA : 0 < A) (hB : 0 < B) (hC : 0 < C) (hR : 0 < R)    (hh : 0 < h) (hx : x₀ ≤ x) (hx' : x ≥ exp (R * (2 * B / C) ^ 2))    (hb : (2 * x + h) * (admissible_bound A B C R x) < h) :    HasPrimeInInterval x h := by  have : Eθ.numericalBound x _ :=    Eθ.classicalBound.to_numericalBound A B C R x₀ x hA hB hC hR hEθ (max_le hx hx')  have hx_pos : x > 0 := lt_of_lt_of_le (exp_pos _) hx'  exact Eθ.numericalBound.hasPrimeInInterval this hh (le_refl _) hx_pos hb