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.

def AbsoluteValue.IsEquiv {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] [PartialOrder S] (v w : AbsoluteValue R S) : Prop

Two absolute values v and w are equivalent if v x ≤ v y precisely when w x ≤ w y.

Note that for real absolute values this condition is equivalent to the existence of a positive real number c such that v x ^ c = w x for all x. See AbsoluteValue.isEquiv_iff_exists_rpow_eq.

Equations

• v.IsEquiv w = ∀ (x y : R), v x ≤ v y ↔ w x ≤ w y

theorem AbsoluteValue.IsEquiv.refl {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] [PartialOrder S] (v : AbsoluteValue R S) : v.IsEquiv v

theorem AbsoluteValue.IsEquiv.rfl {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] [PartialOrder S] {v : AbsoluteValue R S} : v.IsEquiv v

theorem AbsoluteValue.IsEquiv.symm {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] [PartialOrder S] {v w : AbsoluteValue R S} (h : v.IsEquiv w) : w.IsEquiv v

theorem AbsoluteValue.IsEquiv.trans {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] [PartialOrder S] {v w u : AbsoluteValue R S} (h₁ : v.IsEquiv w) (h₂ : w.IsEquiv u) : v.IsEquiv u

@[deprecated AbsoluteValue.IsEquiv.refl (since := "2025-09-12")]

theorem AbsoluteValue.isEquiv_refl {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] [PartialOrder S] (v : AbsoluteValue R S) : v.IsEquiv v

Alias of AbsoluteValue.IsEquiv.refl.

@[deprecated AbsoluteValue.IsEquiv.symm (since := "2025-09-12")]

theorem AbsoluteValue.isEquiv_symm {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] [PartialOrder S] {v w : AbsoluteValue R S} (h : v.IsEquiv w) : w.IsEquiv v

Alias of AbsoluteValue.IsEquiv.symm.

@[deprecated AbsoluteValue.IsEquiv.trans (since := "2025-09-12")]

theorem AbsoluteValue.isEquiv_trans {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] [PartialOrder S] {v w u : AbsoluteValue R S} (h₁ : v.IsEquiv w) (h₂ : w.IsEquiv u) : v.IsEquiv u

Alias of AbsoluteValue.IsEquiv.trans.

@[implicit_reducible]

instance AbsoluteValue.instSetoid {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] [PartialOrder S] : Setoid (AbsoluteValue R S)

Equations

• AbsoluteValue.instSetoid = { r := AbsoluteValue.IsEquiv, iseqv := ⋯ }

theorem AbsoluteValue.IsEquiv.le_iff_le {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] [PartialOrder S] {v w : AbsoluteValue R S} (h : v.IsEquiv w) {x y : R} : v x ≤ v y ↔ w x ≤ w y

theorem AbsoluteValue.IsEquiv.lt_iff_lt {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] [PartialOrder S] {v w : AbsoluteValue R S} (h : v.IsEquiv w) {x y : R} : v x < v y ↔ w x < w y

theorem AbsoluteValue.IsEquiv.eq_iff_eq {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] [PartialOrder S] {v w : AbsoluteValue R S} (h : v.IsEquiv w) {x y : R} : v x = v y ↔ w x = w y

theorem AbsoluteValue.IsEquiv.lt_one_iff {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] [PartialOrder S] {v w : AbsoluteValue R S} [IsDomain S] [Nontrivial R] (h : v.IsEquiv w) {x : R} : v x < 1 ↔ w x < 1

theorem AbsoluteValue.IsEquiv.one_lt_iff {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] [PartialOrder S] {v w : AbsoluteValue R S} [IsDomain S] [Nontrivial R] (h : v.IsEquiv w) {x : R} : 1 < v x ↔ 1 < w x

theorem AbsoluteValue.IsEquiv.le_one_iff {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] [PartialOrder S] {v w : AbsoluteValue R S} [IsDomain S] [Nontrivial R] (h : v.IsEquiv w) {x : R} : v x ≤ 1 ↔ w x ≤ 1

theorem AbsoluteValue.IsEquiv.one_le_iff {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] [PartialOrder S] {v w : AbsoluteValue R S} [IsDomain S] [Nontrivial R] (h : v.IsEquiv w) {x : R} : 1 ≤ v x ↔ 1 ≤ w x

theorem AbsoluteValue.IsEquiv.eq_one_iff {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] [PartialOrder S] {v w : AbsoluteValue R S} [IsDomain S] [Nontrivial R] (h : v.IsEquiv w) {x : R} : v x = 1 ↔ w x = 1

theorem AbsoluteValue.IsEquiv.isNontrivial_congr {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] [PartialOrder S] {v : AbsoluteValue R S} [IsDomain S] [Nontrivial R] {w : AbsoluteValue R S} (h : v.IsEquiv w) : v.IsNontrivial ↔ w.IsNontrivial

theorem AbsoluteValue.IsEquiv.isNontrivial {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] [PartialOrder S] {v : AbsoluteValue R S} [IsDomain S] [Nontrivial R] {w : AbsoluteValue R S} (h : v.IsEquiv w) : v.IsNontrivial → w.IsNontrivial

Alias of the forward direction of AbsoluteValue.IsEquiv.isNontrivial_congr.

@[simp]

theorem AbsoluteValue.isEquiv_trivial_iff_eq_trivial {R : Type u_1} {S : Type u_2} [Field R] [Semifield S] [LinearOrder S] [DecidablePred fun (x : R) => x = 0] [NoZeroDivisors R] [IsStrictOrderedRing S] {f : AbsoluteValue R S} : f.IsEquiv AbsoluteValue.trivial ↔ f = AbsoluteValue.trivial

An absolute value is equivalent to the trivial iff it is trivial itself.

@[deprecated AbsoluteValue.isEquiv_trivial_iff_eq_trivial (since := "2025-09-12")]

theorem AbsoluteValue.eq_trivial_of_isEquiv_trivial {R : Type u_1} {S : Type u_2} [Field R] [Semifield S] [LinearOrder S] [DecidablePred fun (x : R) => x = 0] [NoZeroDivisors R] [IsStrictOrderedRing S] {f : AbsoluteValue R S} : f.IsEquiv AbsoluteValue.trivial ↔ f = AbsoluteValue.trivial

Alias of AbsoluteValue.isEquiv_trivial_iff_eq_trivial.

---

An absolute value is equivalent to the trivial iff it is trivial itself.

theorem AbsoluteValue.isEquiv_iff_lt_one_iff {R : Type u_1} {S : Type u_2} [Field R] [Semifield S] [LinearOrder S] {v w : AbsoluteValue R S} [IsStrictOrderedRing S] : v.IsEquiv w ↔ ∀ (x : R), v x < 1 ↔ w x < 1

theorem AbsoluteValue.isEquiv_of_lt_one_imp {R : Type u_1} {S : Type u_2} [Field R] [Semifield S] [LinearOrder S] {v w : AbsoluteValue R S} [IsStrictOrderedRing S] [Archimedean S] [ExistsAddOfLE S] (hv : v.IsNontrivial) (h : ∀ (x : R), v x < 1 → w x < 1) : v.IsEquiv w

theorem AbsoluteValue.exists_lt_one_one_le_of_not_isEquiv {R : Type u_1} {S : Type u_2} [Field R] [Semifield S] [LinearOrder S] [IsStrictOrderedRing S] [Archimedean S] [ExistsAddOfLE S] {v w : AbsoluteValue R S} (hv : v.IsNontrivial) (h : ¬v.IsEquiv w) : ∃ (a : R), v a < 1 ∧ 1 ≤ w a

If v and w are inequivalent absolute values and v is non-trivial, then we can find an a : R such that v a < 1 while 1 ≤ w a.

theorem AbsoluteValue.exists_one_lt_lt_one_of_not_isEquiv {R : Type u_1} {S : Type u_2} [Field R] [Semifield S] [LinearOrder S] [IsStrictOrderedRing S] [Archimedean S] [ExistsAddOfLE S] {v w : AbsoluteValue R S} (hv : v.IsNontrivial) (hw : w.IsNontrivial) (h : ¬v.IsEquiv w) : ∃ (a : R), 1 < v a ∧ w a < 1

If v and w are two non-trivial and inequivalent absolute values then we can find an a : R such that 1 < v a while w a < 1.

theorem AbsoluteValue.exists_one_lt_lt_one_pi_of_not_isEquiv {R : Type u_1} {S : Type u_2} [Field R] [Field S] [LinearOrder S] [TopologicalSpace S] [IsStrictOrderedRing S] [Archimedean S] [OrderTopology S] {ι : Type u_3} [Finite ι] {v : ι → AbsoluteValue R S} (h : ∀ (i : ι), (v i).IsNontrivial) (hv : Pairwise fun (i j : ι) => ¬(v i).IsEquiv (v j)) (i : ι) : ∃ (a : R), 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1

If v : ι → AbsoluteValue R S is a finite collection of non-trivial and pairwise inequivalent absolute values, then for any i there is some a : R such that 1 < v i a and v j a < 1 for all j ≠ i.

theorem AbsoluteValue.IsEquiv.log_div_log_pos {F : Type u_1} [Field F] {v w : AbsoluteValue F ℝ} (h : v.IsEquiv w) {a : F} (ha₀ : a ≠ 0) (ha₁ : w a ≠ 1) : 0 < Real.log (w a) / Real.log (v a)

theorem AbsoluteValue.IsEquiv.log_div_log_eq_log_div_log {F : Type u_1} [Field F] {v w : AbsoluteValue F ℝ} (h : v.IsEquiv w) {a : F} (ha₀ : a ≠ 0) (ha₁ : v a ≠ 1) {b : F} (hb₀ : b ≠ 0) (hb₁ : v b ≠ 1) : Real.log (v b) / Real.log (w b) = Real.log (v a) / Real.log (w a)

If $v$ and $w$ are two real absolute values on a field $F$, equivalent in the sense that $v(x) \leq v(y)$ if and only if $w(x) \leq w(y)$, then $\frac{\log (v(a))}{\log (w(a))}$ is constant for all $0 \neq a\in F$ with $v(a) \neq 1$.

theorem AbsoluteValue.isEquiv_iff_exists_rpow_eq {F : Type u_1} [Field F] {v w : AbsoluteValue F ℝ} : v.IsEquiv w ↔ ∃ (c : ℝ), 0 < c ∧ (fun (x : F) => v x ^ c) = ⇑w

If v and w are two real absolute values on a field F, then v and w are equivalent if and only if there exists a positive real constant c such that for all x : R, (f x)^c = g x.

theorem AbsoluteValue.IsEquiv.equivWithAbs_image_mem_nhds_zero {F : Type u_1} [Field F] {v w : AbsoluteValue F ℝ} (h : v.IsEquiv w) {U : Set (WithAbs v)} (hU : U ∈ nhds 0) : ⇑(WithAbs.congr v w (RingEquiv.refl F)) '' U ∈ nhds 0

theorem AbsoluteValue.IsEquiv.isEmbedding_equivWithAbs {F : Type u_1} [Field F] {v w : AbsoluteValue F ℝ} (h : v.IsEquiv w) : Topology.IsEmbedding ⇑(WithAbs.congr v w (RingEquiv.refl F))

theorem AbsoluteValue.isEquiv_iff_isHomeomorph {F : Type u_1} [Field F] (v w : AbsoluteValue F ℝ) : v.IsEquiv w ↔ IsHomeomorph ⇑(WithAbs.congr v w (RingEquiv.refl F))