The Liouville Function

This file defines the Liouville function λ(n).

Main Definitions

• ArithmeticFunction.liouville is the Liouville function λ(n) defined to be 1 if n has an even number of prime factors (counting multiplicity) and -1 otherwise.

def ArithmeticFunction.liouville : ArithmeticFunction ℤ

OEIS A008836 (the sequence skips n = 0)

Equations

• ArithmeticFunction.liouville = { toFun := fun (n : ℕ) => if n = 0 then 0 else (-1) ^ ArithmeticFunction.cardFactors n, map_zero' := ArithmeticFunction.liouville._proof_1 }

theorem ArithmeticFunction.liouville_apply {n : ℕ} (h : n ≠ 0) : liouville n = (-1) ^ cardFactors n

theorem ArithmeticFunction.liouville_ne_zero {n : ℕ} (h : n ≠ 0) : liouville n ≠ 0

theorem ArithmeticFunction.liouville_apply_one : liouville 1 = 1

theorem ArithmeticFunction.liouville_apply_mul (m n : ℕ) : liouville (m * n) = liouville m * liouville n

theorem ArithmeticFunction.isMultiplicative_liouville : liouville.IsMultiplicative