import ErdosBorwein.Core

noncomputable section

namespace ErdosBorwein

/-- Primes at most `X` in the residue class `s` modulo `B`. -/
def primesAP (X B s : ℕ) : Finset ℕ :=
  (Finset.range (X + 1)).filter fun p => p.Prime ∧ Nat.ModEq B p s

/-- The Alford--Granville--Pomerance estimate, in the form of
Vandehey, Proposition 2.1. This is an explicit external input, not
a theorem claimed to have been formalized in this project. -/
def AGP : Prop :=
  ∃ X₀ D₀ : ℕ, ∀ X : ℕ, X₀ ≤ X →
    ∃ exceptional : Finset ℕ,
      exceptional.card ≤ D₀ ∧
      (∀ D ∈ exceptional, Real.log (X : ℝ) < (D : ℝ)) ∧
      ∀ B s : ℕ, 1 ≤ B →
        (B : ℝ) ≤ (X : ℝ) ^ (1 / 4 : ℝ) →
        Nat.Coprime s B →
        (∀ D ∈ exceptional, ¬ D ∣ B) →
        (X : ℝ) / (2 * (Nat.totient B : ℝ) * Real.log (X : ℝ)) ≤
          ((primesAP X B s).card : ℝ)

/-- A standard consequence of the prime number theorem. This is the
second explicit external input permitted in the conditional project. -/
def PrimeIntervalSupply : Prop :=
  ∃ L₀ : ℕ, ∀ L : ℕ, L₀ ≤ L → 2 ≤ L →
    (L : ℝ) / (3 * Real.log (L : ℝ)) ≤
      (((Finset.Ioo L (2 * L)).filter Nat.Prime).card : ℝ)

end ErdosBorwein