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.

source
def AbsoluteValue.IsEquiv {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
    Instances For
      source
      theorem AbsoluteValue.isEquiv_refl {R : Type u_1} [Semiring R] (f : AbsoluteValue R ℝ) :
      f.IsEquiv f

      Equivalence of absolute values is reflexive.

      source
      theorem AbsoluteValue.isEquiv_symm {R : Type u_1} [Semiring R] {f g : AbsoluteValue R ℝ} (hfg : f.IsEquiv g) :
      g.IsEquiv f

      Equivalence of absolute values is symmetric.

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

      Equivalence of absolute values is transitive.

      source
      instance AbsoluteValue.instSetoidReal {R : Type u_1} [Semiring R] :
      Setoid (AbsoluteValue R ℝ)
      Equations
        source
        @[simp]
        theorem AbsoluteValue.eq_trivial_of_isEquiv_trivial {R : Type u_1} [Semiring R] [DecidablePred fun (x : R) => x = 0] [NoZeroDivisors R] (f : AbsoluteValue R ℝ) :
        f ≈ AbsoluteValue.trivial ↔ f = AbsoluteValue.trivial

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