def Nat.modEqs {q : ℕ} (a : ZMod q) : Set ℕ

Equations

• Nat.modEqs a = {n : ℕ | ↑n = a}

@[simp]

theorem Nat.modEqs_one_one : modEqs 1 = Set.univ

@[simp]

theorem Nat.mem_modEqs {q : ℕ} (a : ZMod q) (n : ℕ) : n ∈ modEqs a ↔ ↑n = a

theorem chebyPsi_eq_summatory (x : ℝ) {q : ℕ} (a : ZMod q) : chebyPsi x a = summatory ((Nat.modEqs a).indicator ⇑ArithmeticFunction.vonMangoldt) x

def BV.termψ : Lean.ParserDescr

Equations

• BV.termψ = Lean.ParserDescr.node `BV.termψ 1024 (Lean.ParserDescr.symbol "ψ")

theorem summatory_vonMangoldt {x : ℝ} : summatory (fun (n : ℕ) => ArithmeticFunction.vonMangoldt n) x = Chebyshev.psi x

theorem ψ_one_one {x : ℝ} : chebyPsi x 1 = Chebyshev.psi x

def onCoprime {R : Type u_1} [Zero R] (r : ℕ) (f : ℕ → R) (n : ℕ) : R

Equations

• onCoprime r f n = if r.Coprime n then f n else 0

theorem onCoprime_apply {R : Type u_1} [Zero R] (r : ℕ) (f : ℕ → R) (n : ℕ) : onCoprime r f n = if r.Coprime n then f n else 0

theorem onCoprime_congr {R : Type u_1} [Zero R] (r s : ℕ) (f g : ℕ → R) (n m : ℕ) (hrs : r = s) (hfg : ∀ (x : ℕ), x = n → r.Coprime x → f x = g x) (hnm : n = m) : onCoprime r f n = onCoprime s g m

theorem onCoprime_nonneg {R : Type u_1} [Zero R] [Preorder R] {r : ℕ} {f : ℕ → R} {n : ℕ} (hf : 0 ≤ f n) : 0 ≤ onCoprime r f n

def onCoprime_positivity : Mathlib.Meta.Positivity.PositivityExt

Equations

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

theorem onCoprime_le_of_nonneg {R : Type u_1} [Zero R] [Preorder R] {r : ℕ} {f : ℕ → R} {n : ℕ} (hf : 0 ≤ f n) : onCoprime r f n ≤ f n

class ProofData : Type

• U : ℝ
• V : ℝ
• x : ℝ
• le_x : 2 ≤ x
• UV_le : U * V ≤ √x
• le_U : Real.exp √(Real.log x) ≤ U
• le_V : Real.exp √(Real.log x) ≤ V

theorem ProofData.x_pos [data : ProofData] : 0 < x

theorem ProofData.U_pos [data : ProofData] : 0 < U

theorem ProofData.U_nonneg [data : ProofData] : 0 ≤ U

theorem ProofData.one_le_U [data : ProofData] : 1 ≤ U

theorem ProofData.V_pos [data : ProofData] : 0 < V

theorem ProofData.V_nonneg [data : ProofData] : 0 ≤ V

theorem ProofData.one_le_V [data : ProofData] : 1 ≤ V

theorem ProofData.x_nonneg [data : ProofData] : 0 ≤ x

theorem ProofData.U_le_sqrt_x [data : ProofData] : U ≤ √x

theorem ProofData.U_le_x [data : ProofData] : U ≤ x

def U_positivity : Mathlib.Meta.Positivity.PositivityExt

Equations

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

def V_positivity : Mathlib.Meta.Positivity.PositivityExt

Equations

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

theorem log_x_pos [data : ProofData] : 0 < Real.log ProofData.x

def x_positivity : Mathlib.Meta.Positivity.PositivityExt

Equations

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

def log_x_positivity : Mathlib.Meta.Positivity.PositivityExt

Equations

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

theorem Nat.Icc_sqrt_nonempty [data : ProofData] : (Icc (√ProofData.x) ProofData.x).Nonempty

noncomputable def maxy [data : ProofData] (f : ℝ → ℝ) : ℝ

Equations

• maxy f = ⨆ y ∈ Set.Icc (√ProofData.x) ProofData.x, f y

theorem maxy_le [data : ProofData] {f : ℝ → ℝ} {M : ℝ} (hf : ∀ (y : ℝ), √ProofData.x ≤ y → y ≤ ProofData.x → f y ≤ M) (hM : 0 ≤ M) : maxy f ≤ M

noncomputable def maxya [data : ProofData] (q : ℕ) (f : ℝ → ZMod q → ℝ) : ℝ

The maximum of $f$ over all $y \in \left[\sqrt{x}, x\right]$ and $a \in (\mathbb{Z} / q\mathbb{Z})^*

Equations

• maxya q f = ⨆ (a : (ZMod q)ˣ), maxy fun (y : ℝ) => f y ↑a

theorem maxya_le [data : ProofData] {q : ℕ} {f : ℝ → ZMod q → ℝ} {M : ℝ} (hf : ∀ (y : ℝ), √ProofData.x ≤ y → y ≤ ProofData.x → ∀ (a : ZMod q), f y a ≤ M) (hM : 0 ≤ M) : maxya q f ≤ M

noncomputable def ArithmeticFunction.on {R : Type u_1} [Zero R] (s : Set ℕ) (f : ArithmeticFunction R) : ArithmeticFunction R

Restrict an arithmetic function to a set, setting all values outside the set to zero. Like Set.indicator but for ArithmeticFunction.

Equations

• ArithmeticFunction.on s f = { toFun := s.indicator ⇑f, map_zero' := ⋯ }

@[simp]

theorem ArithmeticFunction.on_apply_of_mem {R : Type u_1} [Zero R] (s : Set ℕ) (f : ArithmeticFunction R) (n : ℕ) (hn : n ∈ s) : (on s f) n = f n

@[simp]

theorem ArithmeticFunction.on_apply_of_not_mem {R : Type u_1} [Zero R] (s : Set ℕ) (f : ArithmeticFunction R) (n : ℕ) (hn : n ∉ s) : (on s f) n = 0

theorem ArithmeticFunction.on_nonneg {R : Type u_1} [Zero R] [Preorder R] {s : Set ℕ} {f : ArithmeticFunction R} (hf : ∀ n ∈ s, 0 ≤ f n) (n : ℕ) : 0 ≤ (on s f) n

@[simp]

theorem ArithmeticFunction.on_nonneg_iff {R : Type u_1} [Zero R] [Preorder R] (s : Set ℕ) (f : ArithmeticFunction R) : (∀ (n : ℕ), 0 ≤ (on s f) n) ↔ ∀ n ∈ s, 0 ≤ f n

noncomputable def LambdaLEU [data : ProofData] : ArithmeticFunction ℝ

$\Lambda_{\le U} = 1_{≤ U} \cdot \Lambda$

Equations

• LambdaLEU = ArithmeticFunction.on (Set.Icc 1 ⌊ProofData.U⌋₊) ArithmeticFunction.vonMangoldt

def BV.«termΛ≤U» : Lean.ParserDescr

Equations

• BV.«termΛ≤U» = Lean.ParserDescr.node `BV.«termΛ≤U» 1024 (Lean.ParserDescr.symbol "Λ≤U")

@[simp]

theorem LambdaLEU_apply_of_le [data : ProofData] {n : ℕ} (hn : ↑n ≤ ProofData.U) : LambdaLEU n = ArithmeticFunction.vonMangoldt n

@[simp]

theorem LambdaLEU_apply_of_gt [data : ProofData] {n : ℕ} (hn : ProofData.U < ↑n) : LambdaLEU n = 0

@[simp]

theorem LambdaLEU_nonneg [data : ProofData] {n : ℕ} : 0 ≤ LambdaLEU n

def LambdaLEU_positivity : Mathlib.Meta.Positivity.PositivityExt

Equations

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

noncomputable def moebiusLEV [data : ProofData] : ArithmeticFunction ℝ

$\mu{\le U} = 1_{≤ U} \cdot \mu$

Equations

• moebiusLEV = ArithmeticFunction.on (Set.Icc 1 ⌊ProofData.V⌋₊) ↑ArithmeticFunction.moebius

def BV.«termμ≤V» : Lean.ParserDescr

Equations

• BV.«termμ≤V» = Lean.ParserDescr.node `BV.«termμ≤V» 1024 (Lean.ParserDescr.symbol "μ≤V")

noncomputable def LambdaSharp [data : ProofData] : ArithmeticFunction ℝ

Equations

• LambdaSharp = moebiusLEV * ArithmeticFunction.log - LambdaLEU * moebiusLEV * ↑ArithmeticFunction.zeta

def BV.«termΛ♯» : Lean.ParserDescr

Equations

• BV.«termΛ♯» = Lean.ParserDescr.node `BV.«termΛ♯» 1024 (Lean.ParserDescr.symbol "Λ♯")

noncomputable def LambdaFlat [data : ProofData] : ArithmeticFunction ℝ

Equations

• LambdaFlat = (ArithmeticFunction.vonMangoldt - LambdaLEU) * ↑ArithmeticFunction.zeta * (↑ArithmeticFunction.moebius - moebiusLEV)

def BV.«termΛ♭» : Lean.ParserDescr

Equations

• BV.«termΛ♭» = Lean.ParserDescr.node `BV.«termΛ♭» 1024 (Lean.ParserDescr.symbol "Λ♭")

theorem Lambda_decomp [data : ProofData] (n : ℕ) : ArithmeticFunction.vonMangoldt n = LambdaSharp n + LambdaFlat n + LambdaLEU n

Decompose $\Lambda = \Lambda^\sharp + \Lambda^\flat + \Lambda_{\le U}$