doc-next-gen

Mathlib.Analysis.Normed.Group.Seminorm

Module docstring

{"# Group seminorms

This file defines norms and seminorms in a group. A group seminorm is a function to the reals which is positive-semidefinite and subadditive. A norm further only maps zero to zero.

Main declarations

  • AddGroupSeminorm: A function f from an additive group G to the reals that preserves zero, takes nonnegative values, is subadditive and such that f (-x) = f x for all x.
  • NonarchAddGroupSeminorm: A function f from an additive group G to the reals that preserves zero, takes nonnegative values, is nonarchimedean and such that f (-x) = f x for all x.
  • GroupSeminorm: A function f from a group G to the reals that sends one to zero, takes nonnegative values, is submultiplicative and such that f x⁻¹ = f x for all x.
  • AddGroupNorm: A seminorm f such that f x = 0 → x = 0 for all x.
  • NonarchAddGroupNorm: A nonarchimedean seminorm f such that f x = 0 → x = 0 for all x.
  • GroupNorm: A seminorm f such that f x = 0 → x = 1 for all x.

Notes

The corresponding hom classes are defined in Analysis.Order.Hom.Basic to be used by absolute values.

We do not define NonarchAddGroupSeminorm as an extension of AddGroupSeminorm to avoid having a superfluous add_le' field in the resulting structure. The same applies to NonarchAddGroupNorm.

References

  • [H. H. Schaefer, Topological Vector Spaces][schaefer1966]

Tags

norm, seminorm ","NOTE: We do not define NonarchAddGroupSeminorm as an extension of AddGroupSeminorm to avoid having a superfluous add_le' field in the resulting structure. The same applies to NonarchAddGroupNorm below. ","### Seminorms ","### Norms "}

AddGroupSeminorm structure
(G : Type*) [AddGroup G]
Full source 
/-- A seminorm on an additive group `G` is a function `f : G → ℝ` that preserves zero, is
subadditive and such that `f (-x) = f x` for all `x`. -/
structure AddGroupSeminorm (G : Type*) [AddGroup G] where
  -- Porting note: can't extend `ZeroHom G ℝ` because otherwise `to_additive` won't work since
  -- we aren't using old structures
  /-- The bare function of an `AddGroupSeminorm`. -/
  protected toFun : G → ℝ
  /-- The image of zero is zero. -/
  protected map_zero' : toFun 0 = 0
  /-- The seminorm is subadditive. -/
  protected add_le' : ∀ r s, toFun (r + s) ≤ toFun r + toFun s
  /-- The seminorm is invariant under negation. -/
  protected neg' : ∀ r, toFun (-r) = toFun r
Additive group seminorm
Informal description
An additive group seminorm on an additive group $G$ is a function $f \colon G \to \mathbb{R}$ that satisfies the following properties: 1. **Preservation of zero**: $f(0) = 0$. 2. **Nonnegativity**: $f(x) \geq 0$ for all $x \in G$. 3. **Subadditivity**: $f(x + y) \leq f(x) + f(y)$ for all $x, y \in G$. 4. **Symmetry**: $f(-x) = f(x)$ for all $x \in G$.
GroupSeminorm structure
(G : Type*) [Group G]
Full source 
/-- A seminorm on a group `G` is a function `f : G → ℝ` that sends one to zero, is submultiplicative
and such that `f x⁻¹ = f x` for all `x`. -/
@[to_additive]
structure GroupSeminorm (G : Type*) [Group G] where
  /-- The bare function of a `GroupSeminorm`. -/
  protected toFun : G → ℝ
  /-- The image of one is zero. -/
  protected map_one' : toFun 1 = 0
  /-- The seminorm applied to a product is dominated by the sum of the seminorm applied to the
  factors. -/
  protected mul_le' : ∀ x y, toFun (x * y) ≤ toFun x + toFun y
  /-- The seminorm is invariant under inversion. -/
  protected inv' : ∀ x, toFun x⁻¹ = toFun x
Group seminorm
Informal description
A group seminorm on a group $G$ is a function $f \colon G \to \mathbb{R}$ that satisfies the following properties: 1. $f(1) = 0$ (sends the identity to zero) 2. $f(x) \geq 0$ for all $x \in G$ (nonnegative) 3. $f(xy) \leq f(x) + f(y)$ for all $x, y \in G$ (subadditive) 4. $f(x^{-1}) = f(x)$ for all $x \in G$ (inverse-invariant)
NonarchAddGroupSeminorm structure
(G : Type*) [AddGroup G] extends ZeroHom G ℝ
Full source 
/-- A nonarchimedean seminorm on an additive group `G` is a function `f : G → ℝ` that preserves
zero, is nonarchimedean and such that `f (-x) = f x` for all `x`. -/
structure NonarchAddGroupSeminorm (G : Type*) [AddGroup G] extends ZeroHom G ℝ where
  /-- The seminorm applied to a sum is dominated by the maximum of the function applied to the
  addends. -/
  protected add_le_max' : ∀ r s, toFun (r + s) ≤ max (toFun r) (toFun s)
  /-- The seminorm is invariant under negation. -/
  protected neg' : ∀ r, toFun (-r) = toFun r
Nonarchimedean additive group seminorm
Informal description
A nonarchimedean seminorm on an additive group $G$ is a function $f: G \to \mathbb{R}$ that satisfies the following properties: 1. **Preservation of zero**: $f(0) = 0$. 2. **Nonnegativity**: $f(x) \geq 0$ for all $x \in G$. 3. **Nonarchimedean property**: $f(x + y) \leq \max(f(x), f(y))$ for all $x, y \in G$. 4. **Symmetry**: $f(-x) = f(x)$ for all $x \in G$.
AddGroupNorm structure
(G : Type*) [AddGroup G] extends AddGroupSeminorm G
Full source 
/-- A norm on an additive group `G` is a function `f : G → ℝ` that preserves zero, is subadditive
and such that `f (-x) = f x` and `f x = 0 → x = 0` for all `x`. -/
structure AddGroupNorm (G : Type*) [AddGroup G] extends AddGroupSeminorm G where
  /-- If the image under the seminorm is zero, then the argument is zero. -/
  protected eq_zero_of_map_eq_zero' : ∀ x, toFun x = 0 → x = 0
Additive Group Norm
Informal description
An additive group norm on an additive group $G$ is a function $f \colon G \to \mathbb{R}$ that satisfies the following properties: 1. **Preservation of zero**: $f(0) = 0$. 2. **Nonnegativity**: $f(x) \geq 0$ for all $x \in G$. 3. **Subadditivity**: $f(x + y) \leq f(x) + f(y)$ for all $x, y \in G$. 4. **Symmetry**: $f(-x) = f(x)$ for all $x \in G$. 5. **Definiteness**: $f(x) = 0$ implies $x = 0$ for all $x \in G$.
GroupNorm structure
(G : Type*) [Group G] extends GroupSeminorm G
Full source 
/-- A seminorm on a group `G` is a function `f : G → ℝ` that sends one to zero, is submultiplicative
and such that `f x⁻¹ = f x` and `f x = 0 → x = 1` for all `x`. -/
@[to_additive]
structure GroupNorm (G : Type*) [Group G] extends GroupSeminorm G where
  /-- If the image under the norm is zero, then the argument is one. -/
  protected eq_one_of_map_eq_zero' : ∀ x, toFun x = 0 → x = 1
Group norm
Informal description
A group norm on a group $G$ is a function $f \colon G \to \mathbb{R}$ that satisfies the following properties: 1. $f(1) = 0$ (preserves the identity), 2. $f(x) \geq 0$ for all $x \in G$ (nonnegativity), 3. $f(xy) \leq f(x) + f(y)$ for all $x, y \in G$ (subadditivity), 4. $f(x^{-1}) = f(x)$ for all $x \in G$ (symmetry under inversion), and 5. $f(x) = 0$ implies $x = 1$ (definiteness).
NonarchAddGroupNorm structure
(G : Type*) [AddGroup G] extends NonarchAddGroupSeminorm G
Full source 
/-- A nonarchimedean norm on an additive group `G` is a function `f : G → ℝ` that preserves zero, is
nonarchimedean and such that `f (-x) = f x` and `f x = 0 → x = 0` for all `x`. -/
structure NonarchAddGroupNorm (G : Type*) [AddGroup G] extends NonarchAddGroupSeminorm G where
  /-- If the image under the norm is zero, then the argument is zero. -/
  protected eq_zero_of_map_eq_zero' : ∀ x, toFun x = 0 → x = 0
Nonarchimedean additive group norm
Informal description
A nonarchimedean norm on an additive group $G$ is a function $f: G \to \mathbb{R}$ that satisfies: 1. $f(0) = 0$ (preserves zero) 2. $f(x) \geq 0$ for all $x \in G$ (nonnegative) 3. $f(-x) = f(x)$ for all $x \in G$ (even) 4. $f(x + y) \leq \max(f(x), f(y))$ for all $x, y \in G$ (nonarchimedean/subadditive) 5. $f(x) = 0$ implies $x = 0$ (definite)
NonarchAddGroupSeminormClass structure
(F : Type*) (α : outParam Type*) [AddGroup α] [FunLike F α ℝ] : Prop extends NonarchimedeanHomClass F α ℝ
Full source 
/-- `NonarchAddGroupSeminormClass F α` states that `F` is a type of nonarchimedean seminorms on
the additive group `α`.

You should extend this class when you extend `NonarchAddGroupSeminorm`. -/
class NonarchAddGroupSeminormClass (F : Type*) (α : outParam Type*)
    [AddGroup α] [FunLike F α ℝ] : Prop
    extends NonarchimedeanHomClass F α ℝ where
  /-- The image of zero is zero. -/
  protected map_zero (f : F) : f 0 = 0
  /-- The seminorm is invariant under negation. -/
  protected map_neg_eq_map' (f : F) (a : α) : f (-a) = f a
Nonarchimedean additive group seminorm class
Informal description
The class `NonarchAddGroupSeminormClass F α` states that `F` is a type of nonarchimedean seminorms on the additive group `α`. A nonarchimedean seminorm is a function $f \colon \alpha \to \mathbb{R}$ that satisfies: 1. $f(0) = 0$ (preserves zero), 2. $f(x) \geq 0$ for all $x \in \alpha$ (nonnegativity), 3. $f(-x) = f(x)$ for all $x \in \alpha$ (evenness), and 4. $f(x + y) \leq \max(f(x), f(y))$ for all $x, y \in \alpha$ (nonarchimedean subadditivity). This class extends `NonarchimedeanHomClass` and should be extended when defining new types of nonarchimedean seminorms.
NonarchAddGroupNormClass structure
(F : Type*) (α : outParam Type*) [AddGroup α] [FunLike F α ℝ] : Prop extends NonarchAddGroupSeminormClass F α
Full source 
/-- `NonarchAddGroupNormClass F α` states that `F` is a type of nonarchimedean norms on the
additive group `α`.

You should extend this class when you extend `NonarchAddGroupNorm`. -/
class NonarchAddGroupNormClass (F : Type*) (α : outParam Type*) [AddGroup α] [FunLike F α ℝ] : Prop
    extends NonarchAddGroupSeminormClass F α where
  /-- If the image under the norm is zero, then the argument is zero. -/
  protected eq_zero_of_map_eq_zero (f : F) {a : α} : f a = 0 → a = 0
Nonarchimedean additive group norm class
Informal description
The class `NonarchAddGroupNormClass F α` states that `F` is a type of nonarchimedean norms on the additive group `α`. A nonarchimedean norm is a function $f: \alpha \to \mathbb{R}$ that satisfies: 1. $f(0) = 0$ (preserves zero) 2. $f(x) \geq 0$ for all $x \in \alpha$ (nonnegative) 3. $f(-x) = f(x)$ for all $x \in \alpha$ (even) 4. $f(x + y) \leq \max(f(x), f(y))$ for all $x, y \in \alpha$ (nonarchimedean/subadditive) 5. $f(x) = 0$ implies $x = 0$ (definite) This class extends `NonarchAddGroupSeminormClass` and should be extended when defining new types of nonarchimedean norms.
map_sub_le_max theorem
: f (x - y) ≤ max (f x) (f y)
Full source 
theorem map_sub_le_max : f (x - y) ≤ max (f x) (f y) := by
  rw [sub_eq_add_neg, ← NonarchAddGroupSeminormClass.map_neg_eq_map' f y]
  exact map_add_le_max _ _ _
Nonarchimedean Seminorm Subadditivity: $f(x - y) \leq \max(f(x), f(y))$
Informal description
For a nonarchimedean additive group seminorm $f$ on an additive group $G$ and any elements $x, y \in G$, the seminorm satisfies the inequality $f(x - y) \leq \max(f(x), f(y))$.
NonarchAddGroupSeminormClass.toAddGroupSeminormClass instance
[FunLike F E ℝ] [AddGroup E] [NonarchAddGroupSeminormClass F E] : AddGroupSeminormClass F E ℝ
Full source 
instance (priority := 100) NonarchAddGroupSeminormClass.toAddGroupSeminormClass
    [FunLike F E ℝ] [AddGroup E] [NonarchAddGroupSeminormClass F E] : AddGroupSeminormClass F E ℝ :=
  { ‹NonarchAddGroupSeminormClass F E› with
    map_add_le_add := fun f _ _ =>
      haveI h_nonneg : ∀ a, 0 ≤ f a := by
        intro a
        rw [← NonarchAddGroupSeminormClass.map_zero f, ← sub_self a]
        exact le_trans (map_sub_le_max _ _ _) (by rw [max_self (f a)])
      le_trans (map_add_le_max _ _ _)
        (max_le (le_add_of_nonneg_right (h_nonneg _)) (le_add_of_nonneg_left (h_nonneg _)))
    map_neg_eq_map := NonarchAddGroupSeminormClass.map_neg_eq_map' }
Nonarchimedean Additive Group Seminorms are Additive Group Seminorms
Informal description
For any type `F` of nonarchimedean additive group seminorms on an additive group `E`, where `F` is equipped with a function-like structure to `ℝ`, the type `F` also forms an additive group seminorm class. This means every nonarchimedean additive group seminorm satisfies the properties of an additive group seminorm: it preserves zero, is nonnegative, even, and subadditive.
NonarchAddGroupNormClass.toAddGroupNormClass instance
[FunLike F E ℝ] [AddGroup E] [NonarchAddGroupNormClass F E] : AddGroupNormClass F E ℝ
Full source 
instance (priority := 100) NonarchAddGroupNormClass.toAddGroupNormClass
    [FunLike F E ℝ] [AddGroup E] [NonarchAddGroupNormClass F E] : AddGroupNormClass F E ℝ :=
  { ‹NonarchAddGroupNormClass F E› with
    map_add_le_add := map_add_le_add
    map_neg_eq_map := NonarchAddGroupSeminormClass.map_neg_eq_map' }
Nonarchimedean Additive Group Norms are Additive Group Norms
Informal description
For any type `F` of nonarchimedean additive group norms on an additive group `E`, where `F` is equipped with a function-like structure to `ℝ`, the type `F` also forms an additive group norm class. This means every nonarchimedean additive group norm satisfies the properties of an additive group norm: it preserves zero, is nonnegative, even, subadditive, and definite (i.e., $f(x) = 0$ implies $x = 0$).
GroupSeminorm.funLike instance
: FunLike (GroupSeminorm E) E ℝ
Full source 
@[to_additive]
instance funLike : FunLike (GroupSeminorm E) E ℝ where
  coe f := f.toFun
  coe_injective' f g h := by cases f; cases g; congr
Group Seminorms as Function-Like Types
Informal description
For any group $E$, the type of group seminorms on $E$ can be treated as a function-like type, where each group seminorm $p$ can be coerced to a function from $E$ to $\mathbb{R}$.
GroupSeminorm.groupSeminormClass instance
: GroupSeminormClass (GroupSeminorm E) E ℝ
Full source 
@[to_additive]
instance groupSeminormClass : GroupSeminormClass (GroupSeminorm E) E ℝ where
  map_one_eq_zero f := f.map_one'
  map_mul_le_add f := f.mul_le'
  map_inv_eq_map f := f.inv'
Group Seminorms Satisfy the Group Seminorm Class Properties
Informal description
For any group $E$, the type `GroupSeminorm E` of group seminorms on $E$ forms a `GroupSeminormClass`, meaning that every group seminorm $p \colon E \to \mathbb{R}$ satisfies the following properties: 1. (Nonnegativity) $0 \leq p(x)$ for all $x \in E$, 2. (Subadditivity) $p(xy) \leq p(x) + p(y)$ for all $x, y \in E$, 3. (Inversion invariance) $p(x^{-1}) = p(x)$ for all $x \in E$, 4. (Preservation of identity) $p(1) = 0$.
GroupSeminorm.toFun_eq_coe theorem
: p.toFun = p
Full source 
@[to_additive (attr := simp)]
theorem toFun_eq_coe : p.toFun = p :=
  rfl
Equality of Group Seminorm Function and Its Coercion
Informal description
For any group seminorm $p$ on a group $G$, the underlying function $p.\text{toFun}$ is equal to $p$ itself when viewed as a function from $G$ to $\mathbb{R}$.
GroupSeminorm.ext theorem
: (∀ x, p x = q x) → p = q
Full source 
@[to_additive (attr := ext)]
theorem ext : (∀ x, p x = q x) → p = q :=
  DFunLike.ext p q
Extensionality of Group Seminorms
Informal description
For two group seminorms $p$ and $q$ on a group $G$, if $p(x) = q(x)$ for all $x \in G$, then $p = q$.
GroupSeminorm.instPartialOrder instance
: PartialOrder (GroupSeminorm E)
Full source 
@[to_additive]
instance : PartialOrder (GroupSeminorm E) :=
  PartialOrder.lift _ DFunLike.coe_injective
Partial Order on Group Seminorms
Informal description
The set of group seminorms on a group $E$ forms a partial order, where for two seminorms $p$ and $q$, we have $p \leq q$ if and only if $p(x) \leq q(x)$ for all $x \in E$.
GroupSeminorm.le_def theorem
: p ≤ q ↔ (p : E → ℝ) ≤ q
Full source 
@[to_additive]
theorem le_def : p ≤ q ↔ (p : E → ℝ) ≤ q :=
  Iff.rfl
Order Relation on Group Seminorms via Pointwise Comparison
Informal description
For two group seminorms $p$ and $q$ on a group $E$, the inequality $p \leq q$ holds if and only if $p(x) \leq q(x)$ for all $x \in E$.
GroupSeminorm.lt_def theorem
: p < q ↔ (p : E → ℝ) < q
Full source 
@[to_additive]
theorem lt_def : p < q ↔ (p : E → ℝ) < q :=
  Iff.rfl
Strict Order Relation on Group Seminorms via Pointwise Comparison
Informal description
For two group seminorms $p$ and $q$ on a group $E$, the strict inequality $p < q$ holds if and only if $p(x) < q(x)$ for all $x \in E$.
GroupSeminorm.coe_le_coe theorem
: (p : E → ℝ) ≤ q ↔ p ≤ q
Full source 
@[to_additive (attr := simp, norm_cast)]
theorem coe_le_coe : (p : E → ℝ) ≤ q ↔ p ≤ q :=
  Iff.rfl
Pointwise Ordering of Group Seminorms
Informal description
For two group seminorms $p$ and $q$ on a group $E$, the pointwise inequality $p(x) \leq q(x)$ holds for all $x \in E$ if and only if $p \leq q$ in the partial order of group seminorms.
GroupSeminorm.coe_lt_coe theorem
: (p : E → ℝ) < q ↔ p < q
Full source 
@[to_additive (attr := simp, norm_cast)]
theorem coe_lt_coe : (p : E → ℝ) < q ↔ p < q :=
  Iff.rfl
Pointwise Strict Inequality of Group Seminorms is Equivalent to Partial Order
Informal description
For two group seminorms $p$ and $q$ on a group $E$, the pointwise inequality $p(x) < q(x)$ holds for all $x \in E$ if and only if $p < q$ in the partial order of group seminorms.
GroupSeminorm.coe_zero theorem
: ⇑(0 : GroupSeminorm E) = 0
Full source 
@[to_additive (attr := simp, norm_cast)]
theorem coe_zero : ⇑(0 : GroupSeminorm E) = 0 :=
  rfl
Zero Group Seminorm is the Zero Function
Informal description
The zero group seminorm, when viewed as a function, is equal to the zero function. That is, for any group $E$, the function associated with the zero group seminorm $0 \colon \text{GroupSeminorm}(E)$ satisfies $0(x) = 0$ for all $x \in E$.
GroupSeminorm.zero_apply theorem
(x : E) : (0 : GroupSeminorm E) x = 0
Full source 
@[to_additive (attr := simp)]
theorem zero_apply (x : E) : (0 : GroupSeminorm E) x = 0 :=
  rfl
Zero Group Seminorm Evaluates to Zero
Informal description
For any group $E$ and any element $x \in E$, the zero group seminorm evaluated at $x$ equals zero, i.e., $0(x) = 0$.
GroupSeminorm.instInhabited instance
: Inhabited (GroupSeminorm E)
Full source 
@[to_additive]
instance : Inhabited (GroupSeminorm E) :=
  ⟨0⟩
Inhabitedness of Group Seminorms
Informal description
For any group $E$, the type of group seminorms on $E$ is inhabited. In particular, the zero function is a group seminorm.
GroupSeminorm.instAdd instance
: Add (GroupSeminorm E)
Full source 
@[to_additive]
instance : Add (GroupSeminorm E) :=
  ⟨fun p q =>
    { toFun := fun x => p x + q x
      map_one' := by simp_rw [map_one_eq_zero p, map_one_eq_zero q, zero_add]
      mul_le' := fun _ _ =>
        (add_le_add (map_mul_le_add p _ _) <| map_mul_le_add q _ _).trans_eq <|
          add_add_add_comm _ _ _ _
      inv' := fun x => by simp_rw [map_inv_eq_map p, map_inv_eq_map q] }⟩
Additive Structure on Group Seminorms
Informal description
For any group $E$, the set of group seminorms on $E$ forms an additive structure, where the addition of two group seminorms $p$ and $q$ is defined pointwise as $(p + q)(x) = p(x) + q(x)$ for all $x \in E$.
GroupSeminorm.coe_add theorem
: ⇑(p + q) = p + q
Full source 
@[to_additive (attr := simp)]
theorem coe_add : ⇑(p + q) = p + q :=
  rfl
Pointwise Sum Formula for Group Seminorms
Informal description
For any group seminorms $p$ and $q$ on a group $G$, the underlying function of their sum $p + q$ is equal to the pointwise sum of the functions $p$ and $q$, i.e., $(p + q)(x) = p(x) + q(x)$ for all $x \in G$.
GroupSeminorm.add_apply theorem
(x : E) : (p + q) x = p x + q x
Full source 
@[to_additive (attr := simp)]
theorem add_apply (x : E) : (p + q) x = p x + q x :=
  rfl
Pointwise Sum Formula for Group Seminorms
Informal description
For any group seminorms $p$ and $q$ on a group $E$ and any element $x \in E$, the value of the sum seminorm $p + q$ at $x$ equals the sum of the values of $p$ and $q$ at $x$, i.e., $(p + q)(x) = p(x) + q(x)$.
GroupSeminorm.instMax instance
: Max (GroupSeminorm E)
Full source 
@[to_additive]
instance : Max (GroupSeminorm E) :=
  ⟨fun p q =>
    { toFun := p ⊔ q
      map_one' := by
        rw [Pi.sup_apply, ← map_one_eq_zero p, sup_eq_left, map_one_eq_zero p, map_one_eq_zero q]
      mul_le' := fun x y =>
        sup_le ((map_mul_le_add p x y).trans <| add_le_add le_sup_left le_sup_left)
          ((map_mul_le_add q x y).trans <| add_le_add le_sup_right le_sup_right)
      inv' := fun x => by rw [Pi.sup_apply, Pi.sup_apply, map_inv_eq_map p, map_inv_eq_map q] }⟩
Pointwise Maximum Operation on Group Seminorms
Informal description
For any group $E$, the set of group seminorms on $E$ has a maximum operation defined pointwise. That is, for any two group seminorms $p$ and $q$ on $E$, their supremum $p \sqcup q$ is the group seminorm given by $(p \sqcup q)(x) = \max(p(x), q(x))$ for all $x \in E$.
GroupSeminorm.coe_sup theorem
: ⇑(p ⊔ q) = ⇑p ⊔ ⇑q
Full source 
@[to_additive (attr := simp, norm_cast)]
theorem coe_sup : ⇑(p ⊔ q) = ⇑p ⊔ ⇑q :=
  rfl
Supremum of Group Seminorms is Pointwise Maximum
Informal description
For any two group seminorms $p$ and $q$ on a group $E$, the underlying function of their supremum $p \sqcup q$ is equal to the pointwise supremum of the underlying functions of $p$ and $q$. That is, for all $x \in E$, we have $(p \sqcup q)(x) = \max(p(x), q(x))$.
GroupSeminorm.sup_apply theorem
(x : E) : (p ⊔ q) x = p x ⊔ q x
Full source 
@[to_additive (attr := simp)]
theorem sup_apply (x : E) : (p ⊔ q) x = p x ⊔ q x :=
  rfl
Pointwise Maximum Property of Group Seminorm Supremum
Informal description
For any group $E$ and any two group seminorms $p, q$ on $E$, the value of their supremum $p \sqcup q$ at any element $x \in E$ is equal to the maximum of $p(x)$ and $q(x)$, i.e., $(p \sqcup q)(x) = \max(p(x), q(x))$.
GroupSeminorm.semilatticeSup instance
: SemilatticeSup (GroupSeminorm E)
Full source 
@[to_additive]
instance semilatticeSup : SemilatticeSup (GroupSeminorm E) :=
  DFunLike.coe_injective.semilatticeSup _ coe_sup
Join-Semilattice Structure on Group Seminorms
Informal description
The set of group seminorms on a group $E$ forms a join-semilattice, where the supremum operation is defined pointwise. That is, for any two group seminorms $p$ and $q$ on $E$, their supremum $p \sqcup q$ is the group seminorm given by $(p \sqcup q)(x) = \max(p(x), q(x))$ for all $x \in E$.
GroupSeminorm.comp definition
(p : GroupSeminorm E) (f : F →* E) : GroupSeminorm F
Full source 
/-- Composition of a group seminorm with a monoid homomorphism as a group seminorm. -/
@[to_additive "Composition of an additive group seminorm with an additive monoid homomorphism as an
additive group seminorm."]
def comp (p : GroupSeminorm E) (f : F →* E) : GroupSeminorm F where
  toFun x := p (f x)
  map_one' := by simp_rw [f.map_one, map_one_eq_zero p]
  mul_le' _ _ := (congr_arg p <| f.map_mul _ _).trans_le <| map_mul_le_add p _ _
  inv' x := by simp_rw [map_inv, map_inv_eq_map p]
Composition of a group seminorm with a monoid homomorphism
Informal description
Given a group seminorm \( p \) on a group \( E \) and a monoid homomorphism \( f \colon F \to E \), the composition \( p \circ f \) defines a group seminorm on \( F \). Explicitly, this seminorm maps \( x \in F \) to \( p(f(x)) \), and satisfies: 1. \( p(f(1)) = 0 \) (preserves identity) 2. \( p(f(xy)) \leq p(f(x)) + p(f(y)) \) for all \( x, y \in F \) (subadditive) 3. \( p(f(x^{-1})) = p(f(x)) \) for all \( x \in F \) (inverse-invariant)
GroupSeminorm.coe_comp theorem
: ⇑(p.comp f) = p ∘ f
Full source 
@[to_additive (attr := simp)]
theorem coe_comp : ⇑(p.comp f) = p ∘ f :=
  rfl
Function Representation of Composed Group Seminorm
Informal description
For a group seminorm $p$ on a group $E$ and a monoid homomorphism $f \colon F \to E$, the function representation of the composition $p \circ f$ is equal to the pointwise composition of $p$ with $f$, i.e., $(p \circ f)(x) = p(f(x))$ for all $x \in F$.
GroupSeminorm.comp_apply theorem
(x : F) : (p.comp f) x = p (f x)
Full source 
@[to_additive (attr := simp)]
theorem comp_apply (x : F) : (p.comp f) x = p (f x) :=
  rfl
Evaluation of Composed Group Seminorm: $(p \circ f)(x) = p(f(x))$
Informal description
For a group seminorm $p$ on a group $E$, a monoid homomorphism $f \colon F \to E$, and an element $x \in F$, the value of the composed seminorm $p \circ f$ at $x$ is equal to $p(f(x))$.
GroupSeminorm.comp_id theorem
: p.comp (MonoidHom.id _) = p
Full source 
@[to_additive (attr := simp)]
theorem comp_id : p.comp (MonoidHom.id _) = p :=
  ext fun _ => rfl
Identity Composition Preserves Group Seminorm: $p \circ \text{id} = p$
Informal description
For any group seminorm $p$ on a group $G$, the composition of $p$ with the identity monoid homomorphism on $G$ is equal to $p$ itself, i.e., $p \circ \text{id} = p$.
GroupSeminorm.comp_zero theorem
: p.comp (1 : F →* E) = 0
Full source 
@[to_additive (attr := simp)]
theorem comp_zero : p.comp (1 : F →* E) = 0 :=
  ext fun _ => map_one_eq_zero p
Composition with Constant One Homomorphism Yields Zero Seminorm
Informal description
For any group seminorm $p$ on a group $E$, the composition of $p$ with the constant monoid homomorphism $1 \colon F \to E$ (which sends every element of $F$ to the identity element of $E$) yields the zero seminorm on $F$, i.e., $(p \circ 1)(x) = 0$ for all $x \in F$.
GroupSeminorm.zero_comp theorem
: (0 : GroupSeminorm E).comp f = 0
Full source 
@[to_additive (attr := simp)]
theorem zero_comp : (0 : GroupSeminorm E).comp f = 0 :=
  ext fun _ => rfl
Composition of Zero Seminorm with Homomorphism Yields Zero Seminorm
Informal description
For any monoid homomorphism $f \colon F \to E$, the composition of the zero group seminorm on $E$ with $f$ is the zero group seminorm on $F$, i.e., $(0 \circ f)(x) = 0$ for all $x \in F$.
GroupSeminorm.comp_assoc theorem
(g : F →* E) (f : G →* F) : p.comp (g.comp f) = (p.comp g).comp f
Full source 
@[to_additive]
theorem comp_assoc (g : F →* E) (f : G →* F) : p.comp (g.comp f) = (p.comp g).comp f :=
  ext fun _ => rfl
Associativity of Group Seminorm Composition
Informal description
Let $p$ be a group seminorm on a group $E$, and let $g \colon F \to E$ and $f \colon G \to F$ be monoid homomorphisms. Then the composition of $p$ with the composition of $g$ and $f$ is equal to the composition of the composition of $p$ with $g$ and $f$, i.e., \[ p \circ (g \circ f) = (p \circ g) \circ f. \]
GroupSeminorm.add_comp theorem
(f : F →* E) : (p + q).comp f = p.comp f + q.comp f
Full source 
@[to_additive]
theorem add_comp (f : F →* E) : (p + q).comp f = p.comp f + q.comp f :=
  ext fun _ => rfl
Additivity of Group Seminorm Composition: $(p + q) \circ f = p \circ f + q \circ f$
Informal description
Let $p$ and $q$ be group seminorms on a group $E$, and let $f \colon F \to E$ be a monoid homomorphism. Then the composition of the sum $p + q$ with $f$ equals the sum of the compositions, i.e., $$(p + q) \circ f = (p \circ f) + (q \circ f).$$
GroupSeminorm.comp_mono theorem
(hp : p ≤ q) : p.comp f ≤ q.comp f
Full source 
@[to_additive]
theorem comp_mono (hp : p ≤ q) : p.comp f ≤ q.comp f := fun _ => hp _
Monotonicity of Group Seminorm Composition
Informal description
Let $p$ and $q$ be group seminorms on a group $E$ such that $p \leq q$ (i.e., $p(x) \leq q(x)$ for all $x \in E$). Then for any monoid homomorphism $f \colon F \to E$, the composition seminorms satisfy $(p \circ f)(x) \leq (q \circ f)(x)$ for all $x \in F$.
GroupSeminorm.comp_mul_le theorem
(f g : F →* E) : p.comp (f * g) ≤ p.comp f + p.comp g
Full source 
@[to_additive]
theorem comp_mul_le (f g : F →* E) : p.comp (f * g) ≤ p.comp f + p.comp g := fun _ =>
  map_mul_le_add p _ _
Subadditivity of Group Seminorm Composition under Pointwise Product
Informal description
Let $p$ be a group seminorm on a group $E$, and let $f, g \colon F \to E$ be monoid homomorphisms. Then the composition seminorm satisfies the inequality: $$ p \circ (f \cdot g) \leq p \circ f + p \circ g $$ where $(f \cdot g)(x) = f(x) \cdot g(x)$ denotes the pointwise product of $f$ and $g$.
GroupSeminorm.mul_bddBelow_range_add theorem
{p q : GroupSeminorm E} {x : E} : BddBelow (range fun y => p y + q (x / y))
Full source 
@[to_additive]
theorem mul_bddBelow_range_add {p q : GroupSeminorm E} {x : E} :
    BddBelow (range fun y => p y + q (x / y)) :=
  ⟨0, by
    rintro _ ⟨x, rfl⟩
    dsimp
    positivity⟩
Lower Boundedness of Combined Group Seminorm Values
Informal description
For any group seminorms $p$ and $q$ on a group $E$ and any element $x \in E$, the set $\{p(y) + q(x/y) \mid y \in E\}$ is bounded below.
GroupSeminorm.instMin instance
: Min (GroupSeminorm E)
Full source 
@[to_additive]
noncomputable instance : Min (GroupSeminorm E) :=
  ⟨fun p q =>
    { toFun := fun x => ⨅ y, p y + q (x / y)
      map_one' :=
        ciInf_eq_of_forall_ge_of_forall_gt_exists_lt
          (fun _ => by positivity) fun r hr =>
          ⟨1, by rwa [div_one, map_one_eq_zero p, map_one_eq_zero q, add_zero]⟩
      mul_le' := fun x y =>
        le_ciInf_add_ciInf fun u v => by
          refine ciInf_le_of_le mul_bddBelow_range_add (u * v) ?_
          rw [mul_div_mul_comm, add_add_add_comm]
          exact add_le_add (map_mul_le_add p _ _) (map_mul_le_add q _ _)
      inv' := fun x =>
        (inv_surjective.iInf_comp _).symm.trans <| by
          simp_rw [map_inv_eq_map p, ← inv_div', map_inv_eq_map q] }⟩
Minimum Operation on Group Seminorms
Informal description
For any group $E$, the set of group seminorms on $E$ has a minimum operation.
GroupSeminorm.inf_apply theorem
: (p ⊓ q) x = ⨅ y, p y + q (x / y)
Full source 
@[to_additive (attr := simp)]
theorem inf_apply : (p ⊓ q) x = ⨅ y, p y + q (x / y) :=
  rfl
Infimum of Group Seminorms Formula
Informal description
For any group seminorms $p$ and $q$ on a group $E$, and any element $x \in E$, the value of the infimum seminorm $p \sqcap q$ at $x$ is given by the infimum over all $y \in E$ of the sum $p(y) + q(x/y)$. In other words, $$(p \sqcap q)(x) = \inf_{y \in E} \big(p(y) + q(x/y)\big).$$
GroupSeminorm.instLattice instance
: Lattice (GroupSeminorm E)
Full source 
@[to_additive]
noncomputable instance : Lattice (GroupSeminorm E) :=
  { GroupSeminorm.semilatticeSup with
    inf := (· ⊓ ·)
    inf_le_left := fun p q x =>
      ciInf_le_of_le mul_bddBelow_range_add x <| by rw [div_self', map_one_eq_zero q, add_zero]
    inf_le_right := fun p q x =>
      ciInf_le_of_le mul_bddBelow_range_add (1 : E) <| by
        simpa only [div_one x, map_one_eq_zero p, zero_add (q x)] using le_rfl
    le_inf := fun a _ _ hb hc _ =>
      le_ciInf fun _ => (le_map_add_map_div a _ _).trans <| add_le_add (hb _) (hc _) }
Lattice Structure on Group Seminorms
Informal description
The set of group seminorms on a group $E$ forms a lattice, where the supremum and infimum operations are defined pointwise. That is, for any two group seminorms $p$ and $q$ on $E$, their supremum $p \sqcup q$ is the group seminorm given by $(p \sqcup q)(x) = \max(p(x), q(x))$ for all $x \in E$, and their infimum $p \sqcap q$ is the group seminorm given by $(p \sqcap q)(x) = \inf_{y \in E} \big(p(y) + q(x/y)\big)$ for all $x \in E$.
AddGroupSeminorm.toOne instance
[DecidableEq E] : One (AddGroupSeminorm E)
Full source 
instance toOne [DecidableEq E] : One (AddGroupSeminorm E) :=
  ⟨{  toFun := fun x => if x = 0 then 0 else 1
      map_zero' := if_pos rfl
      add_le' := fun x y => by
        by_cases hx : x = 0
        · rw [if_pos hx, hx, zero_add, zero_add]
        · rw [if_neg hx]
          refine le_add_of_le_of_nonneg ?_ ?_ <;> split_ifs <;> norm_num
      neg' := fun x => by simp_rw [neg_eq_zero] }⟩
Trivial Additive Group Seminorm
Informal description
For any additive group $E$ with decidable equality, there is a canonical way to define a trivial additive group seminorm $1$ on $E$ that maps $0$ to $0$ and all other elements to $1$.
AddGroupSeminorm.apply_one theorem
[DecidableEq E] (x : E) : (1 : AddGroupSeminorm E) x = if x = 0 then 0 else 1
Full source 
@[simp]
theorem apply_one [DecidableEq E] (x : E) : (1 : AddGroupSeminorm E) x = if x = 0 then 0 else 1 :=
  rfl
Evaluation of Trivial Additive Group Seminorm
Informal description
For any additive group $E$ with decidable equality, the trivial additive group seminorm $1$ evaluated at an element $x \in E$ is defined as: \[ 1(x) = \begin{cases} 0 & \text{if } x = 0, \\ 1 & \text{otherwise}. \end{cases} \]
AddGroupSeminorm.toSMul instance
: SMul R (AddGroupSeminorm E)
Full source 
/-- Any action on `ℝ` which factors through `ℝ≥0` applies to an `AddGroupSeminorm`. -/
instance toSMul : SMul R (AddGroupSeminorm E) :=
  ⟨fun r p =>
    { toFun := fun x => r • p x
      map_zero' := by
        simp only [← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul, map_zero, mul_zero]
      add_le' := fun _ _ => by
        simp only [← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul, ← mul_add]
        gcongr
        apply map_add_le_add
      neg' := fun x => by simp_rw [map_neg_eq_map] }⟩
Scalar Multiplication on Additive Group Seminorms
Informal description
For any scalar action on $\mathbb{R}$ that factors through $\mathbb{R}_{\geq 0}$, there is a corresponding scalar multiplication operation on additive group seminorms. Specifically, if $R$ is a type with a scalar multiplication operation on $\mathbb{R}$ that preserves nonnegativity, then $R$ also has a scalar multiplication operation on the space of additive group seminorms on an additive group $E$.
AddGroupSeminorm.coe_smul theorem
(r : R) (p : AddGroupSeminorm E) : ⇑(r • p) = r • ⇑p
Full source 
@[simp, norm_cast]
theorem coe_smul (r : R) (p : AddGroupSeminorm E) : ⇑(r • p) = r • ⇑p :=
  rfl
Scalar Multiplication of Additive Group Seminorms: $(r \cdot p)(x) = r \cdot p(x)$
Informal description
For any scalar $r \in R$ and any additive group seminorm $p$ on an additive group $E$, the function corresponding to the scalar multiple $r \cdot p$ is equal to the scalar multiple of the function corresponding to $p$, i.e., $(r \cdot p)(x) = r \cdot p(x)$ for all $x \in E$.
AddGroupSeminorm.smul_apply theorem
(r : R) (p : AddGroupSeminorm E) (x : E) : (r • p) x = r • p x
Full source 
@[simp]
theorem smul_apply (r : R) (p : AddGroupSeminorm E) (x : E) : (r • p) x = r • p x :=
  rfl
Scalar multiplication of additive group seminorms: $(r \cdot p)(x) = r \cdot p(x)$
Informal description
For any scalar $r \in R$, any additive group seminorm $p$ on an additive group $E$, and any element $x \in E$, the seminorm $(r \cdot p)(x)$ is equal to $r \cdot p(x)$.
AddGroupSeminorm.isScalarTower instance
[SMul R' ℝ] [SMul R' ℝ≥0] [IsScalarTower R' ℝ≥0 ℝ] [SMul R R'] [IsScalarTower R R' ℝ] : IsScalarTower R R' (AddGroupSeminorm E)
Full source 
instance isScalarTower [SMul R' ℝ] [SMul R' ℝ≥0] [IsScalarTower R' ℝ≥0 ℝ] [SMul R R']
    [IsScalarTower R R' ℝ] : IsScalarTower R R' (AddGroupSeminorm E) :=
  ⟨fun r a p => ext fun x => smul_assoc r a (p x)⟩
Scalar Tower Structure on Additive Group Seminorms
Informal description
For any types $R$ and $R'$ with scalar multiplication operations on $\mathbb{R}$ and $\mathbb{R}_{\geq 0}$ respectively, such that $R'$ forms a scalar tower over $\mathbb{R}_{\geq 0}$ and $\mathbb{R}$, and $R$ forms a scalar tower over $R'$ and $\mathbb{R}$, the space of additive group seminorms on an additive group $E$ also forms a scalar tower over $R$ and $R'$.
AddGroupSeminorm.smul_sup theorem
(r : R) (p q : AddGroupSeminorm E) : r • (p ⊔ q) = r • p ⊔ r • q
Full source 
theorem smul_sup (r : R) (p q : AddGroupSeminorm E) : r • (p ⊔ q) = r • p ⊔ r • q :=
  have Real.smul_max : ∀ x y : ℝ, r • max x y = max (r • x) (r • y) := fun x y => by
    simpa only [← smul_eq_mul, ← NNReal.smul_def, smul_one_smul ℝ≥0 r (_ : ℝ)] using
      mul_max_of_nonneg x y (r • (1 : ℝ≥0) : ℝ≥0).coe_nonneg
  ext fun _ => Real.smul_max _ _
Scalar Multiplication Distributes Over Supremum of Additive Group Seminorms
Informal description
Let $R$ be a type with a scalar multiplication operation on $\mathbb{R}$ that factors through $\mathbb{R}_{\geq 0}$, and let $E$ be an additive group. For any scalar $r \in R$ and any two additive group seminorms $p, q$ on $E$, the following equality holds: \[ r \cdot (p \sqcup q) = (r \cdot p) \sqcup (r \cdot q), \] where $\sqcup$ denotes the pointwise supremum of seminorms.
NonarchAddGroupSeminorm.funLike instance
: FunLike (NonarchAddGroupSeminorm E) E ℝ
Full source 
instance funLike : FunLike (NonarchAddGroupSeminorm E) E ℝ where
  coe f := f.toFun
  coe_injective' f g h := by obtain ⟨⟨_, _⟩, _, _⟩ := f; cases g; congr
Function-Like Structure of Nonarchimedean Additive Group Seminorms
Informal description
For any additive group $E$, the type of nonarchimedean additive group seminorms on $E$ is a function-like class, where each seminorm $f$ can be treated as a function from $E$ to $\mathbb{R}$.
NonarchAddGroupSeminorm.nonarchAddGroupSeminormClass instance
: NonarchAddGroupSeminormClass (NonarchAddGroupSeminorm E) E
Full source 
instance nonarchAddGroupSeminormClass :
    NonarchAddGroupSeminormClass (NonarchAddGroupSeminorm E) E where
  map_add_le_max f := f.add_le_max'
  map_zero f := f.map_zero'
  map_neg_eq_map' f := f.neg'
Nonarchimedean Additive Group Seminorm Class
Informal description
For any additive group $E$, the type of nonarchimedean additive group seminorms on $E$ forms a class of nonarchimedean seminorms. This means each seminorm $f$ in this class satisfies: 1. $f(0) = 0$, 2. $f(x) \geq 0$ for all $x \in E$, 3. $f(-x) = f(x)$ for all $x \in E$, and 4. $f(x + y) \leq \max(f(x), f(y))$ for all $x, y \in E$.
NonarchAddGroupSeminorm.toZeroHom_eq_coe theorem
: ⇑p.toZeroHom = p
Full source 
@[simp]
theorem toZeroHom_eq_coe : ⇑p.toZeroHom = p := by
  rfl
Equality of Zero-Preserving Homomorphism and Seminorm Function
Informal description
For any nonarchimedean additive group seminorm $p$ on an additive group $G$, the underlying zero-preserving homomorphism of $p$ is equal to $p$ itself when viewed as a function from $G$ to $\mathbb{R}$.
NonarchAddGroupSeminorm.ext theorem
: (∀ x, p x = q x) → p = q
Full source 
@[ext]
theorem ext : (∀ x, p x = q x) → p = q :=
  DFunLike.ext p q
Extensionality of Nonarchimedean Additive Group Seminorms
Informal description
For any two nonarchimedean additive group seminorms $p$ and $q$ on an additive group $G$, if $p(x) = q(x)$ for all $x \in G$, then $p = q$.
NonarchAddGroupSeminorm.instPartialOrder instance
: PartialOrder (NonarchAddGroupSeminorm E)
Full source 
noncomputable instance : PartialOrder (NonarchAddGroupSeminorm E) :=
  PartialOrder.lift _ DFunLike.coe_injective
Partial Order on Nonarchimedean Additive Group Seminorms
Informal description
The set of nonarchimedean additive group seminorms on an additive group $E$ forms a partial order, where the order relation is defined pointwise: for two seminorms $p$ and $q$, $p \leq q$ if and only if $p(x) \leq q(x)$ for all $x \in E$.
NonarchAddGroupSeminorm.le_def theorem
: p ≤ q ↔ (p : E → ℝ) ≤ q
Full source 
theorem le_def : p ≤ q ↔ (p : E → ℝ) ≤ q :=
  Iff.rfl
Pointwise Order Characterization for Nonarchimedean Additive Group Seminorms
Informal description
For two nonarchimedean additive group seminorms $p$ and $q$ on an additive group $E$, the inequality $p \leq q$ holds if and only if $p(x) \leq q(x)$ for all $x \in E$.
NonarchAddGroupSeminorm.lt_def theorem
: p < q ↔ (p : E → ℝ) < q
Full source 
theorem lt_def : p < q ↔ (p : E → ℝ) < q :=
  Iff.rfl
Pointwise Strict Order Characterization for Nonarchimedean Additive Group Seminorms
Informal description
For two nonarchimedean additive group seminorms $p$ and $q$ on an additive group $E$, the strict inequality $p < q$ holds if and only if $p(x) < q(x)$ for all $x \in E$.
NonarchAddGroupSeminorm.coe_le_coe theorem
: (p : E → ℝ) ≤ q ↔ p ≤ q
Full source 
@[simp, norm_cast]
theorem coe_le_coe : (p : E → ℝ) ≤ q ↔ p ≤ q :=
  Iff.rfl
Pointwise Inequality Characterization for Nonarchimedean Additive Group Seminorms
Informal description
For two nonarchimedean additive group seminorms $p$ and $q$ on an additive group $E$, the pointwise inequality $p(x) \leq q(x)$ holds for all $x \in E$ if and only if $p \leq q$ in the partial order of seminorms.
NonarchAddGroupSeminorm.coe_lt_coe theorem
: (p : E → ℝ) < q ↔ p < q
Full source 
@[simp, norm_cast]
theorem coe_lt_coe : (p : E → ℝ) < q ↔ p < q :=
  Iff.rfl
Pointwise Strict Inequality of Nonarchimedean Additive Group Seminorms
Informal description
For two nonarchimedean additive group seminorms $p$ and $q$ on an additive group $E$, the pointwise strict inequality $p(x) < q(x)$ holds for all $x \in E$ if and only if $p < q$ in the partial order of seminorms.
NonarchAddGroupSeminorm.coe_zero theorem
: ⇑(0 : NonarchAddGroupSeminorm E) = 0
Full source 
@[simp, norm_cast]
theorem coe_zero : ⇑(0 : NonarchAddGroupSeminorm E) = 0 :=
  rfl
Zero Nonarchimedean Additive Group Seminorm Evaluates to Zero
Informal description
The zero nonarchimedean additive group seminorm, when applied to any element $x$ of the additive group $E$, yields zero, i.e., $0(x) = 0$ for all $x \in E$.
NonarchAddGroupSeminorm.zero_apply theorem
(x : E) : (0 : NonarchAddGroupSeminorm E) x = 0
Full source 
@[simp]
theorem zero_apply (x : E) : (0 : NonarchAddGroupSeminorm E) x = 0 :=
  rfl
Zero Nonarchimedean Seminorm Evaluates to Zero
Informal description
For any element $x$ in an additive group $E$, the zero nonarchimedean additive group seminorm evaluated at $x$ is equal to zero, i.e., $0(x) = 0$.
NonarchAddGroupSeminorm.instInhabited instance
: Inhabited (NonarchAddGroupSeminorm E)
Full source 
instance : Inhabited (NonarchAddGroupSeminorm E) :=
  ⟨0⟩
Existence of Nonarchimedean Additive Group Seminorms
Informal description
The type of nonarchimedean additive group seminorms on an additive group $E$ is inhabited, meaning there exists at least one such seminorm.
NonarchAddGroupSeminorm.instMax instance
: Max (NonarchAddGroupSeminorm E)
Full source 
instance : Max (NonarchAddGroupSeminorm E) :=
  ⟨fun p q =>
    { toFun := p ⊔ q
      map_zero' := by rw [Pi.sup_apply, ← map_zero p, sup_eq_left, map_zero p, map_zero q]
      add_le_max' := fun x y =>
        sup_le ((map_add_le_max p x y).trans <| max_le_max le_sup_left le_sup_left)
          ((map_add_le_max q x y).trans <| max_le_max le_sup_right le_sup_right)
      neg' := fun x => by simp_rw [Pi.sup_apply, map_neg_eq_map p, map_neg_eq_map q]}⟩
Pointwise Maximum Operation on Nonarchimedean Additive Group Seminorms
Informal description
For any additive group $E$, the set of nonarchimedean additive group seminorms on $E$ has a maximum operation defined pointwise. That is, for any two seminorms $p$ and $q$, their supremum $p \sqcup q$ is the seminorm given by $(p \sqcup q)(x) = \max(p(x), q(x))$ for all $x \in E$.
NonarchAddGroupSeminorm.coe_sup theorem
: ⇑(p ⊔ q) = ⇑p ⊔ ⇑q
Full source 
@[simp, norm_cast]
theorem coe_sup : ⇑(p ⊔ q) = ⇑p ⊔ ⇑q :=
  rfl
Pointwise Maximum of Nonarchimedean Additive Group Seminorms
Informal description
For any two nonarchimedean additive group seminorms $p$ and $q$ on an additive group $E$, the underlying function of their supremum $p \sqcup q$ is equal to the pointwise maximum of the underlying functions of $p$ and $q$. That is, $(p \sqcup q)(x) = \max(p(x), q(x))$ for all $x \in E$.
NonarchAddGroupSeminorm.sup_apply theorem
(x : E) : (p ⊔ q) x = p x ⊔ q x
Full source 
@[simp]
theorem sup_apply (x : E) : (p ⊔ q) x = p x ⊔ q x :=
  rfl
Pointwise Maximum Property of Nonarchimedean Additive Group Seminorms
Informal description
For any nonarchimedean additive group seminorms $p$ and $q$ on an additive group $E$, and for any element $x \in E$, the value of the pointwise maximum seminorm $p \sqcup q$ at $x$ equals the maximum of $p(x)$ and $q(x)$, i.e., $(p \sqcup q)(x) = \max(p(x), q(x))$.
NonarchAddGroupSeminorm.instSemilatticeSup instance
: SemilatticeSup (NonarchAddGroupSeminorm E)
Full source 
noncomputable instance : SemilatticeSup (NonarchAddGroupSeminorm E) :=
  DFunLike.coe_injective.semilatticeSup _ coe_sup
Join-Semilattice Structure on Nonarchimedean Additive Group Seminorms
Informal description
For any additive group $E$, the set of nonarchimedean additive group seminorms on $E$ forms a join-semilattice with the pointwise supremum operation. That is, for any two seminorms $p$ and $q$, their supremum $p \sqcup q$ is defined by $(p \sqcup q)(x) = \max(p(x), q(x))$ for all $x \in E$.
NonarchAddGroupSeminorm.add_bddBelow_range_add theorem
{p q : NonarchAddGroupSeminorm E} {x : E} : BddBelow (range fun y => p y + q (x - y))
Full source 
theorem add_bddBelow_range_add {p q : NonarchAddGroupSeminorm E} {x : E} :
    BddBelow (range fun y => p y + q (x - y)) :=
  ⟨0, by
    rintro _ ⟨x, rfl⟩
    dsimp
    positivity⟩
Lower Boundedness of Combined Nonarchimedean Seminorms
Informal description
For any nonarchimedean additive group seminorms $p$ and $q$ on an additive group $E$, and for any element $x \in E$, the set $\{p(y) + q(x - y) \mid y \in E\}$ is bounded below.
GroupSeminorm.toOne instance
[DecidableEq E] : One (GroupSeminorm E)
Full source 
@[to_additive existing AddGroupSeminorm.toOne]
instance toOne [DecidableEq E] : One (GroupSeminorm E) :=
  ⟨{  toFun := fun x => if x = 1 then 0 else 1
      map_one' := if_pos rfl
      mul_le' := fun x y => by
        by_cases hx : x = 1
        · rw [if_pos hx, hx, one_mul, zero_add]
        · rw [if_neg hx]
          refine le_add_of_le_of_nonneg ?_ ?_ <;> split_ifs <;> norm_num
      inv' := fun x => by simp_rw [inv_eq_one] }⟩
The One Element in Group Seminorms
Informal description
For any group $E$ with decidable equality, the group seminorms on $E$ form a structure with a distinguished element $1$, which is the seminorm defined by $f(x) = 0$ if $x = 1$ and $f(x) = 1$ otherwise.
GroupSeminorm.apply_one theorem
[DecidableEq E] (x : E) : (1 : GroupSeminorm E) x = if x = 1 then 0 else 1
Full source 
@[to_additive existing (attr := simp) AddGroupSeminorm.apply_one]
theorem apply_one [DecidableEq E] (x : E) : (1 : GroupSeminorm E) x = if x = 1 then 0 else 1 :=
  rfl
Evaluation of the One Group Seminorm
Informal description
For any group $E$ with decidable equality, the group seminorm $1$ evaluated at an element $x \in E$ satisfies: \[ 1(x) = \begin{cases} 0 & \text{if } x = 1, \\ 1 & \text{otherwise}. \end{cases} \]
GroupSeminorm.instSMul instance
: SMul R (GroupSeminorm E)
Full source 
/-- Any action on `ℝ` which factors through `ℝ≥0` applies to an `AddGroupSeminorm`. -/
@[to_additive existing AddGroupSeminorm.toSMul]
instance : SMul R (GroupSeminorm E) :=
  ⟨fun r p =>
    { toFun := fun x => r • p x
      map_one' := by
        simp only [← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul, map_one_eq_zero p,
          mul_zero]
      mul_le' := fun _ _ => by
        simp only [← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul, ← mul_add]
        gcongr
        apply map_mul_le_add
      inv' := fun x => by simp_rw [map_inv_eq_map p] }⟩
Scalar Multiplication on Group Seminorms
Informal description
For any type $R$ and group $E$, the group seminorms on $E$ can be equipped with a scalar multiplication operation by elements of $R$, provided that $R$ has an action on $\mathbb{R}$ that factors through $\mathbb{R}_{\geq 0}$.
GroupSeminorm.instIsScalarTowerOfReal instance
[SMul R' ℝ] [SMul R' ℝ≥0] [IsScalarTower R' ℝ≥0 ℝ] [SMul R R'] [IsScalarTower R R' ℝ] : IsScalarTower R R' (GroupSeminorm E)
Full source 
@[to_additive existing AddGroupSeminorm.isScalarTower]
instance [SMul R' ℝ] [SMul R' ℝ≥0] [IsScalarTower R' ℝ≥0 ℝ] [SMul R R'] [IsScalarTower R R' ℝ] :
    IsScalarTower R R' (GroupSeminorm E) :=
  ⟨fun r a p => ext fun x => smul_assoc r a <| p x⟩
Scalar Tower Structure on Group Seminorms
Informal description
For any types $R$ and $R'$ with scalar multiplication actions on $\mathbb{R}$ and $\mathbb{R}_{\geq 0}$ such that $R'$ forms a scalar tower over $\mathbb{R}_{\geq 0}$ and $\mathbb{R}$, and $R$ forms a scalar tower over $R'$ and $\mathbb{R}$, the group seminorms on a group $E$ inherit a scalar tower structure from $R$ to $R'$.
GroupSeminorm.coe_smul theorem
(r : R) (p : GroupSeminorm E) : ⇑(r • p) = r • ⇑p
Full source 
@[to_additive existing (attr := simp, norm_cast) AddGroupSeminorm.coe_smul]
theorem coe_smul (r : R) (p : GroupSeminorm E) : ⇑(r • p) = r • ⇑p :=
  rfl
Scalar Multiplication Preserves Function Representation of Group Seminorms
Informal description
For any scalar $r$ in a type $R$ and any group seminorm $p$ on a group $E$, the function associated with the scalar multiple $r \cdot p$ is equal to the scalar multiple $r$ applied to the function associated with $p$. In other words, $(r \cdot p)(x) = r \cdot p(x)$ for all $x \in E$.
GroupSeminorm.smul_apply theorem
(r : R) (p : GroupSeminorm E) (x : E) : (r • p) x = r • p x
Full source 
@[to_additive existing (attr := simp) AddGroupSeminorm.smul_apply]
theorem smul_apply (r : R) (p : GroupSeminorm E) (x : E) : (r • p) x = r • p x :=
  rfl
Scalar Multiplication Preserves Evaluation of Group Seminorms
Informal description
For any scalar $r$ in a type $R$, any group seminorm $p$ on a group $E$, and any element $x \in E$, the evaluation of the scalar multiple $r \cdot p$ at $x$ equals the scalar multiple $r$ of the evaluation $p(x)$, i.e., $(r \cdot p)(x) = r \cdot p(x)$.
GroupSeminorm.smul_sup theorem
(r : R) (p q : GroupSeminorm E) : r • (p ⊔ q) = r • p ⊔ r • q
Full source 
@[to_additive existing AddGroupSeminorm.smul_sup]
theorem smul_sup (r : R) (p q : GroupSeminorm E) : r • (p ⊔ q) = r • p ⊔ r • q :=
  have Real.smul_max : ∀ x y : ℝ, r • max x y = max (r • x) (r • y) := fun x y => by
    simpa only [← smul_eq_mul, ← NNReal.smul_def, smul_one_smul ℝ≥0 r (_ : ℝ)] using
      mul_max_of_nonneg x y (r • (1 : ℝ≥0) : ℝ≥0).coe_nonneg
  ext fun _ => Real.smul_max _ _
Scalar Multiplication Distributes Over Maximum of Group Seminorms: $r \cdot \max(p, q) = \max(r \cdot p, r \cdot q)$
Informal description
Let $R$ be a type with a scalar multiplication operation on $\mathbb{R}_{\geq 0}$, and let $E$ be a group. For any scalar $r \in R$ and any two group seminorms $p, q$ on $E$, the scalar multiple of the pointwise maximum seminorm satisfies: \[ r \cdot (\max(p, q)) = \max(r \cdot p, r \cdot q). \] Here, $\max(p, q)$ denotes the group seminorm defined by $\max(p, q)(x) = \max(p(x), q(x))$ for all $x \in E$.
NonarchAddGroupSeminorm.instOneOfDecidableEq instance
[DecidableEq E] : One (NonarchAddGroupSeminorm E)
Full source 
instance [DecidableEq E] : One (NonarchAddGroupSeminorm E) :=
  ⟨{  toFun := fun x => if x = 0 then 0 else 1
      map_zero' := if_pos rfl
      add_le_max' := fun x y => by
        by_cases hx : x = 0
        · simp_rw [if_pos hx, hx, zero_add]
          exact le_max_of_le_right (le_refl _)
        · simp_rw [if_neg hx]
          split_ifs <;> simp
      neg' := fun x => by simp_rw [neg_eq_zero] }⟩
The Indicator Nonarchimedean Seminorm on an Additive Group with Decidable Equality
Informal description
For any additive group $E$ with decidable equality, there is a canonical nonarchimedean additive group seminorm defined by $1(x) = 0$ if $x = 0$ and $1(x) = 1$ otherwise.
NonarchAddGroupSeminorm.apply_one theorem
[DecidableEq E] (x : E) : (1 : NonarchAddGroupSeminorm E) x = if x = 0 then 0 else 1
Full source 
@[simp]
theorem apply_one [DecidableEq E] (x : E) :
    (1 : NonarchAddGroupSeminorm E) x = if x = 0 then 0 else 1 :=
  rfl
Evaluation of the Indicator Seminorm on an Additive Group
Informal description
For any additive group $E$ with decidable equality, the indicator seminorm $1$ evaluated at an element $x \in E$ is defined as: \[ 1(x) = \begin{cases} 0 & \text{if } x = 0, \\ 1 & \text{otherwise.} \end{cases} \]
NonarchAddGroupSeminorm.instSMul instance
: SMul R (NonarchAddGroupSeminorm E)
Full source 
/-- Any action on `ℝ` which factors through `ℝ≥0` applies to a `NonarchAddGroupSeminorm`. -/
instance : SMul R (NonarchAddGroupSeminorm E) :=
  ⟨fun r p =>
    { toFun := fun x => r • p x
      map_zero' := by
        simp only [← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul, map_zero p,
          mul_zero]
      add_le_max' := fun x y => by
        simp only [← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul, ←
          mul_max_of_nonneg _ _ NNReal.zero_le_coe]
        gcongr
        apply map_add_le_max
      neg' := fun x => by simp_rw [map_neg_eq_map p] }⟩
Scalar Multiplication on Nonarchimedean Additive Group Seminorms
Informal description
For any type $R$ with a scalar multiplication action on $\mathbb{R}$ that factors through $\mathbb{R}_{\geq 0}$, the type of nonarchimedean additive group seminorms on an additive group $E$ inherits a scalar multiplication structure from $R$. Specifically, for any scalar $r \in R$ and seminorm $p$, the scalar multiple $r \cdot p$ is defined pointwise as $(r \cdot p)(x) = r \cdot p(x)$ for all $x \in E$.
NonarchAddGroupSeminorm.instIsScalarTowerOfReal instance
[SMul R' ℝ] [SMul R' ℝ≥0] [IsScalarTower R' ℝ≥0 ℝ] [SMul R R'] [IsScalarTower R R' ℝ] : IsScalarTower R R' (NonarchAddGroupSeminorm E)
Full source 
instance [SMul R' ℝ] [SMul R' ℝ≥0] [IsScalarTower R' ℝ≥0 ℝ] [SMul R R'] [IsScalarTower R R' ℝ] :
    IsScalarTower R R' (NonarchAddGroupSeminorm E) :=
  ⟨fun r a p => ext fun x => smul_assoc r a <| p x⟩
Scalar Tower Structure on Nonarchimedean Additive Group Seminorms
Informal description
For any types $R$ and $R'$ with scalar multiplication actions on $\mathbb{R}$ and $\mathbb{R}_{\geq 0}$ such that $R'$ forms a scalar tower over $\mathbb{R}_{\geq 0}$ and $\mathbb{R}$, and $R$ forms a scalar tower over $R'$ and $\mathbb{R}$, the nonarchimedean additive group seminorms on an additive group $E$ inherit a scalar tower structure from $R$ and $R'$.
NonarchAddGroupSeminorm.coe_smul theorem
(r : R) (p : NonarchAddGroupSeminorm E) : ⇑(r • p) = r • ⇑p
Full source 
@[simp, norm_cast]
theorem coe_smul (r : R) (p : NonarchAddGroupSeminorm E) : ⇑(r • p) = r • ⇑p :=
  rfl
Scalar Multiplication Preserves Function Application for Nonarchimedean Additive Group Seminorms
Informal description
For any scalar $r \in R$ and nonarchimedean additive group seminorm $p$ on an additive group $E$, the underlying function of the scalar multiple $r \cdot p$ is equal to the scalar multiple of the underlying function of $p$, i.e., $(r \cdot p)(x) = r \cdot p(x)$ for all $x \in E$.
NonarchAddGroupSeminorm.smul_apply theorem
(r : R) (p : NonarchAddGroupSeminorm E) (x : E) : (r • p) x = r • p x
Full source 
@[simp]
theorem smul_apply (r : R) (p : NonarchAddGroupSeminorm E) (x : E) : (r • p) x = r • p x :=
  rfl
Scalar Multiplication of Nonarchimedean Seminorm Evaluates to Scalar Multiple
Informal description
For any scalar $r \in R$, any nonarchimedean additive group seminorm $p$ on an additive group $E$, and any element $x \in E$, the evaluation of the scalar multiple $r \cdot p$ at $x$ is equal to the scalar multiple of the evaluation of $p$ at $x$, i.e., $(r \cdot p)(x) = r \cdot p(x)$.
NonarchAddGroupSeminorm.smul_sup theorem
(r : R) (p q : NonarchAddGroupSeminorm E) : r • (p ⊔ q) = r • p ⊔ r • q
Full source 
theorem smul_sup (r : R) (p q : NonarchAddGroupSeminorm E) : r • (p ⊔ q) = r • p ⊔ r • q :=
  have Real.smul_max : ∀ x y : ℝ, r • max x y = max (r • x) (r • y) := fun x y => by
    simpa only [← smul_eq_mul, ← NNReal.smul_def, smul_one_smul ℝ≥0 r (_ : ℝ)] using
      mul_max_of_nonneg x y (r • (1 : ℝ≥0) : ℝ≥0).coe_nonneg
  ext fun _ => Real.smul_max _ _
Scalar Multiplication Distributes Over Pointwise Maximum of Nonarchimedean Seminorms
Informal description
For any scalar $r \in R$ and any two nonarchimedean additive group seminorms $p$ and $q$ on an additive group $E$, the scalar multiple of their pointwise supremum equals the supremum of their scalar multiples. That is: \[ r \cdot (\max(p, q)) = \max(r \cdot p, r \cdot q). \]
GroupNorm.funLike instance
: FunLike (GroupNorm E) E ℝ
Full source 
@[to_additive]
instance funLike : FunLike (GroupNorm E) E ℝ where
  coe f := f.toFun
  coe_injective' f g h := by obtain ⟨⟨_, _, _, _⟩, _⟩ := f; cases g; congr
Function-Like Structure of Group Norms
Informal description
For any group $E$, the type of group norms on $E$ can be treated as a function-like type, where each group norm $f$ can be coerced to a function from $E$ to $\mathbb{R}$.
GroupNorm.groupNormClass instance
: GroupNormClass (GroupNorm E) E ℝ
Full source 
@[to_additive]
instance groupNormClass : GroupNormClass (GroupNorm E) E ℝ where
  map_one_eq_zero f := f.map_one'
  map_mul_le_add f := f.mul_le'
  map_inv_eq_map f := f.inv'
  eq_one_of_map_eq_zero f := f.eq_one_of_map_eq_zero' _
Group Norms Satisfy the Group Norm Class Properties
Informal description
For any group $E$, the type of group norms on $E$ forms a `GroupNormClass`, meaning that every group norm $f \colon E \to \mathbb{R}$ satisfies the following properties: 1. (Nonnegativity) $0 \leq f(a)$ for all $a \in E$, 2. (Subadditivity) $f(ab) \leq f(a) + f(b)$ for all $a, b \in E$, 3. (Inversion invariance) $f(a^{-1}) = f(a)$ for all $a \in E$, 4. (Positivity) $f(a) = 0$ implies $a = 1$ for all $a \in E$.
GroupNorm.toGroupSeminorm_eq_coe theorem
: ⇑p.toGroupSeminorm = p
Full source 
@[to_additive (attr := simp)]
theorem toGroupSeminorm_eq_coe : ⇑p.toGroupSeminorm = p :=
  rfl
Equality of Group Norm and its Underlying Seminorm
Informal description
For any group norm $p$ on a group $G$, the underlying group seminorm of $p$ is equal to $p$ when viewed as a function from $G$ to $\mathbb{R}$.
GroupNorm.ext theorem
: (∀ x, p x = q x) → p = q
Full source 
@[to_additive (attr := ext)]
theorem ext : (∀ x, p x = q x) → p = q :=
  DFunLike.ext p q
Extensionality of Group Norms
Informal description
For any two group norms $p$ and $q$ on a group $G$, if $p(x) = q(x)$ for all $x \in G$, then $p = q$.
GroupNorm.instPartialOrder instance
: PartialOrder (GroupNorm E)
Full source 
@[to_additive]
instance : PartialOrder (GroupNorm E) :=
  PartialOrder.lift _ DFunLike.coe_injective
Partial Order on Group Norms
Informal description
The set of group norms on a group $E$ forms a partial order, where the ordering is defined pointwise: for two group norms $p$ and $q$, we have $p \leq q$ if and only if $p(x) \leq q(x)$ for all $x \in E$.
GroupNorm.le_def theorem
: p ≤ q ↔ (p : E → ℝ) ≤ q
Full source 
@[to_additive]
theorem le_def : p ≤ q ↔ (p : E → ℝ) ≤ q :=
  Iff.rfl
Pointwise Order Characterization for Group Norms
Informal description
For two group norms $p$ and $q$ on a group $E$, the inequality $p \leq q$ holds if and only if $p(x) \leq q(x)$ for all $x \in E$.
GroupNorm.lt_def theorem
: p < q ↔ (p : E → ℝ) < q
Full source 
@[to_additive]
theorem lt_def : p < q ↔ (p : E → ℝ) < q :=
  Iff.rfl
Strict Pointwise Order Characterization for Group Norms
Informal description
For two group norms $p$ and $q$ on a group $E$, the strict inequality $p < q$ holds if and only if the function $p$ is pointwise strictly less than $q$ on all elements of $E$.
GroupNorm.coe_le_coe theorem
: (p : E → ℝ) ≤ q ↔ p ≤ q
Full source 
@[to_additive (attr := simp, norm_cast)]
theorem coe_le_coe : (p : E → ℝ) ≤ q ↔ p ≤ q :=
  Iff.rfl
Pointwise Order on Group Norms
Informal description
For two group norms $p$ and $q$ on a group $E$, the pointwise inequality $p(x) \leq q(x)$ for all $x \in E$ holds if and only if $p \leq q$ in the partial order of group norms.
GroupNorm.coe_lt_coe theorem
: (p : E → ℝ) < q ↔ p < q
Full source 
@[to_additive (attr := simp, norm_cast)]
theorem coe_lt_coe : (p : E → ℝ) < q ↔ p < q :=
  Iff.rfl
Pointwise Strict Order Characterization for Group Norms
Informal description
For two group norms $p$ and $q$ on a group $E$, the pointwise strict inequality $p(x) < q(x)$ holds for all $x \in E$ if and only if $p < q$ in the partial order of group norms.
GroupNorm.instAdd instance
: Add (GroupNorm E)
Full source 
@[to_additive]
instance : Add (GroupNorm E) :=
  ⟨fun p q =>
    { p.toGroupSeminorm + q.toGroupSeminorm with
      eq_one_of_map_eq_zero' := fun _x hx =>
        of_not_not fun h => hx.not_gt <| add_pos (map_pos_of_ne_one p h) (map_pos_of_ne_one q h) }⟩
Additive Structure on Group Norms
Informal description
For any group $E$, the set of group norms on $E$ forms an additive structure, where the addition of two group norms $p$ and $q$ is defined pointwise as $(p + q)(x) = p(x) + q(x)$ for all $x \in E$.
GroupNorm.coe_add theorem
: ⇑(p + q) = p + q
Full source 
@[to_additive (attr := simp)]
theorem coe_add : ⇑(p + q) = p + q :=
  rfl
Pointwise Sum of Group Norms
Informal description
For any two group norms $p$ and $q$ on a group $E$, the function corresponding to their sum $p + q$ is equal to the pointwise sum of the functions $p$ and $q$, i.e., $(p + q)(x) = p(x) + q(x)$ for all $x \in E$.
GroupNorm.add_apply theorem
(x : E) : (p + q) x = p x + q x
Full source 
@[to_additive (attr := simp)]
theorem add_apply (x : E) : (p + q) x = p x + q x :=
  rfl
Pointwise Addition Formula for Group Norms
Informal description
For any group $E$ and group norms $p, q$ on $E$, the sum of norms evaluated at any element $x \in E$ equals the sum of their evaluations, i.e., $(p + q)(x) = p(x) + q(x)$.
GroupNorm.instMax instance
: Max (GroupNorm E)
Full source 
@[to_additive]
instance : Max (GroupNorm E) :=
  ⟨fun p q =>
    { p.toGroupSeminorm ⊔ q.toGroupSeminorm with
      eq_one_of_map_eq_zero' := fun _x hx =>
        of_not_not fun h => hx.not_gt <| lt_sup_iff.2 <| Or.inl <| map_pos_of_ne_one p h }⟩
Pointwise Maximum Operation on Group Norms
Informal description
For any group $E$, the set of group norms on $E$ has a maximum operation defined pointwise. That is, for any two group norms $p$ and $q$ on $E$, their supremum $p \sqcup q$ is the group norm given by $(p \sqcup q)(x) = \max(p(x), q(x))$ for all $x \in E$.
GroupNorm.coe_sup theorem
: ⇑(p ⊔ q) = ⇑p ⊔ ⇑q
Full source 
@[to_additive (attr := simp, norm_cast)]
theorem coe_sup : ⇑(p ⊔ q) = ⇑p ⊔ ⇑q :=
  rfl
Pointwise Supremum of Group Norms
Informal description
For any two group norms $p$ and $q$ on a group $E$, the function corresponding to their supremum $p \sqcup q$ is equal to the pointwise supremum of the functions $p$ and $q$. That is, $(p \sqcup q)(x) = \max(p(x), q(x))$ for all $x \in E$.
GroupNorm.sup_apply theorem
(x : E) : (p ⊔ q) x = p x ⊔ q x
Full source 
@[to_additive (attr := simp)]
theorem sup_apply (x : E) : (p ⊔ q) x = p x ⊔ q x :=
  rfl
Pointwise Maximum Property of Group Norms
Informal description
For any group $E$ and any two group norms $p, q$ on $E$, the supremum norm $p \sqcup q$ evaluated at any element $x \in E$ equals the maximum of $p(x)$ and $q(x)$, i.e., $(p \sqcup q)(x) = \max(p(x), q(x))$.
GroupNorm.instSemilatticeSup instance
: SemilatticeSup (GroupNorm E)
Full source 
@[to_additive]
instance : SemilatticeSup (GroupNorm E) :=
  DFunLike.coe_injective.semilatticeSup _ coe_sup
Join-Semilattice Structure on Group Norms
Informal description
For any group $E$, the set of group norms on $E$ forms a join-semilattice under the pointwise supremum operation. That is, for any two group norms $p$ and $q$ on $E$, their supremum $p \sqcup q$ is the group norm defined by $(p \sqcup q)(x) = \max(p(x), q(x))$ for all $x \in E$.
AddGroupNorm.apply_one theorem
(x : E) : (1 : AddGroupNorm E) x = if x = 0 then 0 else 1
Full source 
@[simp]
theorem apply_one (x : E) : (1 : AddGroupNorm E) x = if x = 0 then 0 else 1 :=
  rfl
Evaluation of Trivial Additive Group Norm
Informal description
For any element $x$ in an additive group $E$, the trivial additive group norm evaluated at $x$ is defined as: \[ 1(x) = \begin{cases} 0 & \text{if } x = 0, \\ 1 & \text{otherwise.} \end{cases} \]
AddGroupNorm.instInhabited instance
: Inhabited (AddGroupNorm E)
Full source 
instance : Inhabited (AddGroupNorm E) :=
  ⟨1⟩
Existence of Additive Group Norms
Informal description
For any additive group $E$, the type of additive group norms on $E$ is inhabited. In other words, there exists at least one additive group norm on $E$.
AddGroupNorm.toOne instance
[AddGroup E] [DecidableEq E] : One (AddGroupNorm E)
Full source 
instance _root_.AddGroupNorm.toOne [AddGroup E] [DecidableEq E] : One (AddGroupNorm E) :=
  ⟨{ (1 : AddGroupSeminorm E) with
    eq_zero_of_map_eq_zero' := fun _ => zero_ne_one.ite_eq_left_iff.1 }⟩
The Trivial Additive Group Norm
Informal description
For any additive group $E$ with decidable equality, there is a canonical additive group norm $1$ on $E$ defined by $1(x) = 0$ if $x = 0$ and $1(x) = 1$ otherwise.
GroupNorm.apply_one theorem
(x : E) : (1 : GroupNorm E) x = if x = 1 then 0 else 1
Full source 
@[to_additive existing (attr := simp) AddGroupNorm.apply_one]
theorem apply_one (x : E) : (1 : GroupNorm E) x = if x = 1 then 0 else 1 :=
  rfl
Evaluation of the Trivial Group Norm
Informal description
For any element $x$ in a group $E$, the trivial group norm evaluated at $x$ is defined as: \[ 1(x) = \begin{cases} 0 & \text{if } x = 1, \\ 1 & \text{otherwise.} \end{cases} \]
GroupNorm.instInhabited instance
: Inhabited (GroupNorm E)
Full source 
@[to_additive existing]
instance : Inhabited (GroupNorm E) :=
  ⟨1⟩
Existence of Group Norms
Informal description
The type of group norms on a group $E$ is inhabited.
NonarchAddGroupNorm.funLike instance
: FunLike (NonarchAddGroupNorm E) E ℝ
Full source 
instance funLike : FunLike (NonarchAddGroupNorm E) E ℝ where
  coe f := f.toFun
  coe_injective' f g h := by obtain ⟨⟨⟨_, _⟩, _, _⟩, _⟩ := f; cases g; congr
Function-Like Structure of Nonarchimedean Additive Group Norms
Informal description
For any additive group $E$, the type of nonarchimedean additive group norms on $E$ has a function-like structure, where each norm $f$ can be viewed as a function from $E$ to $\mathbb{R}$.
NonarchAddGroupNorm.nonarchAddGroupNormClass instance
: NonarchAddGroupNormClass (NonarchAddGroupNorm E) E
Full source 
instance nonarchAddGroupNormClass : NonarchAddGroupNormClass (NonarchAddGroupNorm E) E where
  map_add_le_max f := f.add_le_max'
  map_zero f := f.map_zero'
  map_neg_eq_map' f := f.neg'
  eq_zero_of_map_eq_zero f := f.eq_zero_of_map_eq_zero' _
Nonarchimedean Additive Group Norm Class Structure
Informal description
The type of nonarchimedean additive group norms on an additive group $E$ forms a `NonarchAddGroupNormClass`, meaning it satisfies the properties of nonarchimedean norms: for any norm $f$ in this class, $f(0) = 0$, $f(x) \geq 0$ for all $x \in E$, $f(-x) = f(x)$, $f(x + y) \leq \max(f(x), f(y))$, and $f(x) = 0$ implies $x = 0$.
NonarchAddGroupNorm.toNonarchAddGroupSeminorm_eq_coe theorem
: ⇑p.toNonarchAddGroupSeminorm = p
Full source 
@[simp]
theorem toNonarchAddGroupSeminorm_eq_coe : ⇑p.toNonarchAddGroupSeminorm = p :=
  rfl
Equality of Nonarchimedean Norm and Its Underlying Seminorm
Informal description
For any nonarchimedean additive group norm $p$ on an additive group $E$, the underlying seminorm of $p$ is equal to $p$ itself when viewed as a function from $E$ to $\mathbb{R}$.
NonarchAddGroupNorm.ext theorem
: (∀ x, p x = q x) → p = q
Full source 
@[ext]
theorem ext : (∀ x, p x = q x) → p = q :=
  DFunLike.ext p q
Extensionality of Nonarchimedean Additive Group Norms
Informal description
For any two nonarchimedean additive group norms $p$ and $q$ on an additive group $G$, if $p(x) = q(x)$ for all $x \in G$, then $p = q$.
NonarchAddGroupNorm.instPartialOrder instance
: PartialOrder (NonarchAddGroupNorm E)
Full source 
noncomputable instance : PartialOrder (NonarchAddGroupNorm E) :=
  PartialOrder.lift _ DFunLike.coe_injective
Partial Order on Nonarchimedean Additive Group Norms
Informal description
The set of nonarchimedean additive group norms on an additive group $E$ forms a partial order, where the ordering is defined pointwise: for two norms $p$ and $q$, we have $p \leq q$ if and only if $p(x) \leq q(x)$ for all $x \in E$.
NonarchAddGroupNorm.le_def theorem
: p ≤ q ↔ (p : E → ℝ) ≤ q
Full source 
theorem le_def : p ≤ q ↔ (p : E → ℝ) ≤ q :=
  Iff.rfl
Pointwise Order Characterization for Nonarchimedean Additive Group Norms
Informal description
For two nonarchimedean additive group norms $p$ and $q$ on an additive group $E$, the inequality $p \leq q$ holds if and only if the corresponding real-valued functions satisfy $p(x) \leq q(x)$ for all $x \in E$.
NonarchAddGroupNorm.lt_def theorem
: p < q ↔ (p : E → ℝ) < q
Full source 
theorem lt_def : p < q ↔ (p : E → ℝ) < q :=
  Iff.rfl
Pointwise Strict Order Characterization for Nonarchimedean Additive Group Norms
Informal description
For two nonarchimedean additive group norms $p$ and $q$ on an additive group $E$, the strict inequality $p < q$ holds if and only if the corresponding real-valued functions satisfy $p(x) < q(x)$ for all $x \in E$.
NonarchAddGroupNorm.coe_le_coe theorem
: (p : E → ℝ) ≤ q ↔ p ≤ q
Full source 
@[simp, norm_cast]
theorem coe_le_coe : (p : E → ℝ) ≤ q ↔ p ≤ q :=
  Iff.rfl
Pointwise Inequality Characterization for Nonarchimedean Additive Group Norms
Informal description
For two nonarchimedean additive group norms $p$ and $q$ on an additive group $E$, the pointwise inequality $p(x) \leq q(x)$ for all $x \in E$ holds if and only if $p \leq q$ in the partial order of norms.
NonarchAddGroupNorm.coe_lt_coe theorem
: (p : E → ℝ) < q ↔ p < q
Full source 
@[simp, norm_cast]
theorem coe_lt_coe : (p : E → ℝ) < q ↔ p < q :=
  Iff.rfl
Pointwise Strict Inequality of Nonarchimedean Additive Group Norms
Informal description
For two nonarchimedean additive group norms $p$ and $q$ on an additive group $E$, the pointwise strict inequality $p(x) < q(x)$ for all $x \in E$ holds if and only if $p < q$ in the partial order of norms.
NonarchAddGroupNorm.instMax instance
: Max (NonarchAddGroupNorm E)
Full source 
instance : Max (NonarchAddGroupNorm E) :=
  ⟨fun p q =>
    { p.toNonarchAddGroupSeminorm ⊔ q.toNonarchAddGroupSeminorm with
      eq_zero_of_map_eq_zero' := fun _x hx =>
        of_not_not fun h => hx.not_gt <| lt_sup_iff.2 <| Or.inl <| map_pos_of_ne_zero p h }⟩
Pointwise Maximum Operation on Nonarchimedean Additive Group Norms
Informal description
For any additive group $E$, the set of nonarchimedean additive group norms on $E$ has a maximum operation defined pointwise. That is, for any two norms $p$ and $q$, their supremum $p \sqcup q$ is the norm given by $(p \sqcup q)(x) = \max(p(x), q(x))$ for all $x \in E$.
NonarchAddGroupNorm.coe_sup theorem
: ⇑(p ⊔ q) = ⇑p ⊔ ⇑q
Full source 
@[simp, norm_cast]
theorem coe_sup : ⇑(p ⊔ q) = ⇑p ⊔ ⇑q :=
  rfl
Pointwise Supremum of Nonarchimedean Additive Group Norms
Informal description
For any nonarchimedean additive group norms $p$ and $q$ on an additive group $E$, the function corresponding to the supremum $p \sqcup q$ is equal to the pointwise supremum of the functions $p$ and $q$, i.e., $(p \sqcup q)(x) = \max(p(x), q(x))$ for all $x \in E$.
NonarchAddGroupNorm.sup_apply theorem
(x : E) : (p ⊔ q) x = p x ⊔ q x
Full source 
@[simp]
theorem sup_apply (x : E) : (p ⊔ q) x = p x ⊔ q x :=
  rfl
Pointwise Maximum Formula for Nonarchimedean Additive Group Norms
Informal description
For any nonarchimedean additive group norms $p$ and $q$ on an additive group $E$, and for any element $x \in E$, the value of the pointwise supremum norm $p \sqcup q$ at $x$ is equal to the maximum of $p(x)$ and $q(x)$, i.e., $(p \sqcup q)(x) = \max(p(x), q(x))$.
NonarchAddGroupNorm.instSemilatticeSup instance
: SemilatticeSup (NonarchAddGroupNorm E)
Full source 
noncomputable instance : SemilatticeSup (NonarchAddGroupNorm E) :=
  DFunLike.coe_injective.semilatticeSup _ coe_sup
Join-Semilattice Structure on Nonarchimedean Additive Group Norms
Informal description
For any additive group $E$, the set of nonarchimedean additive group norms on $E$ forms a join-semilattice with the pointwise supremum operation.
NonarchAddGroupNorm.instOneOfDecidableEq instance
[DecidableEq E] : One (NonarchAddGroupNorm E)
Full source 
instance [DecidableEq E] : One (NonarchAddGroupNorm E) :=
  ⟨{ (1 : NonarchAddGroupSeminorm E) with
      eq_zero_of_map_eq_zero' := fun _ => zero_ne_one.ite_eq_left_iff.1 }⟩
The Indicator Nonarchimedean Norm on an Additive Group with Decidable Equality
Informal description
For any additive group $E$ with decidable equality, there is a canonical nonarchimedean additive group norm defined by $1(x) = 0$ if $x = 0$ and $1(x) = 1$ otherwise.
NonarchAddGroupNorm.apply_one theorem
[DecidableEq E] (x : E) : (1 : NonarchAddGroupNorm E) x = if x = 0 then 0 else 1
Full source 
@[simp]
theorem apply_one [DecidableEq E] (x : E) :
    (1 : NonarchAddGroupNorm E) x = if x = 0 then 0 else 1 :=
  rfl
Evaluation of the Indicator Nonarchimedean Norm
Informal description
For any additive group $E$ with decidable equality, the indicator nonarchimedean norm $1$ evaluated at an element $x \in E$ satisfies: \[ 1(x) = \begin{cases} 0 & \text{if } x = 0 \\ 1 & \text{otherwise} \end{cases} \]
NonarchAddGroupNorm.instInhabitedOfDecidableEq instance
[DecidableEq E] : Inhabited (NonarchAddGroupNorm E)
Full source 
instance [DecidableEq E] : Inhabited (NonarchAddGroupNorm E) :=
  ⟨1⟩
Inhabitedness of Nonarchimedean Additive Group Norms
Informal description
For any additive group $E$ with decidable equality, the type of nonarchimedean additive group norms on $E$ is inhabited.