Preliminaries

Decomposing the von Mangoldt function into type I and type II functions.

noncomputable def Delta {R : Type u_1} [Field R] (f : ℕ → R) (x : ℝ) (q : ℕ) (a : ZMod q) : R

Equations

• Δ_[f](x; q, a) = summatory ((Nat.modEqs a).indicator f) x - (↑q.totient)⁻¹ * summatory (onCoprime q f) x

theorem DirichletCharacter.inv_zmod_apply {q : ℕ} {a : ZMod q} (ha : IsUnit a) (χ : DirichletCharacter ℂ q) : χ⁻¹ a = χ a⁻¹

theorem DirichletCharacter.starRingEnd_apply {q : ℕ} {a : ZMod q} (ha : IsUnit a) (χ : DirichletCharacter ℂ q) : (starRingEnd ℂ) (χ a) = χ⁻¹ a

theorem DirichletCharacter.one_natCast_apply {q : ℕ} [NeZero q] (n : ℕ) : 1 ↑n = if q.Coprime n then 1 else 0

def «termΔ_[_](_;_,_)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem isLocallyBounded_Delta {R : Type u_1} [NormedField R] (f : ℕ → R) (q : ℕ) (a : ZMod q) : IsLocallyBounded fun (x : ℝ) => Δ_[f](x; q, a)

theorem isLocallyBoundedOn_Delta {R : Type u_1} [NormedField R] {s : Set ℝ} (f : ℕ → R) (q : ℕ) (a : ZMod q) : IsLocallyBoundedOn (fun (x : ℝ) => Δ_[f](x; q, a)) s

theorem aeStronglyMeasurable_Delta {R : Type u_1} [NormedField R] [MeasurableSpace R] (f : ℕ → R) (q : ℕ) (a : ZMod q) : MeasureTheory.AEStronglyMeasurable (fun (x : ℝ) => Δ_[f](x; q, a)) MeasureTheory.volume

theorem Complex.ofReal_setIndicator {ι : Type u_1} {s : Set ι} (f : ι → ℝ) (n : ι) : ↑(s.indicator (fun (n : ι) => f n) n) = s.indicator (fun (n : ι) => ↑(f n)) n

theorem Complex.ofReal_onCoprime {f : ℕ → ℝ} (r n : ℕ) : ↑(onCoprime r (fun (n : ℕ) => f n) n) = onCoprime r (fun (n : ℕ) => ↑(f n)) n

theorem Complex.ofReal_summatory {g : ℕ → ℝ} {x : ℝ} : ↑(summatory (fun (n : ℕ) => g n) x) = summatory (fun (n : ℕ) => ↑(g n)) x

theorem Complex.ofReal_Delta {g : ℕ → ℝ} {x : ℝ} {q : ℕ} {a : ZMod q} : ↑Δ_[fun (n : ℕ) => g n](x; q, a) = Δ_[fun (n : ℕ) => ↑(g n)](x; q, a)

theorem Complex.ofReal_integral {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {f : X → ℝ} : ↑(∫ (x : X), f x ∂μ) = ∫ (x : X), ↑(f x) ∂μ

theorem Delta_eq_sum_char {𝕜 : Type u_1} [Field 𝕜] [Algebra 𝕜 ℂ] {f : ℕ → 𝕜} {y : ℝ} {q : ℕ} [NeZero q] {a : ZMod q} (ha : IsUnit a) : (algebraMap 𝕜 ℂ) Δ_[f](y; q, a) = (↑q.totient)⁻¹ * ∑ χ : DirichletCharacter ℂ q, if χ ≠ 1 then star (χ a) * summatory (fun (n : ℕ) => (algebraMap 𝕜 ℂ) (f n) * χ ↑n) y else 0

theorem Delta_Lambda_eq (x : ℝ) (q : ℕ) (a : ZMod q) : Δ_[⇑ArithmeticFunction.vonMangoldt](x; q, a) = chebyPsi x a - (↑q.totient)⁻¹ * ∑ n ∈ Nat.Icc 1 x with q.Coprime n, ArithmeticFunction.vonMangoldt n

noncomputable def C_D1 (A : ℕ) : ℝ

Equations

• C_D1 A = C_SW A 0

theorem PNT [ProofData] (A : ℕ) : |summatory (fun (n : ℕ) => ArithmeticFunction.vonMangoldt n) ProofData.x - ProofData.x| ≤ C_D1 A * (ProofData.x / Real.log ProofData.x ^ A)

theorem vonMangoldt_eq_ite_vonMangoldt (n : ℕ) : ArithmeticFunction.vonMangoldt n = if IsPrimePow n then ArithmeticFunction.vonMangoldt n else 0

theorem ArithmeticFunction.mul_coe_zeta_apply (f : ArithmeticFunction ℝ) (n : ℕ) : (f * ↑zeta) n = ∑ d ∈ n.divisors, f d

theorem sum_vonMangoldt_le_log [ProofData] {k : ℕ} (hk : 0 < k) {q : ℕ} (hq : 0 < q) : |∑ p ∈ Finset.Ioc 0 ⌊ProofData.x ^ (1 / ↑k)⌋₊ with Nat.Prime p, if ¬q.Coprime (p ^ k) then ArithmeticFunction.vonMangoldt p else 0| ≤ ArithmeticFunction.log q

theorem sum_PrimePow_eq_sum_sum_of_eq_zero {R : Type u_1} [AddCommMonoid R] (f : ℕ → R) {x : ℝ} (hx : 0 ≤ x) (hf : ∀ (n : ℕ), 0 < n → ↑n ≤ x → ¬IsPrimePow n → f n = 0) : ∑ n ∈ Finset.Ioc 0 ⌊x⌋₊, f n = ∑ k ∈ Finset.Icc 1 ⌊Real.log x / Real.log 2⌋₊, ∑ p ∈ Finset.Ioc 0 ⌊x ^ (1 / ↑k)⌋₊ with Nat.Prime p, f (p ^ k)

theorem C_SVNC_le : C_SVNC✝ ≤ (Real.log 2)⁻¹

theorem sum_vonMangoldt_not_coprime_ll_logq [ProofData] {q : ℕ} (hq : 0 < q) : |summatory (fun (n : ℕ) => if ¬q.Coprime n then ArithmeticFunction.vonMangoldt n else 0) ProofData.x| ≤ C_SVNC✝ * (Real.log ↑q * Real.log ProofData.x)

theorem summatory_sub_ite {P : ℕ → Prop} [DecidablePred P] (f : ℕ → ℝ) {x : ℝ} : summatory f x - summatory (fun (n : ℕ) => if P n then f n else 0) x = summatory (fun (x : ℕ) => if ¬P x then f x else 0) x

theorem sum_primes_not_dvd_log_eq_id [ProofData] (A : ℕ) {q : ℕ} (hq : 0 < q) : |summatory (fun (n : ℕ) => if q.Coprime n then ArithmeticFunction.vonMangoldt n else 0) ProofData.x - ProofData.x| ≤ C_D1 A * (ProofData.x / Real.log ProofData.x ^ A) + C_SVNC✝ * (Real.log ↑q * Real.log ProofData.x)

noncomputable def ArithmeticFunction.twist {𝕜 : Type u_1} [Field 𝕜] [Algebra 𝕜 ℂ] {q : ℕ} (f : ArithmeticFunction 𝕜) (c : DirichletCharacter ℂ q) : ArithmeticFunction ℂ

Equations

• f.twist c = { toFun := fun (n : ℕ) => (algebraMap 𝕜 ℂ) (f n) * c ↑n, map_zero' := ⋯ }

@[simp]

theorem ArithmeticFunction.twist_apply {𝕜 : Type u_1} [Field 𝕜] [Algebra 𝕜 ℂ] {q : ℕ} {f : ArithmeticFunction 𝕜} {χ : DirichletCharacter ℂ q} {n : ℕ} : (f.twist χ) n = (algebraMap 𝕜 ℂ) (f n) * χ ↑n

theorem ArithmeticFunction.mul_twist {𝕜 : Type u_1} [Field 𝕜] [Algebra 𝕜 ℂ] {q : ℕ} (f g : ArithmeticFunction 𝕜) (χ : DirichletCharacter ℂ q) (n : ℕ) : ((f * g).twist χ) n = (f.twist χ * g.twist χ) n

theorem ArithmeticFunction.summatory_mul_eq_summatory {R : Type u_1} [Semiring R] (f g : ArithmeticFunction R) (x : ℝ) : summatory (⇑(f * g)) x = summatory (fun (n : ℕ) => f n * summatory (⇑g) (x / ↑n)) x

theorem Finset.sum_summatory_comm {ι : Type u_1} {R : Type u_2} [DecidableEq ι] {s : Finset ι} [AddCommMonoid R] (f : ι → ℕ → R) {x : ℝ} : ∑ i ∈ s, summatory (f i) x = summatory (fun (n : ℕ) => ∑ i ∈ s, f i n) x

theorem Finset.summatory_sum_comm {ι : Type u_1} {R : Type u_2} [DecidableEq ι] {s : Finset ι} [AddCommMonoid R] (f : ι → ℕ → R) {x : ℝ} : summatory (fun (n : ℕ) => ∑ i ∈ s, f i n) x = ∑ i ∈ s, summatory (f i) x

theorem ZMod.isUnit_inv' {q : ℕ} (n : ZMod q) : IsUnit n → IsUnit n⁻¹

theorem Delta_convolution_eq {𝕜 : Type u_1} [Field 𝕜] [Algebra 𝕜 ℂ] {y : ℝ} {q : ℕ} [NeZero q] {a : ZMod q} (ha : IsUnit a) (f g : ArithmeticFunction 𝕜) : Δ_[⇑(f * g)](y; q, a) = summatory (fun (k : ℕ) => if k.Coprime q then f k * Δ_[⇑g](y / ↑k; q, a * (↑k)⁻¹) else 0) y

Periodic function lemmas for Delta_one_bound

theorem Function.Periodic.add_period_apply {α : Type u_1} {β : Type u_2} [Add α] {f : α → β} {c : α} (hf : Periodic f c) (a : α) : f (a + c) = f a

theorem Function.Periodic.period_add_apply {α : Type u_1} {β : Type u_2} [AddCommMonoid α] {f : α → β} {c : α} (hf : Periodic f c) (a : α) : f (c + a) = f a

theorem summatory_eq_sum_range {R : Type u_1} [AddCommMonoid R] {f : ℕ → R} {x : ℝ} : summatory f x = ∑ n ∈ Finset.range ⌊x⌋₊, f (n + 1)

Rewrite summatory as a sum over Finset.range with a shift.

theorem sum_range_periodic {R : Type u_1} [AddCommMonoid R] [Module ℕ R] {f : ℕ → R} {q : ℕ} (hf : Function.Periodic f q) (k : ℕ) : ∑ n ∈ Finset.range (k * q), f n = k • ∑ n ∈ Finset.range q, f n

Sum of a periodic function over k full periods.

theorem sum_range_periodic_mod {R : Type u_1} [AddCommMonoid R] [Module ℕ R] {f : ℕ → R} {q : ℕ} (hf : Function.Periodic f q) (N : ℕ) : ∑ n ∈ Finset.range N, f n = (N / q) • ∑ n ∈ Finset.range q, f n + ∑ n ∈ Finset.range (N % q), f n

Sum of a periodic function splits into full periods plus a remainder.

theorem indicator_modEqs_periodic {q : ℕ} (a : ZMod q) (c : ℝ) : Function.Periodic ((Nat.modEqs a).indicator fun (x : ℕ) => c) q

The modular residue indicator of a constant function is periodic with period q.

theorem onCoprime_periodic (q : ℕ) (c : ℝ) : Function.Periodic (onCoprime q fun (x : ℕ) => c) q

The coprimality indicator of a constant function is periodic with period q.

theorem sum_range_indicator_modEqs {q : ℕ} [NeZero q] {a : ZMod q} : ∑ n ∈ Finset.range q, (Nat.modEqs a).indicator (fun (x : ℕ) => 1) n = 1

In one full period {0, …, q-1}, the indicator of n ≡ a (mod q) sums to 1, when a is a unit.

theorem sum_range_of_periodic_full_eq_add {R : Type u_1} [AddCommMonoid R] {a q : ℕ} (f : ℕ → R) (hf : Function.Periodic f q) : ∑ i ∈ Finset.range q, f i = ∑ i ∈ Finset.range q, f (i + a)

theorem sum_range_indicator_modEqs_add_one {q : ℕ} [hq : NeZero q] {a : ZMod q} : ∑ n ∈ Finset.range q, (Nat.modEqs a).indicator (fun (x : ℕ) => 1) (n + 1) = 1

In one full period {1, …, q}, the indicator of n ≡ a (mod q) sums to 1, when a is a unit.

theorem sum_range_onCoprime_zeta {q : ℕ} : ∑ n ∈ Finset.range q, onCoprime q (fun (x : ℕ) => 1) n = ↑q.totient

In one full period {0, …, q-1}, the coprime indicator sums to φ(q).

theorem sum_range_onCoprime_zeta_add_one {q : ℕ} : ∑ n ∈ Finset.range q, onCoprime q (fun (x : ℕ) => 1) (n + 1) = ↑q.totient

In one full period {1, …, q}, the coprime indicator sums to φ(q).

theorem apply_mem_range_iff_mem_range_comp {α : Type u_1} {β : Type u_2} {f : α → β} [AddCommGroup β] (a b : β) : a + b ∈ Set.range f ↔ a ∈ Set.range fun (n : α) => f n - b

theorem sum_range_modEq {q : ℕ} {a : ZMod q} [hq : NeZero q] (n : ℕ) : ∃ (c : ℝ), 0 ≤ c ∧ c ≤ 1 ∧ ∑ m ∈ Finset.range n, (Nat.modEqs a).indicator (fun (x : ℕ) => 1) (m + 1) = ↑(n / q) + c

theorem sum_range_onCoprime {q : ℕ} (n : ℕ) : ∑ m ∈ Finset.range n, onCoprime q (fun (x : ℕ) => 1) (m + 1) = ↑q.totient * ↑(n / q) + ∑ m ∈ Finset.range (n % q), onCoprime q (fun (x : ℕ) => 1) (m + 1)

theorem summatory_zeta_eq {x : ℝ} : summatory (⇑↑ArithmeticFunction.zeta) x = summatory (fun (x : ℕ) => 1) x

theorem Set.indicator_apply_congr {α : Type u_1} {β : Type u_2} [Zero β] (r s : Set α) (f g : α → β) (a b : α) (hab : a = b) (hrs : r = s) (hfg : ∀ (n : α), n = a → f n = g n) : r.indicator f a = s.indicator g b

theorem Delta_zeta_eq_Delta_one {x : ℝ} {q : ℕ} (a : ZMod q) : Δ_[⇑↑ArithmeticFunction.zeta](x; q, a) = Δ_[fun (x : ℕ) => 1](x; q, a)

theorem Delta_one_bound {x : ℝ} {q : ℕ} (a : ZMod q) (hq : 0 < q) : ‖Δ_[fun (x : ℕ) => 1](x; q, a)‖ ≤ 1

theorem abel_summation_summatory {𝕜 : Type u_1} [RCLike 𝕜] (c : ℕ → 𝕜) {f f' : ℝ → 𝕜} {a b : ℝ} (hac : ∀ (n : ℕ), 0 < n → ↑n ≤ a → c n * f ↑n = 0) (ha : 0 ≤ a) (hab : a ≤ b) (hf_diff : ∀ t ∈ Set.Icc a b, HasDerivAt f (f' t) t) (hf_int : MeasureTheory.LocallyIntegrableOn f' (Set.Icc a b) MeasureTheory.volume) : summatory (fun (k : ℕ) => f ↑k * c k) b = f b * summatory c b - f a * summatory c a - ∫ (t : ℝ) in Set.Ioc a b, f' t * summatory c t

Abel summation stated interms of summatory.

theorem Delta_abel_summation {q : ℕ} [hq : NeZero q] {a : ZMod q} (ha : IsUnit a) (g g' : ℝ → ℂ) {x : ℝ} (hx : 1 ≤ x) (hg : ∀ t ∈ Set.Icc 1 x, HasDerivAt g (g' t) t) (hg_int : MeasureTheory.LocallyIntegrableOn g' (Set.Icc 1 x) MeasureTheory.volume) (hg_one : g 1 = 0) : Δ_[fun (n : ℕ) => g ↑n](x; q, a) = Δ_[fun (x : ℕ) => 1](x; q, a) * g x - ∫ (t : ℝ) in Set.Ioc 1 x, Δ_[fun (x : ℕ) => 1](t; q, a) * g' t

theorem Delta_abel_summation_real {q : ℕ} [hq : NeZero q] {a : ZMod q} (ha : IsUnit a) (g g' : ℝ → ℝ) {x : ℝ} (hx : 1 ≤ x) (hg : ∀ t ∈ Set.Icc 1 x, HasDerivAt g (g' t) t) (hg_int : MeasureTheory.LocallyIntegrableOn g' (Set.Icc 1 x) MeasureTheory.volume) (hg_one : g 1 = 0) : Δ_[fun (n : ℕ) => g ↑n](x; q, a) = Δ_[fun (x : ℕ) => 1](x; q, a) * g x - ∫ (t : ℝ) in Set.Ioc 1 x, Δ_[fun (x : ℕ) => 1](t; q, a) * g' t

theorem Complex.ofReal_lipschitzWith : LipschitzWith 1 ofReal

theorem Complex.ofReal_antilipschitzWith : AntilipschitzWith 1 ofReal

theorem Delta_monotone_bound_aux {q : ℕ} [hq : NeZero q] {a : ZMod q} (ha : IsUnit a) (g g' : ℝ → ℝ) {x : ℝ} (hx : 1 ≤ x) (hg : ∀ t ∈ Set.Icc 1 x, HasDerivAt g (g' t) t) (hg_int : MeasureTheory.LocallyIntegrableOn g' (Set.Icc 1 x) MeasureTheory.volume) (hg_mono : MonotoneOn g (Set.Icc 1 x)) (hg_one : g 1 = 0) : ‖Δ_[fun (n : ℕ) => g ↑n](x; q, a)‖ ≤ 2 * g x

theorem Delta_monotone_bound {q : ℕ} [hq : NeZero q] {a : ZMod q} (ha : IsUnit a) (g : ℝ → ℝ) {x : ℝ} (hx : 1 ≤ x) (hg : ∀ t ∈ Set.Icc 1 x, DifferentiableAt ℝ g t) (hg_int : MeasureTheory.LocallyIntegrableOn (deriv g) (Set.Icc 1 x) MeasureTheory.volume) (hg_mono : MonotoneOn g (Set.Icc 1 x)) (hg1 : g 1 = 0) : ‖Δ_[fun (n : ℕ) => g ↑n](x; q, a)‖ ≤ 2 * g x

theorem Delta_flog_bound {v : ℕ} {f : ArithmeticFunction ℝ} {x : ℝ} (hx : 2 ≤ x) {q : ℕ} [NeZero q] (a : ZMod q) (ha : IsUnit a) : ‖Δ_[⇑(f * ArithmeticFunction.log.ppow v)](x; q, a)‖ ≤ 2 * Real.log x ^ v * summatory (fun (k : ℕ) => |f k|) x