feat(Data/Real/IsNonarchimedean): add lemmas (#16767)

Used in #15373.



Co-authored-by: Yakov Pechersky <[email protected]>
Co-authored-by: Yakov Pechersky <[email protected]>
Co-authored-by: David Loeffler <[email protected]>

Mathlib.lean

@@ -627,7 +627,9 @@ import Mathlib.Algebra.Order.GroupWithZero.Unbundled.Lemmas
 import Mathlib.Algebra.Order.GroupWithZero.WithZero
 import Mathlib.Algebra.Order.Hom.Basic
 import Mathlib.Algebra.Order.Hom.Monoid
+import Mathlib.Algebra.Order.Hom.Normed
 import Mathlib.Algebra.Order.Hom.Ring
+import Mathlib.Algebra.Order.Hom.Ultra
 import Mathlib.Algebra.Order.Interval.Basic
 import Mathlib.Algebra.Order.Interval.Finset
 import Mathlib.Algebra.Order.Interval.Multiset
@@ -2577,6 +2579,7 @@ import Mathlib.Data.Real.EReal
 import Mathlib.Data.Real.GoldenRatio
 import Mathlib.Data.Real.Hyperreal
 import Mathlib.Data.Real.Irrational
+import Mathlib.Data.Real.IsNonarchimedean
 import Mathlib.Data.Real.Pi.Bounds
 import Mathlib.Data.Real.Pi.Irrational
 import Mathlib.Data.Real.Pi.Leibniz

Mathlib/Algebra/Order/Hom/Normed.lean

@@ -0,0 +1,75 @@
+/-
+Copyright (c) 2024 Yakov Pechersky. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yakov Pechersky
+-/
+import Mathlib.Algebra.Order.Hom.Basic
+import Mathlib.Analysis.Normed.Group.Basic
+
+/-!
+# Constructing (semi)normed groups from (semi)normed homs
+
+This file defines constructions that upgrade `(Comm)Group` to `(Semi)Normed(Comm)Group`
+using a `Group(Semi)normClass` when the codomain is the reals.
+
+See `Mathlib.Algebra.Order.Hom.Ultra` for further upgrades to nonarchimedean normed groups.
+
+-/
+
+variable {F α : Type*} [FunLike F α ℝ]
+
+/-- Constructs a `SeminormedGroup` structure from a `GroupSeminormClass` on a `Group`. -/
+-- See note [reducible non-instances]
+@[to_additive "Constructs a `SeminormedAddGroup` structure from an `AddGroupSeminormClass` on an
+`AddGroup`."]
+abbrev GroupSeminormClass.toSeminormedGroup [Group α] [GroupSeminormClass F α ℝ]
+    (f : F) : SeminormedGroup α where
+  norm := f
+  dist x y := f (x / y)
+  dist_eq _ _ := rfl
+  dist_self _ := by simp
+  dist_comm x y := by simp only [← map_inv_eq_map f (x / y), inv_div]
+  dist_triangle x y z := by simpa using map_mul_le_add f (x / y) (y / z)
+
+@[to_additive]
+lemma GroupSeminormClass.toSeminormedGroup_norm_eq [Group α] [GroupSeminormClass F α ℝ]
+    (f : F) (x : α) : @norm _ (GroupSeminormClass.toSeminormedGroup f).toNorm x = f x := rfl
+
+/-- Constructs a `SeminormedCommGroup` structure from a `GroupSeminormClass` on a `CommGroup`. -/
+-- See note [reducible non-instances]
+@[to_additive "Constructs a `SeminormedAddCommGroup` structure from an `AddGroupSeminormClass` on an
+`AddCommGroup`."]
+abbrev GroupSeminormClass.toSeminormedCommGroup [CommGroup α] [GroupSeminormClass F α ℝ]
+    (f : F) : SeminormedCommGroup α where
+  __ := GroupSeminormClass.toSeminormedGroup f
+  __ : CommGroup α := inferInstance
+
+@[to_additive]
+lemma GroupSeminormClass.toSeminormedCommGroup_norm_eq [CommGroup α] [GroupSeminormClass F α ℝ]
+    (f : F) (x : α) : @norm _ (GroupSeminormClass.toSeminormedCommGroup f).toNorm x = f x := rfl
+
+/-- Constructs a `NormedGroup` structure from a `GroupNormClass` on a `Group`. -/
+-- See note [reducible non-instances]
+@[to_additive "Constructs a `NormedAddGroup` structure from an `AddGroupNormClass` on an
+`AddGroup`."]
+abbrev GroupNormClass.toNormedGroup [Group α] [GroupNormClass F α ℝ]
+    (f : F) : NormedGroup α where
+  __ := GroupSeminormClass.toSeminormedGroup f
+  eq_of_dist_eq_zero h := div_eq_one.mp (eq_one_of_map_eq_zero f h)
+
+@[to_additive]
+lemma GroupNormClass.toNormedGroup_norm_eq [Group α] [GroupNormClass F α ℝ]
+    (f : F) (x : α) : @norm _ (GroupNormClass.toNormedGroup f).toNorm x = f x := rfl
+
+/-- Constructs a `NormedCommGroup` structure from a `GroupNormClass` on a `CommGroup`. -/
+-- See note [reducible non-instances]
+@[to_additive "Constructs a `NormedAddCommGroup` structure from an `AddGroupNormClass` on an
+`AddCommGroup`."]
+abbrev GroupNormClass.toNormedCommGroup [CommGroup α] [GroupNormClass F α ℝ]
+    (f : F) : NormedCommGroup α where
+  __ := GroupNormClass.toNormedGroup f
+  __ : CommGroup α := inferInstance
+
+@[to_additive]
+lemma GroupNormClass.toNormedCommGroup_norm_eq [CommGroup α] [GroupNormClass F α ℝ]
+    (f : F) (x : α) : @norm _ (GroupNormClass.toNormedCommGroup f).toNorm x = f x := rfl

Mathlib/Algebra/Order/Hom/Ultra.lean

@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2024 Yakov Pechersky. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yakov Pechersky
+-/
+import Mathlib.Algebra.Order.Hom.Normed
+import Mathlib.Topology.MetricSpace.Ultra.Basic
+
+/-!
+# Constructing nonarchimedean (ultrametric) normed groups from nonarchimedean normed homs
+
+This file defines constructions that upgrade `Add(Comm)Group` to `(Semi)NormedAdd(Comm)Group`
+using an `AddGroup(Semi)normClass` when the codomain is the reals and the hom is nonarchimedean.
+
+## Implementation details
+
+The lemmas need to assume `[Dist α]` to be able to be stated, so they take an extra argument
+that shows that this distance instance is propositionally equal to the one that comes from the
+hom-based `AddGroupSeminormClass.toSeminormedAddGroup f` construction. To help at use site,
+the argument is an autoparam that resolves by definitional equality when using these constructions.
+-/
+
+variable {F α : Type*} [FunLike F α ℝ]
+
+/-- Proves that when a `SeminormedAddGroup` structure is constructed from an
+`AddGroupSeminormClass` that satifies `IsNonarchimedean`, the group has an `IsUltrametricDist`. -/
+lemma AddGroupSeminormClass.isUltrametricDist [AddGroup α] [AddGroupSeminormClass F α ℝ]
+    [inst : Dist α] {f : F} (hna : IsNonarchimedean f)
+    (hd : inst = (AddGroupSeminormClass.toSeminormedAddGroup f).toDist := by rfl) :
+    IsUltrametricDist α :=
+  ⟨fun x y z ↦ by simpa only [hd, dist_eq_norm, AddGroupSeminormClass.toSeminormedAddGroup_norm_eq,
+      ← sub_add_sub_cancel x y z] using hna _ _⟩

Mathlib/Analysis/Normed/Group/Ultra.lean

@@ -237,6 +237,54 @@ lemma norm_prod_le_of_forall_le_of_nonneg {s : Finset ι} {f : ι → M} {C : 
   lift C to NNReal using h_nonneg
   exact nnnorm_prod_le_of_forall_le hC
 
+/--
+Given a function `f : ι → M` and a nonempty finite set `t ⊆ ι`, we can always find `i ∈ t` such that
+`‖∏ j in t, f j‖ ≤ ‖f i‖`.
+-/
+@[to_additive "Given a function `f : ι → M` and a nonempty finite set `t ⊆ ι`, we can always find
+`i ∈ t` such that `‖∑ j in t, f j‖ ≤ ‖f i‖`."]
+theorem exists_norm_finset_prod_le_of_nonempty {t : Finset ι} (ht : t.Nonempty) (f : ι → M) :
+    ∃ i ∈ t, ‖∏ j in t, f j‖ ≤ ‖f i‖ :=
+  match t.exists_mem_eq_sup' ht (‖f ·‖) with
+  |⟨j, hj, hj'⟩ => ⟨j, hj, (ht.norm_prod_le_sup'_norm f).trans (le_of_eq hj')⟩
+
+/--
+Given a function `f : ι → M` and a finite set `t ⊆ ι`, we can always find `i : ι`, belonging to `t`
+if `t` is nonempty, such that `‖∏ j in t, f j‖ ≤ ‖f i‖`.
+-/
+@[to_additive "Given a function `f : ι → M` and a finite set `t ⊆ ι`, we can always find `i : ι`,
+belonging to `t` if `t` is nonempty, such that `‖∑ j in t, f j‖ ≤ ‖f i‖`."]
+theorem exists_norm_finset_prod_le (t : Finset ι) [Nonempty ι] (f : ι → M) :
+    ∃ i : ι, (t.Nonempty → i ∈ t) ∧ ‖∏ j in t, f j‖ ≤ ‖f i‖ := by
+  rcases t.eq_empty_or_nonempty with rfl | ht
+  · simp
+  exact (fun ⟨i, h, h'⟩ => ⟨i, fun _ ↦ h, h'⟩) <| exists_norm_finset_prod_le_of_nonempty ht f
+
+/--
+Given a function `f : ι → M` and a multiset `t : Multiset ι`, we can always find `i : ι`, belonging
+to `t` if `t` is nonempty, such that `‖(s.map f).prod‖ ≤ ‖f i‖`.
+-/
+@[to_additive "Given a function `f : ι → M` and a multiset `t : Multiset ι`, we can always find
+`i : ι`, belonging to `t` if `t` is nonempty, such that `‖(s.map f).sum‖ ≤ ‖f i‖`."]
+theorem exists_norm_multiset_prod_le (s : Multiset ι) [Nonempty ι] {f : ι → M} :
+    ∃ i : ι, (s ≠ 0 → i ∈ s) ∧ ‖(s.map f).prod‖ ≤ ‖f i‖ := by
+  inhabit ι
+  induction s using Multiset.induction_on with
+  | empty => simp
+  | @cons a t hM =>
+      obtain ⟨M, hMs, hM⟩ := hM
+      by_cases hMa : ‖f M‖ ≤ ‖f a‖
+      · refine ⟨a, by simp, ?_⟩
+        · rw [Multiset.map_cons, Multiset.prod_cons]
+          exact le_trans (norm_mul_le_max _ _) (max_le (le_refl _) (le_trans hM hMa))
+      · rw [not_le] at hMa
+        rcases eq_or_ne t 0 with rfl|ht
+        · exact ⟨a, by simp, by simp⟩
+        · refine ⟨M, ?_, ?_⟩
+          · simp [hMs ht]
+          rw [Multiset.map_cons, Multiset.prod_cons]
+          exact le_trans (norm_mul_le_max _ _) (max_le hMa.le hM)
+
 @[to_additive]
 lemma norm_tprod_le (f : ι → M) : ‖∏' i, f i‖ ≤ ⨆ i, ‖f i‖ := by
   rcases isEmpty_or_nonempty ι with hι | hι

Mathlib/Data/Real/IsNonarchimedean.lean

@@ -0,0 +1,114 @@
+/-
+Copyright (c) 2024 María Inés de Frutos-Fernández. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: María Inés de Frutos-Fernández
+-/
+import Mathlib.Algebra.Order.Hom.Ultra
+import Mathlib.Analysis.Normed.Group.Ultra
+
+/-!
+# 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.
+-/
+
+namespace IsNonarchimedean
+
+open IsUltrametricDist
+
+/-- A nonarchimedean function satisfies the triangle inequality. -/
+theorem add_le {α : Type*} [Add α] {f : α → ℝ} (hf : ∀ x : α, 0 ≤ f x)
+    (hna : IsNonarchimedean f) {a b : α} : f (a + b) ≤ f a + f b := by
+  apply le_trans (hna _ _)
+  rw [max_le_iff, le_add_iff_nonneg_right, le_add_iff_nonneg_left]
+  exact ⟨hf _, hf _⟩
+
+/-- If `f` is a nonarchimedean additive group seminorm on `α`, then for every `n : ℕ` and `a : α`,
+  we have `f (n • a) ≤ (f a)`. -/
+theorem nsmul_le {F α : Type*} [AddGroup α] [FunLike F α ℝ]
+    [AddGroupSeminormClass F α ℝ] {f : F} (hna : IsNonarchimedean f) {n : ℕ} {a : α} :
+    f (n • a) ≤ f a := by
+  let _ := AddGroupSeminormClass.toSeminormedAddGroup f
+  have := AddGroupSeminormClass.isUltrametricDist hna
+  simp only [← AddGroupSeminormClass.toSeminormedAddGroup_norm_eq]
+  exact norm_nsmul_le _ _
+
+/-- If `f` is a nonarchimedean additive group seminorm on `α`, then for every `n : ℕ` and `a : α`,
+  we have `f (n * a) ≤ (f a)`. -/
+theorem nmul_le {F α : Type*} [Ring α] [FunLike F α ℝ] [AddGroupSeminormClass F α ℝ]
+    {f : F} (hna : IsNonarchimedean f) {n : ℕ} {a : α} : f (n * a) ≤ f a := by
+  rw [← nsmul_eq_mul]
+  exact nsmul_le hna
+
+/-- 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 add_eq_max_of_ne {F α : Type*} [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) := by
+  let _ := AddGroupSeminormClass.toSeminormedAddGroup f
+  have := AddGroupSeminormClass.isUltrametricDist hna
+  simp only [← AddGroupSeminormClass.toSeminormedAddGroup_norm_eq] at hne ⊢
+  exact norm_add_eq_max_of_norm_ne_norm hne
+
+/-- 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 finset_image_add {F α β : Type*} [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) := by
+  let _ := AddGroupSeminormClass.toSeminormedAddCommGroup f
+  have := AddGroupSeminormClass.isUltrametricDist hna
+  simp only [← AddGroupSeminormClass.toSeminormedAddCommGroup_norm_eq]
+  apply exists_norm_finset_sum_le
+
+/-- 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 finset_image_add_of_nonempty {F α β : Type*} [AddCommGroup α] [FunLike F α ℝ]
+    [AddGroupSeminormClass F α ℝ] [Nonempty β] {f : F} (hna : IsNonarchimedean f)
+    (g : β → α) {t : Finset β} (ht : t.Nonempty) :
+    ∃ b : β, (b ∈ t) ∧ f (t.sum g) ≤ f (g b) := by
+  obtain ⟨b, hbt, hbf⟩ := finset_image_add hna g t
+  exact ⟨b, hbt ht, hbf⟩
+
+/-- 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 multiset_image_add {F α β : Type*} [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) := by
+  let _ := AddGroupSeminormClass.toSeminormedAddCommGroup f
+  have := AddGroupSeminormClass.isUltrametricDist hna
+  simp only [← AddGroupSeminormClass.toSeminormedAddCommGroup_norm_eq]
+  apply exists_norm_multiset_sum_le
+
+/-- 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 multiset_image_add_of_nonempty {F α β : Type*} [AddCommGroup α] [FunLike F α ℝ]
+    [AddGroupSeminormClass F α ℝ] [Nonempty β] {f : F} (hna : IsNonarchimedean f)
+    (g : β → α) {s : Multiset β} (hs : s ≠ 0) :
+    ∃ b : β, (b ∈ s) ∧ f (Multiset.map g s).sum ≤ f (g b) := by
+  obtain ⟨b, hbs, hbf⟩ := multiset_image_add hna g s
+  exact ⟨b, hbs hs, hbf⟩
+
+/-- 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)))`. -/
+theorem add_pow_le {F α : Type*} [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)) := by
+  obtain ⟨m, hm_lt, hM⟩ := finset_image_add hna
+    (fun m => a ^ m * b ^ (n - m) * ↑(n.choose m)) (Finset.range (n + 1))
+  simp only [Finset.nonempty_range_iff, ne_eq, Nat.succ_ne_zero, not_false_iff, Finset.mem_range,
+    if_true, forall_true_left] at hm_lt
+  refine ⟨m, hm_lt, ?_⟩
+  simp only [← add_pow] at hM
+  rw [mul_comm] at hM
+  exact le_trans hM (le_trans (nmul_le hna) (map_mul_le_mul _ _ _))
+
+end IsNonarchimedean