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.Equiv {R : Type u_1} [Semiring R] (f g : AbsoluteValue R ℝ) : Prop

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.

Equations

• f.Equiv g = ∃ (c : ℝ), 0 < c ∧ (fun (x : R) => f x ^ c) = ⇑g

theorem AbsoluteValue.equiv_refl {R : Type u_1} [Semiring R] (f : AbsoluteValue R ℝ) : f.Equiv f

Equivalence of absolute values is reflexive.

theorem AbsoluteValue.equiv_symm {R : Type u_1} [Semiring R] {f g : AbsoluteValue R ℝ} (hfg : f.Equiv g) : g.Equiv f

Equivalence of absolute values is symmetric.

theorem AbsoluteValue.equiv_trans {R : Type u_1} [Semiring R] {f g k : AbsoluteValue R ℝ} (hfg : f.Equiv g) (hgk : g.Equiv k) : f.Equiv k

Equivalence of absolute values is transitive.

@[simp]

theorem AbsoluteValue.eq_trivial_of_equiv_trivial {R : Type u_1} [Semiring R] [DecidablePred fun (x : R) => x = 0] [NoZeroDivisors R] (f : AbsoluteValue R ℝ) : f.Equiv AbsoluteValue.trivial ↔ f = AbsoluteValue.trivial

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

instance AbsoluteValue.instSetoidReal {R : Type u_1} [Semiring R] : Setoid (AbsoluteValue R ℝ)

Equations

• AbsoluteValue.instSetoidReal = { r := AbsoluteValue.Equiv, iseqv := ⋯ }