theorem Set.Ico_subset_Ico_of_Icc_subset_Icc {a b c d : ℝ} (h : Icc a b ⊆ Icc c d) : Ico a b ⊆ Ico c d

theorem th43_b (x : ℝ) (hx : 2 ≤ x) : ↑⌊x⌋₊.primeCounting = Chebyshev.theta x / Real.log x + ∫ (t : ℝ) in Set.Icc 2 x, Chebyshev.theta t / (t * Real.log t ^ 2)

theorem finsum_range_eq_sum_range {R : Type u_1} [AddCommMonoid R] {f : ArithmeticFunction R} (x : ℝ) : ∑ᶠ (n : ℕ) (_ : ↑n < x), f n = ∑ n ∈ Finset.range ⌈x⌉₊, f n

theorem finsum_range_eq_sum_range' {R : Type u_1} [AddCommMonoid R] {f : ArithmeticFunction R} (x : ℝ) : ∑ᶠ (n : ℕ) (_ : ↑n ≤ x), f n = ∑ n ≤ ⌊x⌋₊, f n

theorem log2_pos : 0 < Real.log 2

theorem Asymptotics.IsEquivalent.add_isLittleO' {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u v w : α → β} {l : Filter α} (huv : IsEquivalent l u v) (hwu : (w - u) =o[l] v) : IsEquivalent l w v

If u v and w-u = o(v) then w v.

theorem Asymptotics.IsEquivalent.add_isLittleO'' {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u v w : α → β} {l : Filter α} (huv : IsEquivalent l u v) (hwu : (u - w) =o[l] v) : IsEquivalent l w v

If u v and u-w = o(v) then w v.

theorem WeakPNT' : Filter.Tendsto (fun (N : ℕ) => (∑ n ≤ N, ArithmeticFunction.vonMangoldt n) / ↑N) Filter.atTop (nhds 1)

theorem WeakPNT'' : Asymptotics.IsEquivalent Filter.atTop Chebyshev.psi fun (x : ℝ) => x

An alternate form of the Weak PNT.

theorem isLittleO_sqrt_mul_log : (fun (x : ℝ) => √x * Real.log x) =o[Filter.atTop] id

√x · log x = o(x) as x → ∞.

theorem tendsto_floor_add_one_div_self : Filter.Tendsto (fun (x : ℝ) => (↑⌊x⌋₊ + 1) / x) Filter.atTop (nhds 1)

(⌊x⌋₊ + 1) / x → 1 as x → ∞.

theorem isTheta_self_div_const {c : ℝ} (hc : c ≠ 0) : (fun (x : ℝ) => x) =Θ[Filter.atTop] fun (x : ℝ) => x / c

x =Θ x / c for nonzero constant c.

theorem filter_prime_Iic_eq_Icc (n : ℕ) : Finset.filter Nat.Prime (Finset.Iic n) = Finset.filter Nat.Prime (Finset.Icc 1 n)

Filtered sum over Iic n equals filtered sum over Icc 1 n for primes.

theorem Icc_zero_eq_insert (n : ℕ) : Finset.Icc 0 n = insert 0 (Finset.Icc 1 n)

Icc 0 n = insert 0 (Icc 1 n)

theorem chebyshev_asymptotic : Asymptotics.IsEquivalent Filter.atTop Chebyshev.theta id

theorem chebyshev_asymptotic_finsum : Asymptotics.IsEquivalent Filter.atTop (fun (x : ℕ) => ∑ᶠ (p : ℕ) (_ : p ≤ x) (_ : Nat.Prime p), Real.log ↑p) fun (x : ℕ) => ↑x

theorem chebyshev_asymptotic' : ∃ (f : ℝ → ℝ), (∀ ε > 0, f =o[Filter.atTop] fun (t : ℝ) => ε * t) ∧ (∀ (x : ℝ), 2 ≤ x → MeasureTheory.IntegrableOn f (Set.Icc 2 x) MeasureTheory.volume) ∧ ∀ (x : ℝ), Chebyshev.theta x = x + f x

theorem chebyshev_asymptotic'' : ∃ (f : ℝ → ℝ), (∀ ε > 0, f =o[Filter.atTop] fun (x : ℝ) => ε) ∧ (∀ (x : ℝ), 2 ≤ x → MeasureTheory.IntegrableOn f (Set.Icc 2 x) MeasureTheory.volume) ∧ ∀ x > 0, Chebyshev.theta x = x + x * f x

theorem primorial_bounds : ∃ (E : ℝ → ℝ), (E =o[Filter.atTop] fun (x : ℝ) => x) ∧ ∀ (x : ℝ), ↑(∏ p ≤ ⌊x⌋₊ with Nat.Prime p, p) = Real.exp (x + E x)

theorem primorial_bounds_finprod : ∃ (E : ℝ → ℝ), (E =o[Filter.atTop] fun (x : ℝ) => x) ∧ ∀ (x : ℝ), ↑(∏ᶠ (p : ℕ) (_ : ↑p ≤ x) (_ : Nat.Prime p), p) = Real.exp (x + E x)

theorem continuousOn_log0 : ContinuousOn (fun (x : ℝ) => -1 / (x * Real.log x ^ 2)) {0, 1, -1}ᶜ

theorem continuousOn_log1 : ContinuousOn (fun (x : ℝ) => (Real.log x ^ 2)⁻¹ * x⁻¹) {0, 1, -1}ᶜ

theorem integral_log_inv (a b : ℝ) (ha : 2 ≤ a) (hb : a ≤ b) : ∫ (t : ℝ) in a..b, (Real.log t)⁻¹ = (Real.log b)⁻¹ * b - (Real.log a)⁻¹ * a + ∫ (t : ℝ) in a..b, (Real.log t ^ 2)⁻¹

theorem integral_log_inv' (a b : ℝ) (ha : 2 ≤ a) (hb : a ≤ b) : ∫ (t : ℝ) in Set.Icc a b, (Real.log t)⁻¹ = (Real.log b)⁻¹ * b - (Real.log a)⁻¹ * a + ∫ (t : ℝ) in Set.Icc a b, (Real.log t ^ 2)⁻¹

theorem integral_log_inv'' (a b : ℝ) (ha : 2 ≤ a) (hb : a ≤ b) : (Real.log a)⁻¹ * a + ∫ (t : ℝ) in Set.Icc a b, (Real.log t)⁻¹ = (Real.log b)⁻¹ * b + ∫ (t : ℝ) in Set.Icc a b, (Real.log t ^ 2)⁻¹

theorem integral_log_inv_pos (x : ℝ) (hx : 2 < x) : 0 < ∫ (t : ℝ) in Set.Icc 2 x, (Real.log t)⁻¹

theorem integral_log_inv_ne_zero (x : ℝ) (hx : 2 < x) : ∫ (t : ℝ) in Set.Icc 2 x, (Real.log t)⁻¹ ≠ 0

theorem pi_asymp_aux (x : ℝ) (hx : 2 ≤ x) : ↑⌊x⌋₊.primeCounting = (Real.log x)⁻¹ * Chebyshev.theta x + ∫ (t : ℝ) in Set.Icc 2 x, Chebyshev.theta t * (t * Real.log t ^ 2)⁻¹

theorem div_log_sq_isLittleO : (fun (x : ℝ) => x / Real.log x ^ 2) =o[Filter.atTop] fun (x : ℝ) => x / Real.log x

The extra logarithm makes the quadratic-log scale negligible.

theorem integral_log_inv_isEquivalent : Asymptotics.IsEquivalent Filter.atTop (fun (x : ℝ) => ∫ (t : ℝ) in Set.Icc 2 x, 1 / Real.log t) fun (x : ℝ) => x / Real.log x

Integration by parts and the quadratic-log bound give the logarithmic integral's scale.

theorem pi_asymp'' : (fun (x : ℝ) => (↑⌊x⌋₊.primeCounting / ∫ (t : ℝ) in Set.Icc 2 x, 1 / Real.log t) - 1) =o[Filter.atTop] fun (x : ℝ) => 1

theorem pi_asymp : ∃ (c : ℝ → ℝ), (c =o[Filter.atTop] fun (x : ℝ) => 1) ∧ ∀ᶠ (x : ℝ) in Filter.atTop, ↑⌊x⌋₊.primeCounting = (1 + c x) * ∫ (t : ℝ) in 2..x, 1 / Real.log t

theorem inv_div_log_asy : ∃ (c : ℝ), ∀ᶠ (x : ℝ) in Filter.atTop, ∫ (t : ℝ) in Set.Icc 2 x, 1 / Real.log t ^ 2 ≤ c * (x / Real.log x ^ 2)

theorem integral_log_inv_pialt (x : ℝ) (hx : 4 ≤ x) : ∫ (t : ℝ) in Set.Icc 2 x, 1 / Real.log t = x / Real.log x - 2 / Real.log 2 + ∫ (t : ℝ) in Set.Icc 2 x, 1 / Real.log t ^ 2

theorem integral_div_log_asymptotic : ∃ (c : ℝ → ℝ), (c =o[Filter.atTop] fun (x : ℝ) => 1) ∧ ∀ᶠ (x : ℝ) in Filter.atTop, ∫ (t : ℝ) in Set.Icc 2 x, 1 / Real.log t = (1 + c x) * x / Real.log x

theorem pi_alt : ∃ (c : ℝ → ℝ), (c =o[Filter.atTop] fun (x : ℝ) => 1) ∧ ∀ (x : ℝ), ↑⌊x⌋₊.primeCounting = (1 + c x) * x / Real.log x

theorem pi_alt' : Asymptotics.IsEquivalent Filter.atTop (fun (x : ℝ) => ↑⌊x⌋₊.primeCounting) fun (x : ℝ) => x / Real.log x

theorem pi_nth_prime (n : ℕ) : (nth_prime n).primeCounting = n + 1

theorem tendsto_nth_prime_atTop : Filter.Tendsto nth_prime Filter.atTop Filter.atTop

theorem pi_nth_prime_asymp : Asymptotics.IsEquivalent Filter.atTop (fun (n : ℕ) => ↑(nth_prime n) / Real.log ↑(nth_prime n)) fun (n : ℕ) => ↑n

theorem log_nth_prime_asymp : Asymptotics.IsEquivalent Filter.atTop (fun (n : ℕ) => Real.log ↑(nth_prime n)) fun (n : ℕ) => Real.log ↑n

theorem nth_prime_asymp : Asymptotics.IsEquivalent Filter.atTop (fun (n : ℕ) => ↑(nth_prime n)) fun (n : ℕ) => ↑n * Real.log ↑n

theorem pn_asymptotic : ∃ (c : ℕ → ℝ), (c =o[Filter.atTop] fun (x : ℕ) => 1) ∧ ∀ n > 1, ↑(nth_prime n) = (1 + c n) * ↑n * Real.log ↑n

theorem pn_pn_plus_one : ∃ (c : ℕ → ℝ), (c =o[Filter.atTop] fun (x : ℕ) => 1) ∧ ∀ (n : ℕ), ↑(nth_prime (n + 1)) - ↑(nth_prime n) = c n * ↑(nth_prime n)

theorem prime_in_gap' (a b : ℕ) (h : a.primeCounting < b.primeCounting) : ∃ (p : ℕ), Nat.Prime p ∧ a + 1 ≤ p ∧ p < b + 1

theorem prime_in_gap (a b : ℝ) (ha : 0 < a) (h : ⌊a⌋₊.primeCounting < ⌊b⌋₊.primeCounting) : ∃ (p : ℕ), Nat.Prime p ∧ a < ↑p ∧ ↑p ≤ b

theorem bound_f_second_term (f : ℝ → ℝ) (hf : Filter.Tendsto f Filter.atTop (nhds 0)) (δ : ℝ) (hδ : δ > 0) : ∀ᶠ (x : ℝ) in Filter.atTop, 1 + f x < 1 + δ

theorem bound_f_first_term {ε : ℝ} (hε : 0 < ε) (f : ℝ → ℝ) (hf : Filter.Tendsto f Filter.atTop (nhds 0)) (δ : ℝ) (hδ : δ > 0) : ∀ᶠ (x : ℝ) in Filter.atTop, 1 + f ((1 + ε) * x) > 1 - δ

theorem smaller_terms {ε : ℝ} (hε : 0 < ε) (f : ℝ → ℝ) (hf : Filter.Tendsto f Filter.atTop (nhds 0)) (δ : ℝ) (hδ : δ > 0) : ∀ᶠ (x : ℝ) in Filter.atTop, (1 - δ) * ((1 + ε) * x / Real.log ((1 + ε) * x)) < (1 + f ((1 + ε) * x)) * ((1 + ε) * x / Real.log ((1 + ε) * x))

theorem second_smaller_terms (f : ℝ → ℝ) (hf : Filter.Tendsto f Filter.atTop (nhds 0)) (δ : ℝ) (hδ : δ > 0) : ∀ᶠ (x : ℝ) in Filter.atTop, (1 + δ) * (x / Real.log x) > (1 + f x) * (x / Real.log x)

theorem x_log_x_atTop : Filter.Tendsto (fun (x : ℝ) => x / Real.log x) Filter.atTop Filter.atTop

theorem tendsto_by_squeeze (ε : ℝ) (hε : ε > 0) : Filter.Tendsto (fun (x : ℝ) => ↑⌊(1 + ε) * x⌋₊.primeCounting - ↑⌊x⌋₊.primeCounting) Filter.atTop Filter.atTop

theorem prime_between {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (x : ℝ) in Filter.atTop, ∃ (p : ℕ), Nat.Prime p ∧ x < ↑p ∧ ↑p < (1 + ε) * x

theorem sum_mobius_div_self_le (N : ℕ) : |∑ n ∈ Finset.range N, ↑(ArithmeticFunction.moebius n) / ↑n| ≤ 1

theorem sum_mobius_mul_floor (x : ℝ) (hx : 1 ≤ x) : ∑ n ≤ ⌊x⌋₊, ↑(ArithmeticFunction.moebius n) * ↑⌊x / ↑n⌋ = 1

noncomputable def mu_log : ArithmeticFunction ℝ

Equations

• mu_log = { toFun := fun (n : ℕ) => ↑(ArithmeticFunction.moebius n) * ArithmeticFunction.log n, map_zero' := mu_log._proof_1 }

theorem mu_log_apply (n : ℕ) : mu_log n = ↑(ArithmeticFunction.moebius n) * ArithmeticFunction.log n

theorem mu_log_mul_zeta : mu_log * ↑ArithmeticFunction.zeta = -ArithmeticFunction.vonMangoldt

theorem mu_log_eq_mu_mul_neg_lambda : mu_log = ↑ArithmeticFunction.moebius * -ArithmeticFunction.vonMangoldt

theorem sum_mu_Lambda (x : ℝ) : ∑ n ≤ ⌊x⌋₊, ↑(ArithmeticFunction.moebius n) * Real.log ↑n = -∑ k ≤ ⌊x⌋₊, ↑(ArithmeticFunction.moebius k) * Psi (x / ↑k)

theorem M_log_identity (x : ℝ) (hx : 1 ≤ x) : M x * Real.log x = ∑ k ≤ ⌊x⌋₊, ↑(ArithmeticFunction.moebius k) * (Real.log (x / ↑k) - Psi (x / ↑k))

noncomputable def R (x : ℝ) : ℝ

Equations

• R x = Psi x - x

theorem R_isLittleO : R =o[Filter.atTop] id

theorem sum_mobius_div_isBigO : (fun (x : ℝ) => ∑ k ≤ ⌊x⌋₊, ↑(ArithmeticFunction.moebius k) * (x / ↑k)) =O[Filter.atTop] id

theorem sum_log_div_isBigO : (fun (x : ℝ) => ∑ k ≤ ⌊x⌋₊, Real.log (x / ↑k)) =O[Filter.atTop] id

theorem R_locally_bounded (K : ℝ) (hK : 0 ≤ K) : ∃ (C : ℝ), ∀ y ∈ Set.Icc 0 K, |R y| ≤ C

theorem sum_bounded_of_linear_bound {f : ℝ → ℝ} {ε C : ℝ} (hε : 0 ≤ ε) (hC : 0 ≤ C) (h : ∀ (y : ℝ), 1 ≤ y → |f y| ≤ ε * y + C) (x : ℝ) (hx : 1 ≤ x) : ∑ k ∈ Finset.Icc 1 ⌊x⌋₊, |f (x / ↑k)| ≤ ε * x * (Real.log x + 1) + C * x

theorem sum_abs_R_isLittleO : (fun (x : ℝ) => ∑ k ≤ ⌊x⌋₊, |R (x / ↑k)|) =o[Filter.atTop] fun (x : ℝ) => x * Real.log x

theorem R_linear_bound (ε : ℝ) (hε : 0 < ε) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (y : ℝ), 1 ≤ y → |R y| ≤ ε * y + C

theorem sum_abs_R_isLittleO' : (fun (x : ℝ) => ∑ k ≤ ⌊x⌋₊, |R (x / ↑k)|) =o[Filter.atTop] fun (x : ℝ) => x * Real.log x

theorem M_isLittleO : M =o[Filter.atTop] id

theorem M_isLittleO' : M =o[Filter.atTop] id

theorem mu_pnt : (fun (x : ℝ) => ∑ n ∈ Finset.range ⌊x⌋₊, ArithmeticFunction.moebius n) =o[Filter.atTop] fun (x : ℝ) => x

theorem lambda_eq_sum_sq_dvd_mu (n : ℕ) (hn : n ≠ 0) : (-1) ^ ArithmeticFunction.cardFactors n = ∑ d ∈ Finset.Icc 1 n with d ^ 2 ∣ n, ↑(ArithmeticFunction.moebius (n / d ^ 2))

theorem sum_lambda_eq_sum_mu_div_sq (N : ℕ) : ∑ n ∈ Finset.Icc 1 N, (-1) ^ ArithmeticFunction.cardFactors n = ∑ d ∈ Finset.Icc 1 N.sqrt, ∑ k ∈ Finset.Icc 1 (N / d ^ 2), ↑(ArithmeticFunction.moebius k)

theorem sum_mu_div_sq_isLittleO : (fun (N : ℕ) => ∑ d ∈ Finset.Icc 1 N.sqrt, ∑ k ∈ Finset.Icc 1 (N / d ^ 2), ↑(ArithmeticFunction.moebius k)) =o[Filter.atTop] fun (N : ℕ) => ↑N

theorem lambda_pnt : (fun (x : ℝ) => ∑ n ∈ Finset.range ⌊x⌋₊, (-1) ^ ArithmeticFunction.cardFactors n) =o[Filter.atTop] fun (x : ℝ) => x

theorem sum_mobius_floor (x : ℝ) (hx : 1 ≤ x) : ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, ↑(ArithmeticFunction.moebius n) * ↑⌊x / ↑n⌋ = 1

theorem sum_mobius_floor_tail_isLittleO (K : ℕ) (hK : 0 < K) : (fun (x : ℝ) => ∑ n ∈ Finset.Ioc ⌊x / ↑K⌋₊ ⌊x⌋₊, ↑(ArithmeticFunction.moebius n) * ↑⌊x / ↑n⌋) =o[Filter.atTop] fun (x : ℝ) => x

theorem sum_mobius_div_approx (x : ℝ) (K : ℕ) (hK : 0 < K) (hx : 1 ≤ x) : |x * ∑ n ∈ Finset.Icc 1 ⌊x / ↑K⌋₊, ↑(ArithmeticFunction.moebius n) / ↑n - 1| ≤ x / ↑K + |∑ n ∈ Finset.Ioc ⌊x / ↑K⌋₊ ⌊x⌋₊, ↑(ArithmeticFunction.moebius n) * ↑⌊x / ↑n⌋|

theorem mu_pnt_alt : (fun (x : ℝ) => ∑ n ∈ Finset.range ⌊x⌋₊, ↑(ArithmeticFunction.moebius n) / ↑n) =o[Filter.atTop] fun (x : ℝ) => 1

theorem chebyshev_asymptotic_pnt {q a : ℕ} (hq : q ≥ 1) (ha : a.Coprime q) (ha' : a < q) : Asymptotics.IsEquivalent Filter.atTop (fun (x : ℝ) => ∑ p ≤ ⌊x⌋₊ with Nat.Prime p, if p % q = a then Real.log ↑p else 0) fun (x : ℝ) => x / ↑q.totient

theorem dirichlet_thm {q a : ℕ} (hq : q ≥ 1) (ha : a.Coprime q) (ha' : a < q) : Infinite { p : ℕ // Nat.Prime p ∧ p % q = a }