Coprime prime mass on fixed half-open intervals; endpoints precede the limit.

noncomputable def MathlibNt.SieveTheory.LiuWeight.primeLogIntervalPrimes (N : ℕ) (a b : ℝ) : Finset ℕ

Equations

• MathlibNt.SieveTheory.LiuWeight.primeLogIntervalPrimes N a b = {p ∈ Finset.range (MathlibNt.SieveTheory.PrimeReciprocalLogScale.rpowFloor N b + 1) | Nat.Prime p ∧ ↑N ^ a < ↑p ∧ ↑p ≤ ↑N ^ b}

theorem MathlibNt.SieveTheory.LiuWeight.mem_primeLogIntervalPrimes {N p : ℕ} {a b : ℝ} : p ∈ primeLogIntervalPrimes N a b ↔ Nat.Prime p ∧ ↑N ^ a < ↑p ∧ ↑p ≤ ↑N ^ b

noncomputable def MathlibNt.SieveTheory.LiuWeight.coprimePrimeLogIntervalPrimes (N : ℕ) (a b : ℝ) : Finset ℕ

Equations

• MathlibNt.SieveTheory.LiuWeight.coprimePrimeLogIntervalPrimes N a b = {p ∈ MathlibNt.SieveTheory.LiuWeight.primeLogIntervalPrimes N a b | ¬p ∣ N}

noncomputable def MathlibNt.SieveTheory.LiuWeight.coprimePrimeReciprocalLogInterval (N : ℕ) (a b : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiuWeight.coprimePrimeReciprocalLogInterval N a b = ∑ p ∈ MathlibNt.SieveTheory.LiuWeight.coprimePrimeLogIntervalPrimes N a b, 1 / ↑p

noncomputable def MathlibNt.SieveTheory.LiuWeight.badPrimeReciprocalLogInterval (N : ℕ) (a b : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiuWeight.badPrimeReciprocalLogInterval N a b = ∑ p ∈ MathlibNt.SieveTheory.LiuWeight.primeLogIntervalPrimes N a b with p ∣ N, 1 / ↑p

theorem MathlibNt.SieveTheory.LiuWeight.coprimePrimeReciprocalLogInterval_eq_sub (N : ℕ) (a b : ℝ) : coprimePrimeReciprocalLogInterval N a b = PrimeReciprocalLogScale.primeReciprocalLogInterval N a b - badPrimeReciprocalLogInterval N a b

theorem MathlibNt.SieveTheory.LiuWeight.badPrimeReciprocalLogInterval_nonneg (N : ℕ) (a b : ℝ) : 0 ≤ badPrimeReciprocalLogInterval N a b

theorem MathlibNt.SieveTheory.LiuWeight.badPrimeReciprocalLogInterval_le {N : ℕ} (hN : 2 ≤ N) (a b : ℝ) : badPrimeReciprocalLogInterval N a b ≤ Real.log ↑N / (Real.log 2 * ↑N ^ a)

theorem MathlibNt.SieveTheory.LiuWeight.tendsto_coprimePrimeLossBound {a : ℝ} (ha : 0 < a) : Filter.Tendsto (fun (N : ℕ) => Real.log ↑N / (Real.log 2 * ↑N ^ a)) Filter.atTop (nhds 0)

theorem MathlibNt.SieveTheory.LiuWeight.tendsto_badPrimeReciprocalLogInterval {a : ℝ} (ha : 0 < a) (b : ℝ) : Filter.Tendsto (fun (N : ℕ) => badPrimeReciprocalLogInterval N a b) Filter.atTop (nhds 0)

theorem MathlibNt.SieveTheory.LiuWeight.tendsto_coprimePrimeReciprocalLogInterval {a b : ℝ} (ha : 0 < a) (hab : a < b) : Filter.Tendsto (fun (N : ℕ) => coprimePrimeReciprocalLogInterval N a b) Filter.atTop (nhds (Real.log (b / a)))