Möbius–Fermat function

DefinitionFermat unit function#✓fully proved

The Fermat unit function \(u_M\) is the integer-valued arithmetic function with \(u_M(l) = 1\) when \(l = 2^n - 1\) for some integer \(n \ge 1\), and \(u_M(l) = 0\) otherwise (in particular \(u_M(0) = 0\)). Equivalently, \(u_M(l) = 1\) exactly when \(l \ge 1\) and \(l + 1\) is a power of \(2\).

def fermatUnitFunction : ArithmeticFunction ℤ :=
  ⟨fun l => if l ≠ 0 ∧ 2 ^ Nat.log 2 (l + 1) = l + 1 then 1 else 0, by simp⟩

Sources

• J. L. Varona, The Möbius and the von Mangoldt-type Functions of the Fermat Zeta Function, INTEGERS 26 (2026), Article A106, equation (7).

Used by 10

Used bySmall values of the Fermat unit function · The Fermat unit function at \(2^n - 1\) · Closed form of the Möbius–Fermat function · Multinomial formula for the Möbius–Fermat function · Reduction of the Möbius–Fermat function to distinct factors · The Möbius–Fermat and von Mangoldt–Fermat functions at \(1\) and off the Fermat semigroup · The Möbius–Fermat function at \(3^m 7^n\) · The Möbius–Fermat function at \(3^m 7^n q^k\) · Closed form of the von Mangoldt–Fermat function · Multinomial formula for the von Mangoldt–Fermat function

TheoremThe Fermat unit function at \(2^n - 1\)#✓fully proved

For every integer \(n \ge 1\), the Fermat unit function \(u_M\) satisfies \(u_M(2^n - 1) = 1\).

theorem fermatUnitFunction_two_pow_sub_one {n : ℕ} (hn : 1 ≤ n) :
    fermatUnitFunction (2 ^ n - 1) = 1

Sources

• J. L. Varona, The Möbius and the von Mangoldt-type Functions of the Fermat Zeta Function, INTEGERS 26 (2026), Article A106, equation (7).

Uses 1

Statement usesFermat unit function

TheoremSmall values of the Fermat unit function#✓fully proved

The Fermat unit function \(u_M\) satisfies \(u_M(1) = u_M(3) = u_M(7) = u_M(63) = 1\) and \(u_M(2) = u_M(9) = 0\).

theorem fermatUnitFunction_small_values :
    fermatUnitFunction 1 = 1 ∧ fermatUnitFunction 3 = 1 ∧ fermatUnitFunction 7 = 1 ∧
      fermatUnitFunction 63 = 1 ∧ fermatUnitFunction 2 = 0 ∧ fermatUnitFunction 9 = 0

Sources

• J. L. Varona, The Möbius and the von Mangoldt-type Functions of the Fermat Zeta Function, INTEGERS 26 (2026), Article A106, equation (7).

Uses 1

Statement usesFermat unit function

TheoremThe Möbius–Fermat and von Mangoldt–Fermat functions at \(1\) and off the Fermat semigroup#●ready to prove

The Möbius–Fermat and von Mangoldt–Fermat functions at \(1\) and off the Fermat semigroup. Let \(u_M\) be the Fermat unit function and let \(\mu_M\) be an integer-valued arithmetic function with \(\mu_M * u_M = \varepsilon\), where \(*\) is Dirichlet convolution and \(\varepsilon\) is its identity, with \(\varepsilon(1) = 1\) and \(\varepsilon(l) = 0\) for \(l \ne 1\); thus \(\mu_M\) is the Dirichlet inverse of \(u_M\), the Möbius–Fermat function. Let \(\Lambda_M = \mu_M * u_M'\), computed with real values, where \(u_M'(l) = u_M(l) \log l\). Then \(\mu_M(1) = 1\) and \(\Lambda_M(1) = 0\), and \(\mu_M(l) = \Lambda_M(l) = 0\) for every natural number \(l\) outside the Fermat semigroup, the multiplicative submonoid of \(\mathbb{N}\) generated by the numbers \(2^n - 1\) with \(n \ge 2\).

public theorem_wanted mobiusFermat_one_and_vanishing (μ : ArithmeticFunction ℤ)
    (hμ : μ * fermatUnitFunction = 1) :
    μ 1 = 1 ∧
      ((μ : ArithmeticFunction ℝ) * (fermatUnitFunction : ArithmeticFunction ℝ).pmul log) 1 = 0 ∧
      ∀ l : ℕ, l ∉ Submonoid.closure {x : ℕ | ∃ n, 2 ≤ n ∧ x = 2 ^ n - 1} →
        μ l = 0 ∧
          ((μ : ArithmeticFunction ℝ) * (fermatUnitFunction : ArithmeticFunction ℝ).pmul log) l
            = 0

Sources

• J. L. Varona, The Möbius and the von Mangoldt-type Functions of the Fermat Zeta Function, INTEGERS 26 (2026), Article A106, Proposition 2.

Uses 1

Statement usesFermat unit function

TheoremMultinomial formula for the Möbius–Fermat function#●ready to prove

Let \(u_M\) be the Fermat unit function and let \(\mu_M\) be an integer-valued arithmetic function with \(\mu_M * u_M = \varepsilon\), where \(*\) is Dirichlet convolution and \(\varepsilon\) is its identity, with \(\varepsilon(1) = 1\) and \(\varepsilon(l) = 0\) for \(l \ne 1\); thus \(\mu_M\) is the Dirichlet inverse of \(u_M\), the Möbius–Fermat function. Let \(n_1, \dots, n_k\) be finitely many (possibly no) distinct integers with \(n_i \ge 2\) and \(n_i \ne 6\), let \(m_1, \dots, m_k \ge 1\) be integers, and put \(l = \prod_{i=1}^{k} (2^{n_i} - 1)^{m_i}\) and \(r = m_1 + \dots + m_k\). Suppose that \(2\) is not among the \(n_i\) or has exponent \(1\), or that \(3\) is not among the \(n_i\); that is, the factor \(3 = 2^2 - 1\) occurs at most to the first power or the factor \(7 = 2^3 - 1\) does not occur. Then, as rational numbers, \(\mu_M(l) = (-1)^r \, r! / (m_1! \cdots m_k!)\).

public theorem_wanted mobiusFermat_eq_multinomial (μ : ArithmeticFunction ℤ)
    (hμ : μ * fermatUnitFunction = 1) (f : ℕ →₀ ℕ) (hf : ∀ n ∈ f.support, 2 ≤ n ∧ n ≠ 6)
    (h37 : f 2 ≤ 1 ∨ f 3 = 0) :
    (μ (f.prod fun n m => (2 ^ n - 1) ^ m) : ℚ) =
      (-1) ^ (f.sum fun _ m => m) * ((f.sum fun _ m => m).factorial : ℚ) /
        (f.prod fun _ m => (m.factorial : ℚ))

Sources

• J. L. Varona, The Möbius and the von Mangoldt-type Functions of the Fermat Zeta Function, INTEGERS 26 (2026), Article A106, Proposition 4.

Uses 1

Statement usesFermat unit function

TheoremMultinomial formula for the von Mangoldt–Fermat function#●ready to prove

Let \(u_M\) be the Fermat unit function, and let \(\mu\) be an integer-valued arithmetic function with \(\mu * u_M = \varepsilon\), where \(*\) is Dirichlet convolution and \(\varepsilon\) is its identity (so \(\mu\) is the Möbius–Fermat function \(\mu_M\)). Let \(\Lambda_M = \mu * u'_M\), computed with real values, where \(u'_M(l) = u_M(l) \log l\). Let \(f : \mathbb{N} \to \mathbb{N}\) be finitely supported, with \(n \ge 2\) and \(n \ne 6\) for every \(n\) such that \(f(n) \ne 0\), and with \(f(2) \le 1\) or \(f(3) = 0\). Put \(l = \prod_n (2^n - 1)^{f(n)}\) and \(r = \sum_n f(n)\). Then

\[\Lambda_M(l) = (-1)^{r - 1} \frac{(r - 1)!}{\prod_n f(n)!} \log l,\]

where \(r - 1\) is read as \(0\) when \(r = 0\).

public theorem_wanted vonMangoldtFermat_eq_multinomial (μ : ArithmeticFunction ℤ)
    (hμ : μ * fermatUnitFunction = 1) (f : ℕ →₀ ℕ) (hf : ∀ n ∈ f.support, 2 ≤ n ∧ n ≠ 6)
    (h37 : f 2 ≤ 1 ∨ f 3 = 0) :
    ((μ : ArithmeticFunction ℝ) * (fermatUnitFunction : ArithmeticFunction ℝ).pmul log)
        (f.prod fun n m => (2 ^ n - 1) ^ m) =
      (-1) ^ ((f.sum fun _ m => m) - 1) * (((f.sum fun _ m => m) - 1).factorial : ℝ) /
        (f.prod fun _ m => (m.factorial : ℝ)) *
        Real.log (f.prod fun n m => (2 ^ n - 1) ^ m : ℕ)

Sources

• J. L. Varona, The Möbius and the von Mangoldt-type Functions of the Fermat Zeta Function, INTEGERS 26 (2026), Article A106, Proposition 5.

Uses 1

Statement usesFermat unit function

TheoremReduction of the Möbius–Fermat function to distinct factors#●ready to prove

Let \(u_M\) be the Fermat unit function and let \(\mu_M\) be an integer-valued arithmetic function with \(\mu_M * u_M = \varepsilon\), where \(*\) is Dirichlet convolution and \(\varepsilon\) is its identity, with \(\varepsilon(1) = 1\) and \(\varepsilon(l) = 0\) for \(l \ne 1\); thus \(\mu_M\) is the Dirichlet inverse of \(u_M\), the Möbius–Fermat function. Let \(m_1, m_2 \ge 0\) be integers, let \(n_3, \dots, n_k\) be finitely many (possibly no) distinct integers with \(n_j \ge 4\) and \(n_j \ne 6\), let \(m_3, \dots, m_k \ge 1\) be integers, and put \(l = 3^{m_1} 7^{m_2} \prod_{j=3}^{k} (2^{n_j} - 1)^{m_j}\). Then for every finite set \(T\) of integers \(n \ge 4\) with \(n \ne 6\) and \(|T| = m_3 + \dots + m_k\),

\[\mu_M(l) \, m_3! \cdots m_k! = \mu_M\Big(3^{m_1} 7^{m_2} \prod_{n \in T} (2^n - 1)\Big).\]

In particular the right-hand side does not depend on the choice of \(T\).

public theorem_wanted mobiusFermat_mul_factorial_eq_squarefree_part (μ : ArithmeticFunction ℤ)
    (hμ : μ * fermatUnitFunction = 1) (m₁ m₂ : ℕ) (f : ℕ →₀ ℕ)
    (hf : ∀ n ∈ f.support, 4 ≤ n ∧ n ≠ 6) (T : Finset ℕ) (hT : ∀ n ∈ T, 4 ≤ n ∧ n ≠ 6)
    (hcard : T.card = f.sum fun _ m => m) :
    μ (3 ^ m₁ * 7 ^ m₂ * f.prod fun n m => (2 ^ n - 1) ^ m) * (f.prod fun _ m => (m.factorial : ℤ)) =
      μ (3 ^ m₁ * 7 ^ m₂ * ∏ n ∈ T, (2 ^ n - 1))

Sources

• J. L. Varona, The Möbius and the von Mangoldt-type Functions of the Fermat Zeta Function, INTEGERS 26 (2026), Article A106, Proposition 6.

Uses 1

Statement usesFermat unit function

TheoremThe Möbius–Fermat function at \(3^m 7^n\)#●ready to prove

Let \(u_M\) be the Fermat unit function and let \(\mu_M\) be an integer-valued arithmetic function with \(\mu_M * u_M = \varepsilon\), where \(*\) is Dirichlet convolution and \(\varepsilon\) is its identity, with \(\varepsilon(1) = 1\) and \(\varepsilon(l) = 0\) for \(l \ne 1\); thus \(\mu_M\) is the Dirichlet inverse of \(u_M\), the Möbius–Fermat function. Then for all integers \(m, n \ge 0\),

\[\mu_M(3^m 7^n) = (-1)^{m+n} \sum_{j=0}^{\min(\lfloor m/2 \rfloor, n)} \binom{n}{j} \binom{m + n - 2j}{m - 2j},\]

and, as rational numbers,

\[\mu_M(3^m 7^n) = (-1)^{m+n} \sum_{j=0}^{\min(\lfloor m/2 \rfloor, n)} \frac{(m + n - 2j)!}{(m - 2j)! \, (n - j)! \, j!}.\]

public theorem_wanted mobiusFermat_three_pow_mul_seven_pow (μ : ArithmeticFunction ℤ)
    (hμ : μ * fermatUnitFunction = 1) (m n : ℕ) :
    μ (3 ^ m * 7 ^ n) = (-1) ^ (m + n) *
        ∑ j ∈ Finset.range (min (m / 2) n + 1),
          ((n.choose j * (m + n - 2 * j).choose (m - 2 * j) : ℕ) : ℤ) ∧
      (μ (3 ^ m * 7 ^ n) : ℚ) = (-1) ^ (m + n) *
        ∑ j ∈ Finset.range (min (m / 2) n + 1),
          ((m + n - 2 * j).factorial : ℚ) /
            ((m - 2 * j).factorial * (n - j).factorial * j.factorial)

Sources

• J. L. Varona, The Möbius and the von Mangoldt-type Functions of the Fermat Zeta Function, INTEGERS 26 (2026), Article A106, Proposition 7.

Uses 1

Statement usesFermat unit function

TheoremThe Möbius–Fermat function at \(3^m 7^n q^k\)#●ready to prove

Let \(u_M\) be the Fermat unit function and let \(\mu_M\) be an integer-valued arithmetic function with \(\mu_M * u_M = \varepsilon\), where \(*\) is Dirichlet convolution and \(\varepsilon\) is its identity, with \(\varepsilon(1) = 1\) and \(\varepsilon(l) = 0\) for \(l \ne 1\); thus \(\mu_M\) is the Dirichlet inverse of \(u_M\), the Möbius–Fermat function. Let \(t \ge 4\) be an integer with \(t \ne 6\) and put \(q = 2^t - 1\). Then for all integers \(m, n, k \ge 0\), as rational numbers,

\[\mu_M(3^m 7^n q^k) = (-1)^{m+n+k} \sum_{j=0}^{\min(\lfloor m/2 \rfloor, n)} \frac{(m + n - 2j + k)!}{(m - 2j)! \, (n - j)! \, j! \, k!}.\]

The conditions on \(t\) exclude \(q = 1, 3, 7, 63\).

public theorem_wanted mobiusFermat_three_pow_mul_seven_pow_mul_pow (μ : ArithmeticFunction ℤ)
    (hμ : μ * fermatUnitFunction = 1) {t : ℕ} (ht : 4 ≤ t) (ht6 : t ≠ 6) (m n k : ℕ) :
    (μ (3 ^ m * 7 ^ n * (2 ^ t - 1) ^ k) : ℚ) = (-1) ^ (m + n + k) *
      ∑ j ∈ Finset.range (min (m / 2) n + 1),
        ((m + n - 2 * j + k).factorial : ℚ) /
          ((m - 2 * j).factorial * (n - j).factorial * j.factorial * k.factorial)

Sources

• J. L. Varona, The Möbius and the von Mangoldt-type Functions of the Fermat Zeta Function, INTEGERS 26 (2026), Article A106, Proposition 8.

Uses 1

Statement usesFermat unit function

TheoremClosed form of the Möbius–Fermat function#●ready to prove

Let \(u_M\) be the Fermat unit function and let \(\mu_M\) be an integer-valued arithmetic function with \(\mu_M * u_M = \varepsilon\), where \(*\) is Dirichlet convolution and \(\varepsilon\) is its identity, with \(\varepsilon(1) = 1\) and \(\varepsilon(l) = 0\) for \(l \ne 1\); thus \(\mu_M\) is the Dirichlet inverse of \(u_M\), the Möbius–Fermat function. Let \(m_1, m_2 \ge 0\) be integers, let \(n_3, \dots, n_k\) be finitely many (possibly no) distinct integers with \(n_j \ge 4\) and \(n_j \ne 6\), let \(m_3, \dots, m_k \ge 1\) be integers, and put \(l = 3^{m_1} 7^{m_2} \prod_{j=3}^{k} (2^{n_j} - 1)^{m_j}\) and \(r = m_1 + m_2 + m_3 + \dots + m_k\). Then, as rational numbers,

\[\mu_M(l) = (-1)^r \sum_{j=0}^{\min(\lfloor m_1/2 \rfloor, m_2)} \frac{(r - 2j)!}{(m_1 - 2j)! \, (m_2 - j)! \, j! \, m_3! \cdots m_k!}.\]

public theorem_wanted mobiusFermat_closed_form (μ : ArithmeticFunction ℤ)
    (hμ : μ * fermatUnitFunction = 1) (m₁ m₂ : ℕ) (f : ℕ →₀ ℕ)
    (hf : ∀ n ∈ f.support, 4 ≤ n ∧ n ≠ 6) :
    (μ (3 ^ m₁ * 7 ^ m₂ * f.prod fun n m => (2 ^ n - 1) ^ m) : ℚ) =
      (-1) ^ (m₁ + m₂ + f.sum fun _ m => m) *
        ∑ j ∈ Finset.range (min (m₁ / 2) m₂ + 1),
          ((m₁ + m₂ + (f.sum fun _ m => m) - 2 * j).factorial : ℚ) /
            ((m₁ - 2 * j).factorial * (m₂ - j).factorial * j.factorial *
              f.prod fun _ m => (m.factorial : ℚ))

Sources

• J. L. Varona, The Möbius and the von Mangoldt-type Functions of the Fermat Zeta Function, INTEGERS 26 (2026), Article A106, Theorem 9.

Uses 1

Statement usesFermat unit function

TheoremClosed form of the von Mangoldt–Fermat function#●ready to prove

Let \(u_M\) be the Fermat unit function and let \(\mu_M\) be an integer-valued arithmetic function with \(\mu_M * u_M = \varepsilon\), where \(*\) is Dirichlet convolution and \(\varepsilon\) is its identity, with \(\varepsilon(1) = 1\) and \(\varepsilon(l) = 0\) for \(l \ne 1\); thus \(\mu_M\) is the Dirichlet inverse of \(u_M\), the Möbius–Fermat function. Let \(\Lambda_M = \mu_M * u_M'\), computed with real values, where \(u_M'(l) = u_M(l) \log l\). Let \(m_1, m_2 \ge 0\) be integers, let \(n_3, \dots, n_k\) be finitely many (possibly no) distinct integers with \(n_j \ge 4\) and \(n_j \ne 6\), let \(m_3, \dots, m_k \ge 1\) be integers, and put \(l = 3^{m_1} 7^{m_2} \prod_{j=3}^{k} (2^{n_j} - 1)^{m_j}\) and \(r = m_1 + m_2 + m_3 + \dots + m_k\). Then

\[\Lambda_M(l) = (-1)^{r-1} \Big(\sum_{j=0}^{\min(\lfloor m_1/2 \rfloor, m_2)} \frac{(r - 2j - 1)!}{(m_1 - 2j)! \, (m_2 - j)! \, j! \, m_3! \cdots m_k!}\Big) \log l.\]

When \(r = 0\), that is \(l = 1\), both sides are \(0\): on the right, \(r - 1\) and \(r - 2j - 1\) are read as \(0\) and \(\log 1 = 0\).

public theorem_wanted vonMangoldtFermat_closed_form (μ : ArithmeticFunction ℤ)
    (hμ : μ * fermatUnitFunction = 1) (m₁ m₂ : ℕ) (f : ℕ →₀ ℕ)
    (hf : ∀ n ∈ f.support, 4 ≤ n ∧ n ≠ 6) :
    ((μ : ArithmeticFunction ℝ) * (fermatUnitFunction : ArithmeticFunction ℝ).pmul log)
        (3 ^ m₁ * 7 ^ m₂ * f.prod fun n m => (2 ^ n - 1) ^ m) =
      (-1) ^ (m₁ + m₂ + (f.sum fun _ m => m) - 1) *
        (∑ j ∈ Finset.range (min (m₁ / 2) m₂ + 1),
          ((m₁ + m₂ + (f.sum fun _ m => m) - 2 * j - 1).factorial : ℝ) /
            ((m₁ - 2 * j).factorial * (m₂ - j).factorial * j.factorial *
              f.prod fun _ m => (m.factorial : ℝ))) *
        Real.log (3 ^ m₁ * 7 ^ m₂ * f.prod fun n m => (2 ^ n - 1) ^ m : ℕ)

Sources

• J. L. Varona, The Möbius and the von Mangoldt-type Functions of the Fermat Zeta Function, INTEGERS 26 (2026), Article A106, Theorem 10.

Uses 1

Statement usesFermat unit function

3 fully proved8 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.