Comparing norm-compatible additive valuations

Two real additive valuations recovering the same norm with specified bases greater than one differ by the ratio of the logarithms of those bases. The comparison includes zero, whose value remains infinity. In particular, fixing the base determines the additive valuation uniquely; no choice of scale is installed as a global instance. Under norm recovery, the sphere ‖x‖ = b ^ σ is the level set v x = -σ (AddValuation.norm_eq_rpow_iff). A norm recovered from an additive valuation with base at least one is ultrametric (AddValuation.isUltrametricDist).

theorem AddValuation.eq_map_of_norm_eq_rpow {K : Type u_1} [NormedDivisionRing K] (v w : AddValuation K (WithTop ℝ)) {b b' : ℝ} (hb : 1 < b) (hb' : 1 < b') (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) (hw : ∀ (x : K), x ≠ 0 → ‖x‖ = b' ^ (-(w x).untop₀)) (x : K) : w x = WithTop.map (fun (t : ℝ) => Real.log b / Real.log b' * t) (v x)

Changing the base in norm recovery scales a real additive valuation by the ratio of the logarithms. At zero the comparison maps infinity to infinity.

theorem AddValuation.eq_of_norm_eq_rpow {K : Type u_1} [NormedDivisionRing K] (v w : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) (hw : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(w x).untop₀)) : w = v

For a fixed base greater than one, norm recovery uniquely specifies the real additive valuation.

theorem AddValuation.norm_eq_rpow_iff {K : Type u_1} [NormedDivisionRing K] (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) {x : K} {σ : ℝ} : ‖x‖ = b ^ σ ↔ v x = ↑(-σ)

Under norm recovery with base b > 1, the points of norm b ^ σ are exactly those of valuation -σ. Zero lies on neither side.

theorem AddValuation.isUltrametricDist {K : Type u_1} [NormedDivisionRing K] (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 ≤ b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) : IsUltrametricDist K

A norm that is given by an additive valuation, ‖x‖ = b ^ (-v x) for x ≠ 0 with 1 ≤ b, is ultrametric.