Rearick logarithm

DefinitionRearick logarithm#✓fully proved

Let \(f\) be a real-valued arithmetic function with \(f(1) > 0\), and let \(f^{-1}\) be its Dirichlet inverse. The Rearick logarithm of \(f\) is the arithmetic function \(L(f)\) with \(L(f)(0) = 0\), \(L(f)(1) = \log f(1)\), and \(L(f)(n) = \sum_{d \mid n} f(d) \, f^{-1}(n/d) \log d\) for \(n > 1\).

noncomputable def rearickLog (f : ArithmeticFunction ℝ) (hf : 0 < f 1) :
    ArithmeticFunction ℝ :=
  ⟨fun n =>
    if n = 0 then 0
    else if n = 1 then Real.log (f 1)
    else
      ∑ d ∈ n.divisors,
        f d *
          ArithmeticFunction.dirichletInverse (⇑f)
            (invertibleOfNonzero (ne_of_gt hf)) (n / d) *
          Real.log (d : ℝ),
    by simp⟩

Used by 4

Used byReal powers preserve multiplicativity and antimultiplicativity · Rearick's real power and its vector space laws · The Rearick logarithm as a Dirichlet convolution · Rearick's characterization of multiplicative functions

TheoremThe Rearick logarithm as a Dirichlet convolution#✓fully proved

Let \(f\) be a real-valued arithmetic function with \(f(1) = 1\), and let \(f^{-1}\) be its Dirichlet inverse. Then the Rearick logarithm of \(f\) is the Dirichlet convolution of the pointwise product \(n \mapsto f(n) \log n\) with \(f^{-1}\).

theorem rearickLog_eq_pmul_log_mul_dirichletInverse (f : ArithmeticFunction ℝ) (hf : 0 < f 1)
    (h1 : f 1 = 1) :
    rearickLog f hf =
      f.pmul ArithmeticFunction.log *
        ArithmeticFunction.dirichletInverse (⇑f) (invertibleOfNonzero (ne_of_gt hf))

noncomputable def rearickLog (f : ArithmeticFunction ℝ) (hf : 0 < f 1) :
    ArithmeticFunction ℝ :=
  ⟨fun n =>
    if n = 0 then 0
    else if n = 1 then Real.log (f 1)
    else
      ∑ d ∈ n.divisors,
        f d *
          ArithmeticFunction.dirichletInverse (⇑f)
            (invertibleOfNonzero (ne_of_gt hf)) (n / d) *
          Real.log (d : ℝ),
    by simp⟩

MathlibExt/NumberTheory/RearickLogarithm.lean:32

Uses 1 · Used by 1

Statement usesRearick logarithm

Used byRearick's characterization of multiplicative functions

TheoremRearick's characterization of multiplicative functions#✓fully proved

Let \(f\) be a real-valued arithmetic function with \(f(1) > 0\), and let \(L(f)\) be its Rearick logarithm. Then \(f\) is multiplicative (that is, \(f(1) = 1\) and \(f(mn) = f(m) f(n)\) whenever \(m\) and \(n\) are coprime) if and only if \(L(f)(m) = 0\) for every natural number \(m\) that is not a prime power, including \(m = 0\) and \(m = 1\).

theorem rearick_log_eq_zero_iff_isMultiplicative
    (f : ArithmeticFunction ℝ) (hf : 0 < f 1) :
    f.IsMultiplicative ↔ ∀ m : ℕ, ¬ IsPrimePow m → rearickLog f hf m = 0

noncomputable def rearickLog (f : ArithmeticFunction ℝ) (hf : 0 < f 1) :
    ArithmeticFunction ℝ :=
  ⟨fun n =>
    if n = 0 then 0
    else if n = 1 then Real.log (f 1)
    else
      ∑ d ∈ n.divisors,
        f d *
          ArithmeticFunction.dirichletInverse (⇑f)
            (invertibleOfNonzero (ne_of_gt hf)) (n / d) *
          Real.log (d : ℝ),
    by simp⟩

MathlibExt/NumberTheory/RearickLogarithm.lean:32

Sources

Rearick logarithm support characterization of multiplicative arithmetic functions, after Huilan Li and Trueman MacHenry, arXiv:1009.1892v1, https://arxiv.org/abs/1009.1892, lines 444-450 (Rearick logarithm definition) and 706-708 (Rearick Theorem 4). Real-valued domain closure with f 1 > 0 after Pong, arXiv:1504.03263v2, https://arxiv.org/abs/1504.03263, lines 174-195; positivity also supplies the nonzero premise for the Dirichlet inverse.

Uses 2

Statement usesRearick logarithm

Proof usesThe Rearick logarithm as a Dirichlet convolution

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.