theorem mertens_third : (fun (n : ℕ) => ∑ p ∈ (n + 1).primesBelow, Real.log (1 - 1 / ↑p) + Real.log (Real.log ↑n) + Real.eulerMascheroniConstant) =O[Filter.atTop] fun (n : ℕ) => 1 / Real.log ↑n

def ArithFuncZ : Type

@[implicit_reducible]

instance ArithFuncZ.instCoeFunForallIntComplex : CoeFun ArithFuncZ fun (x : ArithFuncZ) => ℤ → ℂ

structure ArithFuncZ.IsMultiplicative (f : ArithFuncZ) : Prop

• map_one : f 1 = 1
• map_mul_of_coprime (m n : ℤ) : m.gcd n = 1 → f (m * n) = f m * f n

structure ArithFuncZ.IsTotallyMultiplicative (f : ArithFuncZ) : Prop

• map_one : f 1 = 1
• map_mul (m n : ℤ) : f (m * n) = f m * f n

def ArithFuncZ.IsPeriodic (f : ArithFuncZ) (m : ℤ) : Prop

noncomputable def ArithFuncZ.period (f : ArithFuncZ) : ℤ

structure ArithFuncZ.IsDirichletCharacter (χ : ArithFuncZ) (q : ℤ) : Prop

• modulus_pos : 0 < q
• totallyMultiplicative : χ.IsTotallyMultiplicative
• periodic : χ.IsPeriodic q

structure ArithFuncZ.IsDirichletCharacterMod (χ : ArithFuncZ) (m : ℤ) extends χ.IsDirichletCharacter m : Prop

• modulus_pos : 0 < m
• totallyMultiplicative : χ.IsTotallyMultiplicative
• periodic : χ.IsPeriodic m
• vanish_iff (n : ℤ) : χ n = 0 ↔ n.gcd m > 1

@[reducible, inline]

abbrev ArithFunc : Type

structure ArithFunc.IsTotallyMultiplicative (f : ArithFunc) : Prop

• map_one : f 1 = 1
• map_mul (m n : ℕ) : f (m * n) = f m * f n

def ArithFunc.IsPeriodic (f : ArithFunc) (m : ℕ) : Prop

noncomputable def ArithFunc.period (f : ArithFunc) : ℕ

structure ArithFunc.IsDirichletCharacter (χ : ArithFunc) : Prop

• totallyMultiplicative : χ.IsTotallyMultiplicative
• periodic : ∃ (m : ℕ), 0 < m ∧ χ.IsPeriodic m

noncomputable def ArithFunc.one : ArithFunc

noncomputable def ArithFunc.vonMangoldt : ArithFunc

def DirichletCharacter.IsInducedBy {R : Type u_1} [CommMonoidWithZero R] {m₁ m₂ : ℕ} (χ₂ : DirichletCharacter R m₂) (χ₁ : DirichletCharacter R m₁) (h : m₁ ∣ m₂) : Prop

theorem dirichletChar_factorsThrough_iff_ker_and_unique {R : Type u_1} [CommMonoidWithZero R] {m₂ : ℕ} [NeZero m₂] (χ₂ : DirichletCharacter R m₂) {m₁ : ℕ} (h : m₁ ∣ m₂) : (χ₂.FactorsThrough m₁ ↔ (ZMod.unitsMap h).ker ≤ (MulChar.toUnitHom χ₂).ker) ∧ (χ₂.FactorsThrough m₁ → ∃! χ₁ : DirichletCharacter R m₁, χ₂ = (DirichletCharacter.changeLevel h) χ₁)

def DirichletCharacter.IsPrincipal {R : Type u_1} [CommMonoidWithZero R] {m : ℕ} (χ : DirichletCharacter R m) : Prop

noncomputable def principalDirichletChar (R : Type u_1) [CommMonoidWithZero R] (m : ℕ) : DirichletCharacter R m