@[reducible, inline]

noncomputable abbrev nth_prime (n : ℕ) : ℕ

Equations

• nth_prime n = Nat.nth Nat.Prime n

@[reducible, inline]

noncomputable abbrev nth_prime' (n : ℕ) : ℕ

Equations

• nth_prime' n = Nat.nth Nat.Prime (n - 1)

@[reducible, inline]

noncomputable abbrev Psi (x : ℝ) : ℝ

Equations

• Psi x = Chebyshev.psi x

noncomputable def M (x : ℝ) : ℝ

Equations

• M x = ∑ n ≤ ⌊x⌋₊, ↑(ArithmeticFunction.moebius n)

@[reducible, inline]

noncomputable abbrev nth_prime_gap (n : ℕ) : ℕ

Equations

• nth_prime_gap n = nth_prime (n + 1) - nth_prime n

def prime_gap_record (p g : ℕ) : Prop

Equations

• prime_gap_record p g = ∃ (n : ℕ), nth_prime n = p ∧ nth_prime_gap n = g ∧ ∀ (k : ℕ), nth_prime k < p → nth_prime_gap k < g

noncomputable def first_gap (g : ℕ) : ℕ

Equations

• first_gap g = if h : ∃ (n : ℕ), nth_prime_gap n = g then nth_prime (Nat.find h) else 0

def first_gap_record (g P : ℕ) : Prop

Equations

• first_gap_record g P = (first_gap g = P ∧ ∀ g' ∈ Finset.Ico 1 g, Even g' ∨ g' = 1 → first_gap g' ∈ Set.Ico 1 P)

def HasPrimeInInterval (x h : ℝ) : Prop

Equations

• HasPrimeInInterval x h = ∃ (p : ℕ), Nat.Prime p ∧ x < ↑p ∧ ↑p ≤ x + h

def HasPrimeInInterval.log_thm (X₀ k : ℝ) : Prop

Equations

• HasPrimeInInterval.log_thm X₀ k = ∀ x ≥ X₀, HasPrimeInInterval x (x / Real.log x ^ k)

noncomputable def pi (x : ℝ) : ℝ

Equations

• pi x = ↑⌊x⌋₊.primeCounting

noncomputable def pi_star (x : ℝ) : ℝ

Equations

• pi_star x = ∑' (k : ℕ), pi (x ^ (1 / ↑k)) / ↑k

noncomputable def li (x : ℝ) : ℝ

Equations

• li x = (Filter.map (fun (ε : ℝ) => ∫ (t : ℝ) in (Set.Ioc 0 x).diff (Set.Ioo (1 - ε) (1 + ε)), 1 / Real.log t) (nhdsWithin 0 (Set.Ioi 0))).lim

noncomputable def Li (x : ℝ) : ℝ

Equations

• Li x = ∫ (t : ℝ) in 2..x, 1 / Real.log t

noncomputable def Eψ (x : ℝ) : ℝ

Equations

• Eψ x = |Chebyshev.psi x - x| / x

noncomputable def admissible_bound (A B C R x : ℝ) : ℝ

Equations

• admissible_bound A B C R x = A * (Real.log x / R) ^ B * Real.exp (-C * (Real.log x / R) ^ (1 / 2))

def Eψ.classicalBound (A B C R x₀ : ℝ) : Prop

Equations

• Eψ.classicalBound A B C R x₀ = ∀ x ≥ x₀, Eψ x ≤ admissible_bound A B C R x

def Eψ.bound (ε x₀ : ℝ) : Prop

Equations

• Eψ.bound ε x₀ = ∀ x ≥ x₀, Eψ x ≤ ε

def Eψ.numericalBound (x₀ : ℝ) (ε : ℝ → ℝ) : Prop

Equations

• Eψ.numericalBound x₀ ε = Eψ.bound (ε x₀) x₀

noncomputable def Eπ (x : ℝ) : ℝ

Equations

• Eπ x = |pi x - Li x| / (x / Real.log x)

noncomputable def Eπ_star (x : ℝ) : ℝ

Equations

• Eπ_star x = |pi_star x - Li x| / (x / Real.log x)

noncomputable def Eθ (x : ℝ) : ℝ

Equations

• Eθ x = |Chebyshev.theta x - x| / x

def Eθ.classicalBound (A B C R x₀ : ℝ) : Prop

Equations

• Eθ.classicalBound A B C R x₀ = ∀ x ≥ x₀, Eθ x ≤ admissible_bound A B C R x

def Eθ.numericalBound (x₀ : ℝ) (ε : ℝ → ℝ) : Prop

Equations

• Eθ.numericalBound x₀ ε = ∀ x ≥ x₀, Eθ x ≤ ε x₀

def Eπ.classicalBound (A B C R x₀ : ℝ) : Prop

Equations

• Eπ.classicalBound A B C R x₀ = ∀ x ≥ x₀, Eπ x ≤ admissible_bound A B C R x

def Eπ.bound (ε x₀ : ℝ) : Prop

Equations

• Eπ.bound ε x₀ = ∀ x ≥ x₀, Eπ x ≤ ε

def Eπ.numericalBound (x₀ : ℝ) (ε : ℝ → ℝ) : Prop

Equations

• Eπ.numericalBound x₀ ε = Eπ.bound (ε x₀) x₀

def Eπ.vinogradovBound (A B C x₀ : ℝ) : Prop

Equations

• Eπ.vinogradovBound A B C x₀ = ∀ x ≥ x₀, Eπ x ≤ A * Real.log x ^ B * Real.exp (-C * Real.log x ^ (3 / 5) / Real.log (Real.log x) ^ (1 / 5))

def Eπ_star.classicalBound (A B C R x₀ : ℝ) : Prop

Equations

• Eπ_star.classicalBound A B C R x₀ = ∀ x ≥ x₀, Eπ_star x ≤ admissible_bound A B C R x

def Eπ_star.bound (ε x₀ : ℝ) : Prop

Equations

• Eπ_star.bound ε x₀ = ∀ x ≥ x₀, Eπ_star x ≤ ε

def Eπ_star.numericalBound (x₀ : ℝ) (ε : ℝ → ℝ) : Prop

Equations

• Eπ_star.numericalBound x₀ ε = Eπ_star.bound (ε x₀) x₀

def Eπ_star.vinogradovBound (A B C x₀ : ℝ) : Prop

Equations

• Eπ_star.vinogradovBound A B C x₀ = ∀ x ≥ x₀, Eπ_star x ≤ A * Real.log x ^ B * Real.exp (-C * Real.log x ^ (3 / 5) / Real.log (Real.log x) ^ (1 / 5))

theorem admissible_bound.mono (A B C R : ℝ) (hA : 0 < A) (hB : 0 < B) (hC : 0 < C) (hR : 0 < R) : AntitoneOn (admissible_bound A B C R) (Set.Ici (Real.exp (R * (2 * B / C) ^ 2)))

theorem Eψ.classicalBound.to_numericalBound (A B C R x₀ x₁ : ℝ) (hA : 0 < A) (hB : 0 < B) (hC : 0 < C) (hR : 0 < R) (hEψ : classicalBound A B C R x₀) (hx₁ : x₁ ≥ max x₀ (Real.exp (R * (2 * B / C) ^ 2))) : numericalBound x₁ fun (x : ℝ) => admissible_bound A B C R x

theorem Eθ.classicalBound.to_numericalBound (A B C R x₀ x₁ : ℝ) (hA : 0 < A) (hB : 0 < B) (hC : 0 < C) (hR : 0 < R) (hEθ : classicalBound A B C R x₀) (hx₁ : x₁ ≥ max x₀ (Real.exp (R * (2 * B / C) ^ 2))) : numericalBound x₁ fun (x : ℝ) => admissible_bound A B C R x

theorem Eπ.classicalBound.to_numericalBound (A B C R x₀ x₁ : ℝ) (hA : 0 < A) (hB : 0 < B) (hC : 0 < C) (hR : 0 < R) (hEπ : classicalBound A B C R x₀) (hx₁ : x₁ ≥ max x₀ (Real.exp (R * (2 * B / C) ^ 2))) : numericalBound x₁ fun (x : ℝ) => admissible_bound A B C R x