Nonarchimedean functions

A function f : α → R is nonarchimedean if it satisfies the strong triangle inequality f (a + b) ≤ max (f a) (f b) for all a b : α. This file proves basic properties of nonarchimedean functions.

theorem IsNonarchimedean.add_le {R : Type u_1} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {α : Type u_2} [Add α] {f : α → R} (hf : ∀ (x : α), 0 ≤ f x) (hna : IsNonarchimedean f) {a b : α} : f (a + b) ≤ f a + f b

A nonnegative nonarchimedean function satisfies the triangle inequality.

theorem IsNonarchimedean.nsmul_le {R : Type u_1} [Semiring R] [LinearOrder R] {F : Type u_2} {α : Type u_3} [AddMonoid α] [FunLike F α R] [ZeroHomClass F α R] [NonnegHomClass F α R] {f : F} (hna : IsNonarchimedean ⇑f) {n : ℕ} {a : α} : f (n • a) ≤ f a

If f is a nonnegative nonarchimedean function α → R such that f 0 = 0, then for every n : ℕ and a : α, we have f (n • a) ≤ (f a).

theorem IsNonarchimedean.nmul_le {R : Type u_1} [Semiring R] [LinearOrder R] {F : Type u_2} {α : Type u_3} [NonAssocSemiring α] [FunLike F α R] [ZeroHomClass F α R] [NonnegHomClass F α R] {f : F} (hna : IsNonarchimedean ⇑f) {n : ℕ} {a : α} : f (↑n * a) ≤ f a

If f is a nonnegative nonarchimedean function α → R such that f 0 = 0, then for every n : ℕ and a : α, we have f (n * a) ≤ (f a).

theorem IsNonarchimedean.apply_natCast_le_one {R : Type u_1} [Semiring R] [LinearOrder R] {F : Type u_2} {α : Type u_3} [AddMonoidWithOne α] [FunLike F α R] [ZeroHomClass F α R] [NonnegHomClass F α R] [OneHomClass F α R] {f : F} (hna : IsNonarchimedean ⇑f) {n : ℕ} : f ↑n ≤ 1

@[deprecated IsNonarchimedean.apply_natCast_le_one (since := "2026-04-27")]

theorem IsNonarchimedean.apply_natCast_le_one_of_isNonarchimedean {R : Type u_1} [Semiring R] [LinearOrder R] {F : Type u_2} {α : Type u_3} [AddMonoidWithOne α] [FunLike F α R] [ZeroHomClass F α R] [NonnegHomClass F α R] [OneHomClass F α R] {f : F} (hna : IsNonarchimedean ⇑f) {n : ℕ} : f ↑n ≤ 1

Alias of IsNonarchimedean.apply_natCast_le_one.

theorem IsNonarchimedean.apply_intCast_le_one {R : Type u_1} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {F : Type u_2} {α : Type u_3} [AddGroupWithOne α] [FunLike F α R] [AddGroupSeminormClass F α R] [OneHomClass F α R] {f : F} (hna : IsNonarchimedean ⇑f) {n : ℤ} : f ↑n ≤ 1

If f is a nonarchimedean additive group seminorm on α with f 1 = 1, then for every n : ℤ we have f n ≤ 1.

@[deprecated IsNonarchimedean.apply_intCast_le_one (since := "2026-04-27")]

theorem IsNonarchimedean.apply_intCast_le_one_of_isNonarchimedean {R : Type u_1} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {F : Type u_2} {α : Type u_3} [AddGroupWithOne α] [FunLike F α R] [AddGroupSeminormClass F α R] [OneHomClass F α R] {f : F} (hna : IsNonarchimedean ⇑f) {n : ℤ} : f ↑n ≤ 1

Alias of IsNonarchimedean.apply_intCast_le_one.

---

If f is a nonarchimedean additive group seminorm on α with f 1 = 1, then for every n : ℤ we have f n ≤ 1.

theorem IsNonarchimedean.add_eq_right_of_lt {R : Type u_1} [Semiring R] [LinearOrder R] {F : Type u_2} {α : Type u_3} [AddGroup α] [FunLike F α R] [AddGroupSeminormClass F α R] {f : F} (hna : IsNonarchimedean ⇑f) {x y : α} (h_lt : f x < f y) : f (x + y) = f y

theorem IsNonarchimedean.add_eq_left_of_lt {R : Type u_1} [Semiring R] [LinearOrder R] {F : Type u_2} {α : Type u_3} [AddGroup α] [FunLike F α R] [AddGroupSeminormClass F α R] {f : F} (hna : IsNonarchimedean ⇑f) {x y : α} (h_lt : f y < f x) : f (x + y) = f x

theorem IsNonarchimedean.add_eq_max_of_ne {R : Type u_1} [Semiring R] [LinearOrder R] {F : Type u_2} {α : Type u_3} [AddGroup α] [FunLike F α R] [AddGroupSeminormClass F α R] {f : F} (hna : IsNonarchimedean ⇑f) {x y : α} (hne : f x ≠ f y) : f (x + y) = max (f x) (f y)

If f is a nonarchimedean additive group seminorm on α and x y : α are such that f x ≠ f y, then f (x + y) = max (f x) (f y).

theorem IsNonarchimedean.add_eq_max_of_ne' {α : Type u_2} {S : Type u_3} [LinearOrder S] [AddCommGroup α] (f : α → S) (fna : IsNonarchimedean f) (Neg : ∀ (a : α), f a = f (-a)) {a b : α} (hne : f a ≠ f b) : f (a + b) = max (f a) (f b)

theorem IsNonarchimedean.apply_sum_le_sup {R : Type u_1} [LinearOrder R] {α : Type u_2} {β : Type u_3} [AddCommMonoid α] {f : α → R} (nonarch : IsNonarchimedean f) {s : Finset β} (hnonempty : s.Nonempty) {l : β → α} : f (∑ i ∈ s, l i) ≤ s.sup' hnonempty fun (i : β) => f (l i)

Ultrametric inequality with Finset.sum.

@[deprecated IsNonarchimedean.apply_sum_le_sup (since := "2026-04-27")]

theorem IsNonarchimedean.apply_sum_le_sup_of_isNonarchimedean {R : Type u_1} [LinearOrder R] {α : Type u_2} {β : Type u_3} [AddCommMonoid α] {f : α → R} (nonarch : IsNonarchimedean f) {s : Finset β} (hnonempty : s.Nonempty) {l : β → α} : f (∑ i ∈ s, l i) ≤ s.sup' hnonempty fun (i : β) => f (l i)

Alias of IsNonarchimedean.apply_sum_le_sup.

---

Ultrametric inequality with Finset.sum.

theorem IsNonarchimedean.multiset_image_add_of_nonempty {R : Type u_1} [LinearOrder R] {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [Nonempty β] {f : α → R} (hna : IsNonarchimedean f) (g : β → α) {s : Multiset β} (hs : s ≠ 0) : ∃ b ∈ s, f (Multiset.map g s).sum ≤ f (g b)

Given a nonarchimedean function α → R, a function g : β → α and a nonempty multiset s : Multiset β, we can always find b : β belonging to s such that f (t.sum g) ≤ f (g b) .

theorem IsNonarchimedean.finset_image_add_of_nonempty {R : Type u_1} [LinearOrder R] {α : Type u_2} {β : Type u_3} [AddCommMonoid α] {f : α → R} (hna : IsNonarchimedean f) (g : β → α) {t : Finset β} (ht : t.Nonempty) : ∃ b ∈ t, f (t.sum g) ≤ f (g b)

Given a nonarchimedean function α → R, a function g : β → α and a nonempty finset t : Finset β, we can always find b : β belonging to t such that f (t.sum g) ≤ f (g b) .

theorem IsNonarchimedean.multiset_image_add {R : Type u_1} [Semiring R] [LinearOrder R] {F : Type u_2} {α : Type u_3} {β : Type u_4} [AddCommMonoid α] [FunLike F α R] [ZeroHomClass F α R] [NonnegHomClass F α R] [Nonempty β] {f : F} (hna : IsNonarchimedean ⇑f) (g : β → α) (s : Multiset β) : ∃ (b : β), (s ≠ 0 → b ∈ s) ∧ f (Multiset.map g s).sum ≤ f (g b)

Given a nonnegative nonarchimedean function α → R such that f 0 = 0, a function g : β → α and a multiset s : Multiset β, we can always find b : β, belonging to s if s is nonempty, such that f (s.sum g) ≤ f (g b) .

theorem IsNonarchimedean.finset_image_add {R : Type u_1} [Semiring R] [LinearOrder R] {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [Nonempty β] {f : α → R} (f_zero : f 0 = 0) (f_nonneg : ∀ (x : α), 0 ≤ f x) (hna : IsNonarchimedean f) (g : β → α) (t : Finset β) : ∃ (i : β), (t.Nonempty → i ∈ t) ∧ f (t.sum g) ≤ f (g i)

Given a nonnegative nonarchimedean function α → R such that f 0 = 0, a function g : β → α and a finset t : Finset β, we can always find b : β, belonging to t if t is nonempty, such that f (t.sum g) ≤ f (g b) .

theorem IsNonarchimedean.multiset_powerset_image_add {R : Type u_1} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {F : Type u_2} {α : Type u_3} [CommRing α] [FunLike F α R] [AddGroupSeminormClass F α R] {f : F} (hf_na : IsNonarchimedean ⇑f) (s : Multiset α) (m : ℕ) : ∃ (t : Multiset α), t.card = s.card - m ∧ (∀ x ∈ t, x ∈ s) ∧ f (Multiset.map Multiset.prod (Multiset.powersetCard (s.card - m) s)).sum ≤ f t.prod

theorem IsNonarchimedean.finset_powerset_image_add {R : Type u_1} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {F : Type u_2} {α : Type u_3} {β : Type u_4} [CommRing α] [FunLike F α R] [AddGroupSeminormClass F α R] {f : F} (hf_na : IsNonarchimedean ⇑f) (s : Finset β) (b : β → α) (m : ℕ) : ∃ (u : ↥(Finset.powersetCard (s.card - m) s)), f (∑ t ∈ Finset.powersetCard (s.card - m) s, ∏ i ∈ t, -b i) ≤ f (∏ i ∈ ↑u, -b i)

theorem IsNonarchimedean.apply_sum_eq_of_lt {R : Type u_1} [LinearOrder R] {α : Type u_2} {β : Type u_3} [AddCommGroup α] {f : α → R} (fna : IsNonarchimedean f) (f_neg : ∀ (a : α), f a = f (-a)) {s : Finset β} {l : β → α} {k : β} (hk : k ∈ s) (hmax : ∀ j ∈ s, j ≠ k → f (l j) < f (l k)) : f (∑ i ∈ s, l i) = f (l k)

theorem IsNonarchimedean.add_pow_le {R : Type u_1} [Semiring R] [LinearOrder R] {F : Type u_2} {α : Type u_3} [CommRing α] [FunLike F α R] [ZeroHomClass F α R] [NonnegHomClass F α R] [SubmultiplicativeHomClass F α R] {f : F} (hna : IsNonarchimedean ⇑f) (n : ℕ) (a b : α) : ∃ m < n + 1, f ((a + b) ^ n) ≤ f (a ^ m) * f (b ^ (n - m))

If f is a nonarchimedean additive group seminorm on a commutative ring α, n : ℕ, and a b : α, then we can find m : ℕ such that m ≤ n and f ((a + b) ^ n) ≤ (f (a ^ m)) * (f (b ^ (n - m))).