Alder's totient function

DefinitionAlder's totient with second argument 2#✓fully proved

Alder's extension of Euler's totient with second argument \(2\) is the arithmetic function \(g : \mathbb{N} \to \mathbb{N}\) sending a natural number \(k\) to the number of natural numbers \(r < k\) with \(\gcd(k, r) = 1\) and \(\gcd(k, 2r+1) = 1\). In particular \(g(0) = 0\), since there is no natural number \(r < 0\).

def alderTotientTwo : ArithmeticFunction ℕ where
  toFun k :=
    ((Finset.range k).filter fun r =>
      Nat.Coprime k r ∧ Nat.Coprime k (2 * r + 1)).card
  map_zero' := by simp

Used by 2

Used byAlder's totient with second argument \(2\) is at most Euler's totient · Alder's totient at a successor as a count over an inclusive range

TheoremAlder's totient at a successor as a count over an inclusive range#✓fully proved

For every natural number \(k\), Alder's totient \(g\) with second argument \(2\) satisfies that \(g(k+1)\) is the number of natural numbers \(r \le k\) with \(\gcd(r, k+1) = 1\) and \(\gcd(2r+1, k+1) = 1\).

theorem alderTotientTwo_succ_Iic_apply (k : ℕ) :
    alderTotientTwo (k + 1) =
      ((Finset.Iic k).filter fun r =>
        Nat.Coprime r (k + 1) ∧ Nat.Coprime (2 * r + 1) (k + 1)).card

Uses 1

Statement usesAlder's totient with second argument 2

TheoremAlder's totient with second argument \(2\) is at most Euler's totient#✓fully proved

For every natural number \(k\), Alder's totient \(g(k)\) with second argument \(2\) is at most Euler's totient \(\varphi(k)\).

theorem alderTotientTwo_le_totient (k : ℕ) :
    alderTotientTwo k ≤ Nat.totient k

Uses 1

Statement usesAlder's totient with second argument 2

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.