|
| 1 | +/- |
| 2 | +Copyright (c) 2025 Snir Broshi. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Snir Broshi |
| 5 | +-/ |
| 6 | +module |
| 7 | + |
| 8 | +public import Mathlib.Algebra.GCDMonoid.FinsetLemmas |
| 9 | +public import Mathlib.NumberTheory.ArithmeticFunction.Defs |
| 10 | +public import Mathlib.RingTheory.ZMod.UnitsCyclic |
| 11 | + |
| 12 | +/-! |
| 13 | +# The Carmichael function |
| 14 | +
|
| 15 | +## Main definitions |
| 16 | +
|
| 17 | +* `ArithmeticFunction.Carmichael`: the Carmichael function `λ`, |
| 18 | + also known as the reduced totient function. |
| 19 | +
|
| 20 | +## Main results |
| 21 | +
|
| 22 | +* A formula for `λ n` in terms of the prime factorization of `n`, given by the following theorems: |
| 23 | + `carmichael_two_pow_of_le_two`, `carmichael_two_pow_of_ne_two`, `carmichael_pow_of_prime_ne_two`, |
| 24 | + and `carmichael_factorization`. |
| 25 | +
|
| 26 | +## Notation |
| 27 | +
|
| 28 | +We use the standard notation `λ` to represent the Carmichael function, |
| 29 | +which is accessible in the scope `ArithmeticFunction.Carmichael`. |
| 30 | +Since the notation conflicts with the anonymous function notation, it is impossible to use this |
| 31 | +notation in statements, but the pretty-printer will use it when showing the goal state. |
| 32 | +
|
| 33 | +## Tags |
| 34 | +
|
| 35 | +arithmetic functions, totient |
| 36 | +-/ |
| 37 | + |
| 38 | +@[expose] public section |
| 39 | + |
| 40 | +open Nat Monoid |
| 41 | + |
| 42 | +variable {R : Type*} |
| 43 | + |
| 44 | +namespace ArithmeticFunction |
| 45 | + |
| 46 | +/-- `λ` is the Carmichael function, also known as the reduced totient function, |
| 47 | +defined as the exponent of the unit group of `ZMod n`. -/ |
| 48 | +def Carmichael : ArithmeticFunction ℕ where |
| 49 | + toFun |
| 50 | + | 0 => 0 |
| 51 | + | n + 1 => Nat.find <| ExponentExists.of_finite (G := (ZMod (n + 1))ˣ) |
| 52 | + map_zero' := rfl |
| 53 | + |
| 54 | +@[inherit_doc] |
| 55 | +scoped[ArithmeticFunction.Carmichael] notation "λ" => ArithmeticFunction.Carmichael |
| 56 | + |
| 57 | +open scoped Carmichael |
| 58 | + |
| 59 | +theorem carmichael_eq_exponent {n : ℕ} (hn : n ≠ 0) : Carmichael n = exponent (ZMod n)ˣ := by |
| 60 | + cases n with | zero => contradiction | succ n => |
| 61 | + change Nat.find _ = _ |
| 62 | + grind [exponent, ExponentExists.of_finite] |
| 63 | + |
| 64 | +/-- This takes in an `NeZero n` instance instead of an `n ≠ 0` hypothesis. -/ |
| 65 | +theorem carmichael_eq_exponent' (n : ℕ) [NeZero n] : Carmichael n = exponent (ZMod n)ˣ := |
| 66 | + carmichael_eq_exponent <| NeZero.ne n |
| 67 | + |
| 68 | +@[simp] |
| 69 | +theorem pow_carmichael {n : ℕ} (a : (ZMod n)ˣ) : a ^ Carmichael n = 1 := by |
| 70 | + cases n |
| 71 | + · rw [map_zero, pow_zero] |
| 72 | + rw [carmichael_eq_exponent'] |
| 73 | + exact pow_exponent_eq_one a |
| 74 | + |
| 75 | +theorem carmichael_dvd_totient (n : ℕ) : Carmichael n ∣ n.totient := by |
| 76 | + cases n |
| 77 | + · simp |
| 78 | + rw [← ZMod.card_units_eq_totient, carmichael_eq_exponent'] |
| 79 | + exact Group.exponent_dvd_card |
| 80 | + |
| 81 | +theorem carmichael_dvd {a b : ℕ} (h : a ∣ b) : Carmichael a ∣ Carmichael b := by |
| 82 | + cases b |
| 83 | + · simp |
| 84 | + rw [carmichael_eq_exponent <| ne_zero_of_dvd_ne_zero (by lia) h, carmichael_eq_exponent'] |
| 85 | + exact MonoidHom.exponent_dvd <| ZMod.unitsMap_surjective h |
| 86 | + |
| 87 | +theorem carmichael_lcm (a b : ℕ) : |
| 88 | + Carmichael (Nat.lcm a b) = Nat.lcm (Carmichael a) (Carmichael b) := by |
| 89 | + by_cases! h₀ : a = 0 ∨ b = 0 |
| 90 | + · grind [Nat.lcm_eq_zero_iff, map_zero] |
| 91 | + apply dvd_antisymm |
| 92 | + · rw [carmichael_eq_exponent h₀.left, carmichael_eq_exponent h₀.right, |
| 93 | + carmichael_eq_exponent <| lcm_ne_zero h₀.left h₀.right, ← lcm_eq_nat_lcm <| exponent _, |
| 94 | + ← exponent_prod, ← exponent_eq_of_mulEquiv .prodUnits] |
| 95 | + exact exponent_dvd_of_monoidHom _ <| Units.map_injective <| ZMod.castHom_injective _ |
| 96 | + · have ha := carmichael_dvd <| Nat.dvd_lcm_left a b |
| 97 | + have hb := carmichael_dvd <| Nat.dvd_lcm_right a b |
| 98 | + exact Nat.lcm_dvd ha hb |
| 99 | + |
| 100 | +theorem carmichael_mul {a b : ℕ} (h : Coprime a b) : |
| 101 | + Carmichael (a * b) = Nat.lcm (Carmichael a) (Carmichael b) := |
| 102 | + h.lcm_eq_mul ▸ carmichael_lcm .. |
| 103 | + |
| 104 | +theorem carmichael_finset_lcm {α : Type*} (s : Finset α) (f : α → ℕ) : |
| 105 | + Carmichael (s.lcm f) = s.lcm (Carmichael ∘ f) := by |
| 106 | + classical |
| 107 | + refine s.induction ?_ fun a s ha ih ↦ ?_ |
| 108 | + · exact carmichael_eq_exponent' 1 |>.trans exp_eq_one_of_subsingleton |
| 109 | + rw [Finset.lcm_insert, Finset.lcm_insert, ← ih] |
| 110 | + exact carmichael_lcm .. |
| 111 | + |
| 112 | +theorem carmichael_finset_prod {α : Type*} {s : Finset α} {f : α → ℕ} |
| 113 | + (h : Set.Pairwise s <| Coprime.onFun f) : Carmichael (s.prod f) = s.lcm (Carmichael ∘ f) := |
| 114 | + s.lcm_eq_prod h ▸ carmichael_finset_lcm .. |
| 115 | + |
| 116 | +theorem carmichael_factorization (n : ℕ) [NeZero n] : |
| 117 | + Carmichael n = n.primeFactors.lcm fun p ↦ Carmichael (p ^ n.factorization p) := by |
| 118 | + nth_rw 1 [← n.factorization_prod_pow_eq_self <| NeZero.ne _] |
| 119 | + exact carmichael_finset_prod pairwise_coprime_pow_primeFactors_factorization.set_of_subtype |
| 120 | + |
| 121 | +theorem carmichael_two_pow_of_le_two_eq_totient {n : ℕ} (hn : n ≤ 2) : |
| 122 | + Carmichael (2 ^ n) = (2 ^ n).totient := by |
| 123 | + rw [carmichael_eq_exponent', ← ZMod.card_units_eq_totient, Fintype.card_eq_nat_card] |
| 124 | + exact IsCyclic.iff_exponent_eq_card.mp <| ZMod.isCyclic_units_two_pow_iff n |>.mpr hn |
| 125 | + |
| 126 | +/-- Note that `2 ^ (n - 1) = 1` when `n = 0`. -/ |
| 127 | +@[simp] |
| 128 | +theorem carmichael_two_pow_of_le_two {n : ℕ} (hn : n ≤ 2) : |
| 129 | + Carmichael (2 ^ n) = 2 ^ (n - 1) := by |
| 130 | + rw [carmichael_two_pow_of_le_two_eq_totient hn] |
| 131 | + interval_cases n <;> decide |
| 132 | + |
| 133 | +/-- Note that `2 ^ (n - 2) = 1` when `n ≤ 1`. -/ |
| 134 | +@[simp] |
| 135 | +theorem carmichael_two_pow_of_ne_two {n : ℕ} (hn : n ≠ 2) : |
| 136 | + Carmichael (2 ^ n) = 2 ^ (n - 2) := by |
| 137 | + by_cases hn' : n ≤ 2 |
| 138 | + · grind [carmichael_two_pow_of_le_two] |
| 139 | + refine carmichael_eq_exponent' _ |>.trans <| dvd_antisymm ?_ ?_ |
| 140 | + · have hcard : Nat.card (ZMod (2 ^ n))ˣ = 2 ^ (n - 1) := by |
| 141 | + rw [card_eq_fintype_card, ZMod.card_units_eq_totient, totient_prime_pow prime_two <| by lia, |
| 142 | + Nat.add_one_sub_one, mul_one] |
| 143 | + have ⟨k, hk, h⟩ := dvd_prime_pow prime_two |>.mp <| hcard ▸ Group.exponent_dvd_nat_card |
| 144 | + have := IsCyclic.iff_exponent_eq_card.not.mp <| ZMod.isCyclic_units_two_pow_iff n |>.not.mpr hn' |
| 145 | + exact h ▸ Nat.pow_dvd_pow 2 (by grind) |
| 146 | + · let five : (ZMod (2 ^ n))ˣ := ZMod.unitOfCoprime 5 <| gcd_pow_right_of_gcd_eq_one rfl |
| 147 | + rw [← ZMod.orderOf_five (n - 2), show n - 2 + 2 = n by lia, |
| 148 | + show (5 : ZMod (2 ^ n)) = five by rfl, orderOf_units] |
| 149 | + exact order_dvd_exponent five |
| 150 | + |
| 151 | +theorem two_mul_carmichael_two_pow_of_three_le_eq_totient {n : ℕ} (hn : 3 ≤ n) : |
| 152 | + 2 * Carmichael (2 ^ n) = (2 ^ n).totient := by |
| 153 | + rw [carmichael_two_pow_of_ne_two, ← pow_succ', totient_prime_pow prime_two] |
| 154 | + all_goals lia |
| 155 | + |
| 156 | +@[simp] |
| 157 | +theorem carmichael_pow_of_prime_ne_two {p : ℕ} (n : ℕ) (hp : p.Prime) (hp₂ : p ≠ 2) : |
| 158 | + Carmichael (p ^ n) = (p ^ n).totient := by |
| 159 | + have : NeZero p := ⟨hp.ne_zero⟩ |
| 160 | + rw [carmichael_eq_exponent', ← ZMod.card_units_eq_totient, Fintype.card_eq_nat_card] |
| 161 | + exact IsCyclic.iff_exponent_eq_card.mp <| ZMod.isCyclic_units_of_prime_pow p hp hp₂ n |
| 162 | + |
| 163 | +end ArithmeticFunction |
0 commit comments