refactor(NumberTheory/Ostrowski): use AbsoluteValue instead of MulRingNorm (#20362)

This PR
* replaces `MulRingNorm R` by `AbsoluteValue R ℝ` in the material developed in `Mathlib.NumberTheory.Ostrowski`
* does some cleanup (naming convention, remove redundant name parts etc.)
* and also some golfing...

In addition, it
* creates a new folder `Mathlib.Algebra.Order.AbsoluteValue`
* moves `Mathlib.Algebra.Order.AbsoluteValue` to `Mathlib.Algebra.Order.AbsoluteValue.Basic` and `Mathlib.Algebra.Order.EuclideanAbsoluteValue`to `Mathlib.Algebra.Order.AbsoluteValue.Euclidean`
* adds some API for `AbsoluteValue` to match `MulRingNorm` (in `Mathlib.Algebra.Order.AbsoluteValue.Basic`)
* adds a new file `Mathlib.Algebra.Order.AbsoluteValue.Equivalence` with material on equivalence of real-valued absolute values.

See the [discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/MulRingNorm.20vs.2E.20AbsoluteValue/near/491324423) on Zulip.



Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com>

Author: MichaelStollBayreuth

Mathlib.lean

@@ -628,7 +628,9 @@ import Mathlib.Algebra.NoZeroSMulDivisors.Pi
 import Mathlib.Algebra.NoZeroSMulDivisors.Prod
 import Mathlib.Algebra.Notation
 import Mathlib.Algebra.Opposites
-import Mathlib.Algebra.Order.AbsoluteValue
+import Mathlib.Algebra.Order.AbsoluteValue.Basic
+import Mathlib.Algebra.Order.AbsoluteValue.Equivalence
+import Mathlib.Algebra.Order.AbsoluteValue.Euclidean
 import Mathlib.Algebra.Order.AddGroupWithTop
 import Mathlib.Algebra.Order.AddTorsor
 import Mathlib.Algebra.Order.Algebra
@@ -654,7 +656,6 @@ import Mathlib.Algebra.Order.CauSeq.BigOperators
 import Mathlib.Algebra.Order.CauSeq.Completion
 import Mathlib.Algebra.Order.Chebyshev
 import Mathlib.Algebra.Order.CompleteField
-import Mathlib.Algebra.Order.EuclideanAbsoluteValue
 import Mathlib.Algebra.Order.Field.Basic
 import Mathlib.Algebra.Order.Field.Canonical.Basic
 import Mathlib.Algebra.Order.Field.Canonical.Defs

Mathlib/Algebra/Order/AbsoluteValue.lean renamed to Mathlib/Algebra/Order/AbsoluteValue/Basic.lean

@@ -93,6 +93,12 @@ protected theorem eq_zero {x : R} : abv x = 0 ↔ x = 0 :=
 protected theorem add_le (x y : R) : abv (x + y) ≤ abv x + abv y :=
   abv.add_le' x y
 
+/-- The triangle inequality for an `AbsoluteValue` applied to a list. -/
+lemma listSum_le (l : List R) : abv l.sum ≤ (l.map abv).sum := by
+  induction l with
+  | nil => simp
+  | cons head tail ih => exact (abv.add_le ..).trans <| add_le_add_left ih (abv head)
+
 @[simp]
 protected theorem map_mul (x y : R) : abv (x * y) = abv x * abv y :=
   abv.map_mul' x y
@@ -174,6 +180,20 @@ theorem coe_toMonoidHom : ⇑abv.toMonoidHom = abv :=
 protected theorem map_pow (a : R) (n : ℕ) : abv (a ^ n) = abv a ^ n :=
   abv.toMonoidHom.map_pow a n
 
+omit [Nontrivial R] in
+/-- An absolute value satisfies `f (n : R) ≤ n` for every `n : ℕ`. -/
+lemma apply_nat_le_self (n : ℕ) : abv n ≤ n := by
+  cases subsingleton_or_nontrivial R
+  · simp [Subsingleton.eq_zero (n : R)]
+  induction n with
+  | zero => simp
+  | succ n hn =>
+    simp only [Nat.cast_succ]
+    calc
+      abv (n + 1) ≤ abv n + abv 1 := abv.add_le ..
+      _ = abv n + 1 := congrArg (abv n + ·) abv.map_one
+      _ ≤ n + 1 := add_le_add_right hn 1
+
 end IsDomain
 
 end Semiring
@@ -191,8 +211,8 @@ end Ring
 end OrderedRing
 
 section OrderedCommRing
-variable [OrderedCommRing S] [Ring R] (abv : AbsoluteValue R S)
-variable [NoZeroDivisors S]
+
+variable [OrderedCommRing S] [Ring R] (abv : AbsoluteValue R S) [NoZeroDivisors S]
 
 @[simp]
 protected theorem map_neg (a : R) : abv (-a) = abv a := by
@@ -219,6 +239,18 @@ instance [Nontrivial R] [IsDomain S] : MulRingNormClass (AbsoluteValue R S) R S
     map_neg_eq_map := fun f => f.map_neg
     eq_zero_of_map_eq_zero := fun f _ => f.eq_zero.1 }
 
+open Int in
+lemma apply_natAbs_eq (x : ℤ) : abv (natAbs x) = abv x := by
+  obtain ⟨_, rfl | rfl⟩ := eq_nat_or_neg x <;> simp
+
+open Int in
+/-- Values of an absolute value coincide on the image of `ℕ` in `R`
+if and only if they coincide on the image of `ℤ` in `R`. -/
+lemma eq_on_nat_iff_eq_on_int {f g : AbsoluteValue R S} :
+    (∀ n : ℕ , f n = g n) ↔ ∀ n : ℤ , f n = g n := by
+  refine ⟨fun h z ↦ ?_, fun a n ↦ mod_cast a n⟩
+  obtain ⟨n , rfl | rfl⟩ := eq_nat_or_neg z <;> simp [h n]
+
 end OrderedCommRing
 
 section LinearOrderedRing
@@ -249,6 +281,37 @@ theorem abs_abv_sub_le_abv_sub (a b : R) : abs (abv a - abv b) ≤ abv (a - b) :
 
 end LinearOrderedCommRing
 
+section trivial
+
+variable {R : Type*} [Semiring R] [DecidablePred fun x : R ↦ x = 0] [NoZeroDivisors R]
+variable {S : Type*} [OrderedSemiring S] [Nontrivial S]
+
+/-- The *trivial* absolute value takes the value `1` on all nonzero elements. -/
+protected
+def trivial: AbsoluteValue R S where
+  toFun x := if x = 0 then 0 else 1
+  map_mul' x y := by
+    rcases eq_or_ne x 0 with rfl | hx
+    · simp
+    rcases eq_or_ne y 0 with rfl | hy
+    · simp
+    simp [hx, hy]
+  nonneg' x := by rcases eq_or_ne x 0 with hx | hx <;> simp [hx]
+  eq_zero' x := by rcases eq_or_ne x 0 with hx | hx <;> simp [hx]
+  add_le' x y := by
+    rcases eq_or_ne x 0 with rfl | hx
+    · simp
+    rcases eq_or_ne y 0 with rfl | hy
+    · simp
+    simp only [hx, ↓reduceIte, hy, one_add_one_eq_two]
+    rcases eq_or_ne (x + y) 0 with hxy | hxy <;> simp [hxy, one_le_two]
+
+@[simp]
+lemma trivial_apply {x : R} (hx : x ≠ 0) : AbsoluteValue.trivial (S := S) x = 1 :=
+  if_neg hx
+
+end trivial
+
 end AbsoluteValue
 
 -- Porting note: Removed [] in fields, see

Mathlib/Algebra/Order/AbsoluteValue/Equivalence.lean

@@ -0,0 +1,62 @@
+/-
+Copyright (c) 2025 Michael Stoll. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Stoll
+-/
+import Mathlib.Analysis.SpecialFunctions.Pow.Real
+
+/-!
+# Equivalence of real-valued absolute values
+
+Two absolute values `v₁, v₂ : AbsoluteValue R ℝ` are *equivalent* if there exists a
+positive real number `c` such that `v₁ x ^ c = v₂ x` for all `x : R`.
+-/
+
+namespace AbsoluteValue
+
+variable {R : Type*} [Semiring R]
+
+/-- Two absolute values `f, g` on `R` with values in `ℝ` are *equivalent* if there exists
+a positive real constant `c` such that for all `x : R`, `(f x)^c = g x`. -/
+def Equiv (f g : AbsoluteValue R ℝ) : Prop :=
+  ∃ c : ℝ, 0 < c ∧ (f · ^ c) = g
+
+/-- Equivalence of absolute values is reflexive. -/
+lemma equiv_refl (f : AbsoluteValue R ℝ) : Equiv f f :=
+  ⟨1, Real.zero_lt_one, funext fun x ↦ Real.rpow_one (f x)⟩
+
+/-- Equivalence of absolute values is symmetric. -/
+lemma equiv_symm {f g : AbsoluteValue R ℝ} (hfg : Equiv f g) : Equiv g f := by
+  rcases hfg with ⟨c, hcpos, h⟩
+  refine ⟨1 / c, one_div_pos.mpr hcpos, ?_⟩
+  simp [← h, Real.rpow_rpow_inv (apply_nonneg f _) (ne_of_lt hcpos).symm]
+
+/-- Equivalence of absolute values is transitive. -/
+lemma equiv_trans {f g k : AbsoluteValue R ℝ} (hfg : Equiv f g) (hgk : Equiv g k) :
+    Equiv f k := by
+  rcases hfg with ⟨c, hcPos, hfg⟩
+  rcases hgk with ⟨d, hdPos, hgk⟩
+  refine ⟨c * d, mul_pos hcPos hdPos, ?_⟩
+  simp [← hgk, ← hfg, Real.rpow_mul (apply_nonneg f _)]
+
+/-- An absolute value is equivalent to the trivial iff it is trivial itself. -/
+@[simp]
+lemma eq_trivial_of_equiv_trivial [DecidablePred fun x : R ↦ x = 0] [NoZeroDivisors R]
+    (f : AbsoluteValue R ℝ) :
+    f.Equiv .trivial ↔ f = .trivial := by
+  refine ⟨fun ⟨c, hc₀, hc⟩ ↦ ext fun x ↦ ?_, fun H ↦ H ▸ equiv_refl f⟩
+  apply_fun (· x) at hc
+  rcases eq_or_ne x 0 with rfl | hx
+  · simp
+  · simp only [ne_eq, hx, not_false_eq_true, trivial_apply] at hc ⊢
+    exact (Real.rpow_left_inj (f.nonneg x) zero_le_one hc₀.ne').mp <| (Real.one_rpow c).symm ▸ hc
+
+instance : Setoid (AbsoluteValue R ℝ) where
+  r := Equiv
+  iseqv := {
+    refl := equiv_refl
+    symm := equiv_symm
+    trans := equiv_trans
+  }
+
+end AbsoluteValue

Mathlib/Algebra/Order/EuclideanAbsoluteValue.lean renamed to Mathlib/Algebra/Order/AbsoluteValue/Euclidean.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Anne Baanen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen
 -/
-import Mathlib.Algebra.Order.AbsoluteValue
+import Mathlib.Algebra.Order.AbsoluteValue.Basic
 import Mathlib.Algebra.EuclideanDomain.Int
 
 /-!

Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
 import Mathlib.Algebra.BigOperators.Ring
-import Mathlib.Algebra.Order.AbsoluteValue
+import Mathlib.Algebra.Order.AbsoluteValue.Basic
 import Mathlib.Algebra.Order.BigOperators.Group.Finset
 import Mathlib.Algebra.Order.BigOperators.Ring.Multiset
 import Mathlib.Tactic.Ring

Mathlib/Algebra/Order/CauSeq/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Mathlib.Algebra.Group.Action.Pi
-import Mathlib.Algebra.Order.AbsoluteValue
+import Mathlib.Algebra.Order.AbsoluteValue.Basic
 import Mathlib.Algebra.Order.Field.Basic
 import Mathlib.Algebra.Order.Group.MinMax
 import Mathlib.Algebra.Ring.Pi

Mathlib/Algebra/Polynomial/Degree/CardPowDegree.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Anne Baanen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen
 -/
-import Mathlib.Algebra.Order.EuclideanAbsoluteValue
+import Mathlib.Algebra.Order.AbsoluteValue.Euclidean
 import Mathlib.Algebra.Order.Ring.Basic
 import Mathlib.Algebra.Polynomial.FieldDivision
 

Mathlib/Analysis/Normed/Ring/WithAbs.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Salvatore Mercuri
 -/
 import Mathlib.Algebra.Group.Basic
-import Mathlib.Algebra.Order.AbsoluteValue
+import Mathlib.Algebra.Order.AbsoluteValue.Basic
 import Mathlib.Analysis.Normed.Field.Basic
 import Mathlib.Analysis.Normed.Module.Completion
 

Mathlib/Data/Int/AbsoluteValue.lean

@@ -5,7 +5,7 @@ Authors: Anne Baanen
 -/
 import Mathlib.Algebra.GroupWithZero.Action.Units
 import Mathlib.Algebra.Module.Basic
-import Mathlib.Algebra.Order.AbsoluteValue
+import Mathlib.Algebra.Order.AbsoluteValue.Basic
 import Mathlib.Algebra.Ring.Int.Units
 import Mathlib.Data.Int.Cast.Lemmas
 

Mathlib/NumberTheory/ClassNumber/AdmissibleAbsoluteValue.lean

@@ -5,7 +5,7 @@ Authors: Anne Baanen
 -/
 import Mathlib.Data.Real.Basic
 import Mathlib.Combinatorics.Pigeonhole
-import Mathlib.Algebra.Order.EuclideanAbsoluteValue
+import Mathlib.Algebra.Order.AbsoluteValue.Euclidean
 
 /-!
 # Admissible absolute values