Nonarchimedean functions

A function f : R → ℝ≥0 is nonarchimedean if it satisfies the strong triangle inequality f (r + s) ≤ max (f r) (f s) for all r s : R. This file proves basic properties of nonarchimedean functions.

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

A nonarchimedean function satisfies the triangle inequality.

theorem IsNonarchimedean.nsmul_le {F : Type u_1} {α : Type u_2} [AddGroup α] [FunLike F α ℝ] [AddGroupSeminormClass F α ℝ] {f : F} (hna : IsNonarchimedean ⇑f) {n : ℕ} {a : α} : f (n • a) ≤ f a

If f is a nonarchimedean additive group seminorm on α, then for every n : ℕ and a : α, we have f (n • a) ≤ (f a).

theorem IsNonarchimedean.nmul_le {F : Type u_1} {α : Type u_2} [Ring α] [FunLike F α ℝ] [AddGroupSeminormClass F α ℝ] {f : F} (hna : IsNonarchimedean ⇑f) {n : ℕ} {a : α} : f (↑n * a) ≤ f a

If f is a nonarchimedean additive group seminorm on α, then for every n : ℕ and a : α, we have f (n * a) ≤ (f a).

theorem IsNonarchimedean.add_eq_max_of_ne {F : Type u_1} {α : Type u_2} [AddGroup α] [FunLike F α ℝ] [AddGroupSeminormClass F α ℝ] {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.finset_image_add {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommGroup α] [FunLike F α ℝ] [AddGroupSeminormClass F α ℝ] [Nonempty β] {f : F} (hna : IsNonarchimedean ⇑f) (g : β → α) (t : Finset β) : ∃ (b : β), (t.Nonempty → b ∈ t) ∧ f (t.sum g) ≤ f (g b)

Given a nonarchimedean additive group seminorm f on α, 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.finset_image_add_of_nonempty {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommGroup α] [FunLike F α ℝ] [AddGroupSeminormClass F α ℝ] [Nonempty β] {f : F} (hna : IsNonarchimedean ⇑f) (g : β → α) {t : Finset β} (ht : t.Nonempty) : ∃ b ∈ t, f (t.sum g) ≤ f (g b)

Given a nonarchimedean additive group seminorm f on α, 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 {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommGroup α] [FunLike F α ℝ] [AddGroupSeminormClass F α ℝ] [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 nonarchimedean additive group seminorm f on α, a function g : β → α and a multiset s : Multiset β, we can always find b : β, belonging to s if s is nonempty, such that f (t.sum g) ≤ f (g b) .

theorem IsNonarchimedean.multiset_image_add_of_nonempty {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommGroup α] [FunLike F α ℝ] [AddGroupSeminormClass F α ℝ] [Nonempty β] {f : F} (hna : IsNonarchimedean ⇑f) (g : β → α) {s : Multiset β} (hs : s ≠ 0) : ∃ b ∈ s, f (Multiset.map g s).sum ≤ f (g b)

Given a nonarchimedean additive group seminorm f on α, 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.add_pow_le {F : Type u_1} {α : Type u_2} [CommRing α] [FunLike F α ℝ] [RingSeminormClass F α ℝ] {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))).