Documentation

Mathlib.Analysis.AbsoluteValue.Equivalence

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) :

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
Instances For
    theorem AbsoluteValue.IsEquiv.refl {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] [PartialOrder S] (v : AbsoluteValue R S) :
    theorem AbsoluteValue.IsEquiv.rfl {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] [PartialOrder S] {v : AbsoluteValue R S} :
    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) :
    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) :
    @[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) :

    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) :

    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) :

    Alias of AbsoluteValue.IsEquiv.trans.

    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 {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) :

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

    @[simp]

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

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

    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 < 1w x < 1) :
    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.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.