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 {α : Type u_1} {R : Type u_3} {a b : α} [LinearOrder R] {f : α → R} [Semiring R] [IsStrictOrderedRing R] [Add α] (f_nonneg : ∀ (x : α), 0 ≤ f x) (hna : IsNonarchimedean f) : f (a + b) ≤ f a + f b

A nonnegative nonarchimedean function satisfies the triangle inequality.

theorem IsNonarchimedean.nsmul_le {α : Type u_1} {R : Type u_3} {a : α} [LinearOrder R] {f : α → R} {n : ℕ} [AddMonoid α] (hna : IsNonarchimedean f) (f_zero_le : f 0 ≤ f a) : f (n • a) ≤ f a

If f : α → R is nonarchimedean and f 0 ≤ f a, then f (n • a) ≤ f a for every n : ℕ.

theorem IsNonarchimedean.nsmul_le_of_pos {α : Type u_1} {R : Type u_3} {a : α} [LinearOrder R] {f : α → R} {n : ℕ} [AddMonoid α] (hna : IsNonarchimedean f) (hn : 0 < n) : f (n • a) ≤ f a

If f : α → R is nonarchimedean, then f (n • a) ≤ f a for every positive n : ℕ.

theorem IsNonarchimedean.nmul_le {α : Type u_1} {R : Type u_3} {a : α} [LinearOrder R] {f : α → R} {n : ℕ} [NonAssocSemiring α] (hna : IsNonarchimedean f) (f_zero_le : f 0 ≤ f a) : f (↑n * a) ≤ f a

If f : α → R is nonarchimedean and f 0 ≤ f a, then f (n * a) ≤ f a for every n : ℕ.

theorem IsNonarchimedean.nmul_le_of_pos {α : Type u_1} {R : Type u_3} [LinearOrder R] {f : α → R} {n : ℕ} [NonAssocSemiring α] (hna : IsNonarchimedean f) (a : α) (hn : 0 < n) : f (↑n * a) ≤ f a

If f : α → R is nonarchimedean, then f (n * a) ≤ f a for every positive n : ℕ.

theorem IsNonarchimedean.add_eq_right_of_lt {α : Type u_1} {R : Type u_3} {a b : α} [LinearOrder R] {f : α → R} [AddGroup α] (f_neg : ∀ (a : α), f (-a) = f a) (h_lt : f a < f b) (hna : IsNonarchimedean f) : f (a + b) = f b

theorem IsNonarchimedean.add_eq_left_of_lt {α : Type u_1} {R : Type u_3} {a b : α} [LinearOrder R] {f : α → R} [AddGroup α] (f_neg : ∀ (a : α), f (-a) = f a) (h_lt : f a < f b) (hna : IsNonarchimedean f) : f (b + a) = f b

theorem IsNonarchimedean.add_eq_max_of_ne {α : Type u_1} {R : Type u_3} {a b : α} [LinearOrder R] {f : α → R} [AddGroup α] (f_neg : ∀ (a : α), f (-a) = f a) (hna : IsNonarchimedean f) (hne : f a ≠ f b) : f (a + b) = max (f a) (f b)

If f : α → R is nonarchimedean and invariant under negation, and f a ≠ f b, then f (a + b) = max (f a) (f b).

@[deprecated IsNonarchimedean.add_eq_max_of_ne (since := "2026-08-16")]

theorem IsNonarchimedean.add_eq_max_of_ne' {α : Type u_1} {R : Type u_3} {a b : α} [LinearOrder R] {f : α → R} [AddGroup α] (f_neg : ∀ (a : α), f (-a) = f a) (hna : IsNonarchimedean f) (hne : f a ≠ f b) : f (a + b) = max (f a) (f b)

Alias of IsNonarchimedean.add_eq_max_of_ne.

---

If f : α → R is nonarchimedean and invariant under negation, and f a ≠ f b, then f (a + b) = max (f a) (f b).

theorem IsNonarchimedean.apply_natCast_le_one {α : Type u_1} {R : Type u_3} [LinearOrder R] {f : α → R} {n : ℕ} [AddMonoidWithOne α] [One R] (f_zero_le : f 0 ≤ f 1) (f_one : f 1 = 1) (hna : IsNonarchimedean f) : f ↑n ≤ 1

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

theorem IsNonarchimedean.apply_natCast_le_one_of_isNonarchimedean {α : Type u_1} {R : Type u_3} [LinearOrder R] {f : α → R} {n : ℕ} [AddMonoidWithOne α] [One R] (f_zero_le : f 0 ≤ f 1) (f_one : f 1 = 1) (hna : IsNonarchimedean f) : f ↑n ≤ 1

Alias of IsNonarchimedean.apply_natCast_le_one.

theorem IsNonarchimedean.apply_intCast_le_one {α : Type u_1} {R : Type u_3} [LinearOrder R] {f : α → R} [One R] [AddGroupWithOne α] (f_zero_le : f 0 ≤ f 1) (f_one : f 1 = 1) (f_neg : ∀ (a : α), f (-a) = f a) (hna : IsNonarchimedean f) {n : ℤ} : f ↑n ≤ 1

If f : α → R is nonarchimedean, maps one to one, is invariant under negation, and f 0 ≤ f 1, then f n ≤ 1 for every n : ℤ.

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

theorem IsNonarchimedean.apply_intCast_le_one_of_isNonarchimedean {α : Type u_1} {R : Type u_3} [LinearOrder R] {f : α → R} [One R] [AddGroupWithOne α] (f_zero_le : f 0 ≤ f 1) (f_one : f 1 = 1) (f_neg : ∀ (a : α), f (-a) = f a) (hna : IsNonarchimedean f) {n : ℤ} : f ↑n ≤ 1

Alias of IsNonarchimedean.apply_intCast_le_one.

---

If f : α → R is nonarchimedean, maps one to one, is invariant under negation, and f 0 ≤ f 1, then f n ≤ 1 for every n : ℤ.

theorem IsNonarchimedean.multiset_image_add_of_nonempty {α : Type u_1} {β : Type u_2} {R : Type u_3} [LinearOrder R] {f : α → R} (g : β → α) [AddCommMonoid α] (hna : IsNonarchimedean f) {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.multiset_image_add {α : Type u_1} {β : Type u_2} {R : Type u_3} [LinearOrder R] {f : α → R} (g : β → α) [AddCommMonoid α] (hna : IsNonarchimedean f) [Nonempty β] (s : Multiset β) (f_zero_le : ∀ (x : α), f 0 ≤ f x) : ∃ (b : β), (s ≠ 0 → b ∈ s) ∧ f (Multiset.map g s).sum ≤ f (g b)

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

theorem IsNonarchimedean.multiset_powerset_image_add {α : Type u_1} {R : Type u_3} [LinearOrder R] {f : α → R} [AddCommMonoid α] (hna : IsNonarchimedean f) (n : ℕ) [CommMonoid α] (s : Multiset α) : ∃ (t : Multiset α), t.card = s.card - n ∧ (∀ x ∈ t, x ∈ s) ∧ f (Multiset.map Multiset.prod (Multiset.powersetCard (s.card - n) s)).sum ≤ f t.prod

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

Ultrametric inequality with Finset.sum.

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

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

Alias of IsNonarchimedean.apply_sum_le_sup.

---

Ultrametric inequality with Finset.sum.

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

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

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

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

theorem IsNonarchimedean.finset_powerset_image_add {α : Type u_1} {β : Type u_2} {R : Type u_3} [LinearOrder R] {f : α → R} {n : ℕ} (g : β → α) [AddCommMonoid α] (hna : IsNonarchimedean f) (s : Finset β) [CommMonoid α] : ∃ (u : ↥(Finset.powersetCard (s.card - n) s)), f (∑ t ∈ Finset.powersetCard (s.card - n) s, ∏ i ∈ t, g i) ≤ f (∏ i ∈ ↑u, g i)

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

theorem IsNonarchimedean.add_pow_le {α : Type u_1} {R : Type u_3} (a b : α) [LinearOrder R] {f : α → R} (n : ℕ) [Mul R] [CommSemiring α] (f_mul : ∀ (x y : α), f (x * y) ≤ f x * f y) (hna : IsNonarchimedean f) : ∃ m < n + 1, f ((a + b) ^ n) ≤ f (a ^ m) * f (b ^ (n - m))

If f is a submultiplicative, nonarchimedean function on a commutative semiring α, then for n : ℕ and a b : α we can find m : ℕ such that m ≤ n and f ((a + b) ^ n) ≤ (f (a ^ m)) * (f (b ^ (n - m))).