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
.
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
.
Instances For
Alias of AbsoluteValue.IsEquiv.refl
.
Alias of AbsoluteValue.IsEquiv.symm
.
Alias of AbsoluteValue.IsEquiv.trans
.
Equations
- AbsoluteValue.instSetoid = { r := AbsoluteValue.IsEquiv, iseqv := ⋯ }
Alias of the forward direction of AbsoluteValue.IsEquiv.isNontrivial_congr
.
An absolute value is equivalent to the trivial iff it is trivial itself.
Alias of AbsoluteValue.isEquiv_trivial_iff_eq_trivial
.
An absolute value is equivalent to the trivial iff it is trivial itself.
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
.
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
.
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$.
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
.