feat: bounds for Dirichlet characters (#8449)

This adds `NumberTheory.DirichletCharacter.Bounds` containing proofs of `‖χ a‖ = 1` if `a` is a unit and `‖χ a‖ ≤ 1` in general, where `χ` is a Dirichlet character with values in a normed field.

There are also two API lemmas added elsewhere that are used in the proofs.

Mathlib.lean

@@ -2668,6 +2668,7 @@ import Mathlib.NumberTheory.Cyclotomic.Rat
 import Mathlib.NumberTheory.Dioph
 import Mathlib.NumberTheory.DiophantineApproximation
 import Mathlib.NumberTheory.DirichletCharacter.Basic
+import Mathlib.NumberTheory.DirichletCharacter.Bounds
 import Mathlib.NumberTheory.Divisors
 import Mathlib.NumberTheory.EulerProduct.Basic
 import Mathlib.NumberTheory.FLT.Basic

Mathlib/Algebra/GroupPower/Order.lean

@@ -223,6 +223,12 @@ theorem one_le_pow_iff_of_nonneg {a : R} (ha : 0 ≤ a) {n : ℕ} (hn : n ≠ 0)
   exact mt fun h => pow_lt_one ha h hn
 #align one_le_pow_iff_of_nonneg one_le_pow_iff_of_nonneg
 
+lemma pow_eq_one_iff_of_nonneg {a : R} (ha : 0 ≤ a)
+    {n : ℕ} (hn : n ≠ 0) : a ^ n = 1 ↔ a = 1 :=
+  ⟨fun h ↦ le_antisymm ((pow_le_one_iff_of_nonneg ha hn).mp h.le)
+            ((one_le_pow_iff_of_nonneg ha hn).mp h.ge),
+   fun h ↦ by rw [h]; exact one_pow _⟩
+
 theorem one_lt_pow_iff_of_nonneg {a : R} (ha : 0 ≤ a) {n : ℕ} (hn : n ≠ 0) : 1 < a ^ n ↔ 1 < a :=
   lt_iff_lt_of_le_iff_le (pow_le_one_iff_of_nonneg ha hn)
 #align one_lt_pow_iff_of_nonneg one_lt_pow_iff_of_nonneg

Mathlib/FieldTheory/Finite/Basic.lean

@@ -479,6 +479,11 @@ theorem Nat.ModEq.pow_totient {x n : ℕ} (h : Nat.Coprime x n) : x ^ φ n ≡ 1
     coe_unitOfCoprime, Units.val_pow_eq_pow_val]
 #align nat.modeq.pow_totient Nat.ModEq.pow_totient
 
+/-- For each `n ≥ 0`, the unit group of `ZMod n` is finite. -/
+instance instFiniteZModUnits : (n : ℕ) → Finite (ZMod n)ˣ
+| 0     => Finite.of_fintype ℤˣ
+| _ + 1 => instFiniteUnits
+
 section
 
 variable {V : Type*} [Fintype K] [DivisionRing K] [AddCommGroup V] [Module K V]

Mathlib/NumberTheory/DirichletCharacter/Bounds.lean

@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2023 Michael Stoll. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Stoll
+-/
+import Mathlib.Analysis.Normed.Field.Basic
+import Mathlib.FieldTheory.Finite.Basic
+import Mathlib.NumberTheory.DirichletCharacter.Basic
+
+/-!
+# Bounds for values of Dirichlet characters
+
+We consider Dirichlet characters `χ` with values in a normed field `F`.
+
+We show that `‖χ a‖ = 1` if `a` is a unit and `‖χ a‖ ≤ 1` in general.
+-/
+
+variable {F : Type*} [NormedField F] {n : ℕ} (χ : DirichletCharacter F n)
+
+namespace DirichletCharacter
+
+/-- The value at a unit of a Dirichlet character with target a normed field has norm `1`. -/
+@[simp] lemma unit_norm_eq_one (a : (ZMod n)ˣ) : ‖χ a‖ = 1 := by
+  refine (pow_eq_one_iff_of_nonneg (norm_nonneg _) (Nat.card_pos (α := (ZMod n)ˣ)).ne').mp ?_
+  rw [← norm_pow, ← map_pow, ← Units.val_pow_eq_pow_val, pow_card_eq_one', Units.val_one, map_one,
+    norm_one]
+
+/-- The values of a Dirichlet character with target a normed field have norm bounded by `1`. -/
+lemma norm_le_one (a : ZMod n) : ‖χ a‖ ≤ 1 := by
+  by_cases h : IsUnit a
+  · exact (χ.unit_norm_eq_one h.unit).le
+  · rw [χ.map_nonunit h, norm_zero]
+    exact zero_le_one
+
+
+end DirichletCharacter