Mathlib.Analysis.Normed.Group.Basic

Norm structure

(E : Type*)

Full source

/-- Auxiliary class, endowing a type `E` with a function `norm : E → ℝ` with notation `‖x‖`. This
class is designed to be extended in more interesting classes specifying the properties of the norm.
-/
@[notation_class]
class Norm (E : Type*) where
  /-- the `ℝ`-valued norm function. -/
  norm : E → ℝ

Norm

Informal description

The structure `Norm` endows a type `E` with a function $\| \cdot \| : E \to \mathbb{R}$, called the norm. This is an auxiliary class designed to be extended by more specific classes that impose additional properties on the norm function.

NNNorm structure

(E : Type*)

Full source

/-- Auxiliary class, endowing a type `α` with a function `nnnorm : α → ℝ≥0` with notation `‖x‖₊`. -/
@[notation_class]
class NNNorm (E : Type*) where
  /-- the `ℝ≥0`-valued norm function. -/
  nnnorm : E → ℝ≥0

Non-negative norm

Informal description

The structure `NNNorm` endows a type `E` with a function `nnnorm : E → ℝ≥0` (notation: `‖x‖₊`), which assigns to each element of `E` a non-negative real number representing its norm.

ENorm structure

(E : Type*)

Full source

/-- Auxiliary class, endowing a type `α` with a function `enorm : α → ℝ≥0∞` with notation `‖x‖ₑ`. -/
@[notation_class]
class ENorm (E : Type*) where
  /-- the `ℝ≥0∞`-valued norm function. -/
  enorm : E → ℝ≥0∞

Extended norm

Informal description

The structure `ENorm` endows a type `E` with an extended norm function `‖·‖ₑ : E → ℝ≥0∞`, where `ℝ≥0∞` denotes the extended non-negative real numbers (including infinity). This auxiliary class is used to define norms that can take infinite values.

term‖_‖ definition

: Lean.ParserDescr✝

Full source

@[inherit_doc] notation "‖" e "‖" => norm e

Norm notation

Informal description

The notation `‖x‖` represents the norm of an element `x` in a normed space, which is a real number.

term‖_‖₊ definition

: Lean.ParserDescr✝

Full source

@[inherit_doc] notation "‖" e "‖₊" => nnnorm e

Non-negative norm notation

Informal description

The notation `‖x‖₊` represents the non-negative norm of an element `x`, which is a function mapping `x` to a non-negative real number (ℝ≥0).

term‖_‖ₑ definition

: Lean.ParserDescr✝

Full source

@[inherit_doc] notation "‖" e "‖ₑ" => enorm e

Extended norm notation

Informal description

The notation `‖e‖ₑ` represents the extended norm of an element `e`, where `enorm` is the extended norm function.

NNNorm.toENorm instance

: ENorm E

Full source

instance NNNorm.toENorm : ENorm E where enorm := (‖·‖₊ : E → ℝ≥0∞)

Non-negative Norm Induces Extended Norm

Informal description

For any type $E$ equipped with a non-negative norm $\|\cdot\|_+ : E \to \mathbb{R}_{\geq 0}$, there is a corresponding extended norm $\|\cdot\|_e : E \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ defined by $\|x\|_e = \|x\|_+$.

enorm_eq_nnnorm theorem

(x : E) : ‖x‖ₑ = ‖x‖₊

Full source

lemma enorm_eq_nnnorm (x : E) : ‖x‖ₑ = ‖x‖₊ := rfl

Extended Norm Equals Non-Negative Norm: $\|x\|_e = \|x\|_+$

Informal description

For any element $x$ in a type $E$ equipped with a non-negative norm $\|\cdot\|_+$, the extended norm $\|x\|_e$ is equal to the non-negative norm $\|x\|_+$.

toNNReal_enorm theorem

(x : E) : ‖x‖ₑ.toNNReal = ‖x‖₊

Full source

@[simp] lemma toNNReal_enorm (x : E) : ‖x‖ₑ.toNNReal = ‖x‖₊ := rfl

Conversion of Extended Norm to Non-Negative Norm: $\|x\|_e.\text{toNNReal} = \|x\|_+$

Informal description

For any element $x$ in a type $E$ equipped with a non-negative norm $\|\cdot\|_+$, the conversion of the extended norm $\|x\|_e$ to a non-negative real number equals the non-negative norm $\|x\|_+$, i.e., $\|x\|_e.\text{toNNReal} = \|x\|_+$.

coe_le_enorm theorem

: r ≤ ‖x‖ₑ ↔ r ≤ ‖x‖₊

Full source

@[simp, norm_cast] lemma coe_le_enorm : r ≤ ‖x‖ₑ ↔ r ≤ ‖x‖₊ := by simp [enorm]

Inequality Relating Nonnegative Real Number to Extended Norm and Nonnegative Norm: $r \leq \|x\|_e \leftrightarrow r \leq \|x\|_+$

Informal description

For any nonnegative real number $r$ and any element $x$ in a space $E$ with extended norm $\|x\|_e$ and nonnegative norm $\|x\|_+$, the inequality $r \leq \|x\|_e$ holds if and only if $r \leq \|x\|_+$.

enorm_le_coe theorem

: ‖x‖ₑ ≤ r ↔ ‖x‖₊ ≤ r

Full source

@[simp, norm_cast] lemma enorm_le_coe : ‖x‖ₑ‖x‖ₑ ≤ r ↔ ‖x‖₊ ≤ r := by simp [enorm]

Extended Norm Bounded by Real Number if and only if Non-Negative Norm Is

Informal description

coe_lt_enorm theorem

: r < ‖x‖ₑ ↔ r < ‖x‖₊

Full source

@[simp, norm_cast] lemma coe_lt_enorm : r < ‖x‖ₑ ↔ r < ‖x‖₊ := by simp [enorm]

Inequality Relating Nonnegative Real Number to Extended Norm and Nonnegative Norm

Informal description

enorm_lt_coe theorem

: ‖x‖ₑ < r ↔ ‖x‖₊ < r

Full source

@[simp, norm_cast] lemma enorm_lt_coe : ‖x‖ₑ‖x‖ₑ < r ↔ ‖x‖₊ < r := by simp [enorm]

Extended Norm vs Non-negative Norm Inequality: $\|x\|_e < r \leftrightarrow \|x\|_+ < r$

Informal description

enorm_ne_top theorem

: ‖x‖ₑ ≠ ∞

Full source

@[simp] lemma enorm_ne_top : ‖x‖ₑ‖x‖ₑ ≠ ∞ := by simp [enorm]

Extended Norm is Finite

Informal description

For any element $x$ in a space $E$ equipped with an extended norm $\|\cdot\|_e$, the extended norm of $x$ is not equal to infinity, i.e., $\|x\|_e \neq \infty$.

enorm_lt_top theorem

: ‖x‖ₑ < ∞

Full source

@[simp] lemma enorm_lt_top : ‖x‖ₑ < ∞ := by simp [enorm]

Finite Extended Norm Property

Informal description

For any element $x$ in a space $E$ equipped with an extended norm $\|\cdot\|_e$, the extended norm of $x$ is finite, i.e., $\|x\|_e < \infty$.

ContinuousENorm structure

(E : Type*) [TopologicalSpace E] extends ENorm E

Full source

/-- A type `E` equipped with a continuous map `‖·‖ₑ : E → ℝ≥0∞`

NB. We do not demand that the topology is somehow defined by the enorm:
for ℝ≥0∞ (the motivating example behind this definition), this is not true. -/
class ContinuousENorm (E : Type*) [TopologicalSpace E] extends ENorm E where
  continuous_enorm : Continuous enorm

Continuous extended norm

Informal description

A structure `ContinuousENorm` extends the `ENorm` structure on a topological space `E`, ensuring that the extended norm function `‖·‖ₑ : E → ℝ≥0∞` is continuous. Note that this does not require the topology on `E` to be induced by the extended norm; for example, this is not the case for `ℝ≥0∞` (the motivating example for this definition).

ENormedAddMonoid structure

(E : Type*) [TopologicalSpace E] extends ContinuousENorm E, AddMonoid E

Full source

/-- An enormed monoid is an additive monoid endowed with a continuous enorm. -/
class ENormedAddMonoid (E : Type*) [TopologicalSpace E] extends ContinuousENorm E, AddMonoid E where
  enorm_eq_zero : ∀ x : E, ‖x‖ₑ‖x‖ₑ = 0 ↔ x = 0
  protected enorm_add_le : ∀ x y : E, ‖x + y‖ₑ ≤ ‖x‖ₑ + ‖y‖ₑ

Extended Normed Additive Monoid

Informal description

An `ENormedAddMonoid` is an additive monoid $E$ equipped with a topological space structure and a continuous extended norm function $\|\cdot\|_e : E \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ that satisfies the properties of an extended norm (nonnegativity, zero norm implies zero, triangle inequality, and continuity).

ENormedMonoid structure

(E : Type*) [TopologicalSpace E] extends ContinuousENorm E, Monoid E

Full source

/-- An enormed monoid is a monoid endowed with a continuous enorm. -/
@[to_additive]
class ENormedMonoid (E : Type*) [TopologicalSpace E] extends ContinuousENorm E, Monoid E where
  enorm_eq_zero : ∀ x : E, ‖x‖ₑ‖x‖ₑ = 0 ↔ x = 1
  enorm_mul_le : ∀ x y : E, ‖x * y‖ₑ ≤ ‖x‖ₑ + ‖y‖ₑ

Enormed monoid

Informal description

An enormed monoid is a monoid $E$ equipped with a topological space structure and a continuous enorm function $\| \cdot \| \colon E \to \mathbb{R}$ that satisfies the properties of an enorm (extending the `ENorm` class) while being compatible with the monoid operation.

ENormedAddCommMonoid structure

(E : Type*) [TopologicalSpace E]
  extends ENormedAddMonoid E, AddCommMonoid E

Full source

/-- An enormed commutative monoid is an additive commutative monoid
endowed with a continuous enorm.

We don't have `ENormedAddCommMonoid` extend `EMetricSpace`, since the canonical instance `ℝ≥0∞`
is not an `EMetricSpace`. This is because `ℝ≥0∞` carries the order topology, which is distinct from
the topology coming from `edist`. -/
class ENormedAddCommMonoid (E : Type*) [TopologicalSpace E]
  extends ENormedAddMonoid E, AddCommMonoid E where

Enormed Additive Commutative Monoid

Informal description

An `ENormedAddCommMonoid` is an additive commutative monoid $E$ equipped with a topological space structure and a continuous enorm function, which extends the properties of an `ENormedAddMonoid` (a monoid with a continuous enorm) and an additive commutative monoid. This structure does not extend an `EMetricSpace` because the canonical example $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is not an `EMetricSpace` under the order topology.

ENormedCommMonoid structure

(E : Type*) [TopologicalSpace E] extends ENormedMonoid E, CommMonoid E

Full source

/-- An enormed commutative monoid is a commutative monoid endowed with a continuous enorm. -/
@[to_additive]
class ENormedCommMonoid (E : Type*) [TopologicalSpace E] extends ENormedMonoid E, CommMonoid E where

E-normed commutative monoid

Informal description

An e-normed commutative monoid is a commutative monoid $E$ equipped with a topological space structure and a continuous e-norm function, where the e-norm is compatible with the monoid operation.

SeminormedAddGroup structure

(E : Type*) extends Norm E, AddGroup E, PseudoMetricSpace E

Full source

/-- A seminormed group is an additive group endowed with a norm for which `dist x y = ‖x - y‖`
defines a pseudometric space structure. -/
class SeminormedAddGroup (E : Type*) extends Norm E, AddGroup E, PseudoMetricSpace E where
  dist := fun x y => ‖x - y‖
  /-- The distance function is induced by the norm. -/
  dist_eq : ∀ x y, dist x y = ‖x - y‖ := by aesop

Seminormed additive group

Informal description

A seminormed additive group is an additive group $E$ endowed with a norm function $\|\cdot\| : E \to \mathbb{R}$ and a pseudometric space structure, where the pseudometric is defined by $d(x, y) = \|x - y\|$ for all $x, y \in E$.

SeminormedGroup structure

(E : Type*) extends Norm E, Group E, PseudoMetricSpace E

Full source

/-- A seminormed group is a group endowed with a norm for which `dist x y = ‖x / y‖` defines a
pseudometric space structure. -/
@[to_additive]
class SeminormedGroup (E : Type*) extends Norm E, Group E, PseudoMetricSpace E where
  dist := fun x y => ‖x / y‖
  /-- The distance function is induced by the norm. -/
  dist_eq : ∀ x y, dist x y = ‖x / y‖ := by aesop

Seminormed group

Informal description

A seminormed group is a group $E$ equipped with a norm function $\|\cdot\| : E \to \mathbb{R}$ and a pseudometric space structure, where the distance between elements $x$ and $y$ is given by $\|x / y\|$.

NormedAddGroup structure

(E : Type*) extends Norm E, AddGroup E, MetricSpace E

Full source

/-- A normed group is an additive group endowed with a norm for which `dist x y = ‖x - y‖` defines a
metric space structure. -/
class NormedAddGroup (E : Type*) extends Norm E, AddGroup E, MetricSpace E where
  dist := fun x y => ‖x - y‖
  /-- The distance function is induced by the norm. -/
  dist_eq : ∀ x y, dist x y = ‖x - y‖ := by aesop

Normed additive group

Informal description

A normed additive group is an additive group $ E $ endowed with a norm function $ \|\cdot\| : E \to \mathbb{R} $ such that the distance between any two elements $ x, y \in E $ is given by $ \text{dist}(x, y) = \|x - y\| $, making $ E $ a metric space.

NormedGroup structure

(E : Type*) extends Norm E, Group E, MetricSpace E

Full source

/-- A normed group is a group endowed with a norm for which `dist x y = ‖x / y‖` defines a metric
space structure. -/
@[to_additive]
class NormedGroup (E : Type*) extends Norm E, Group E, MetricSpace E where
  dist := fun x y => ‖x / y‖
  /-- The distance function is induced by the norm. -/
  dist_eq : ∀ x y, dist x y = ‖x / y‖ := by aesop

Normed group

Informal description

A normed group is a group $E$ equipped with a norm function $\|\cdot\| : E \to \mathbb{R}$ and a metric space structure, where the distance between elements $x$ and $y$ is given by $\|x / y\|$.

SeminormedAddCommGroup structure

(E : Type*) extends Norm E, AddCommGroup E,
  PseudoMetricSpace E

Full source

/-- A seminormed group is an additive group endowed with a norm for which `dist x y = ‖x - y‖`
defines a pseudometric space structure. -/
class SeminormedAddCommGroup (E : Type*) extends Norm E, AddCommGroup E,
  PseudoMetricSpace E where
  dist := fun x y => ‖x - y‖
  /-- The distance function is induced by the norm. -/
  dist_eq : ∀ x y, dist x y = ‖x - y‖ := by aesop

Seminormed additive commutative group

Informal description

A seminormed additive commutative group is an additive commutative group $E$ endowed with a norm function $\|\cdot\| : E \to \mathbb{R}$ and a pseudometric space structure, where the distance between elements $x$ and $y$ is given by $\|x - y\|$.

SeminormedCommGroup structure

(E : Type*) extends Norm E, CommGroup E, PseudoMetricSpace E

Full source

/-- A seminormed group is a group endowed with a norm for which `dist x y = ‖x / y‖`
defines a pseudometric space structure. -/
@[to_additive]
class SeminormedCommGroup (E : Type*) extends Norm E, CommGroup E, PseudoMetricSpace E where
  dist := fun x y => ‖x / y‖
  /-- The distance function is induced by the norm. -/
  dist_eq : ∀ x y, dist x y = ‖x / y‖ := by aesop

Seminormed commutative group

Informal description

A seminormed commutative group is a commutative group $ E $ endowed with a norm function $ \|\cdot\| : E \to \mathbb{R} $ and a pseudometric space structure, where the distance between any two elements $ x, y \in E $ is given by $ \text{dist}(x, y) = \|x / y\| $.

NormedAddCommGroup structure

(E : Type*) extends Norm E, AddCommGroup E, MetricSpace E

Full source

/-- A normed group is an additive group endowed with a norm for which `dist x y = ‖x - y‖` defines a
metric space structure. -/
class NormedAddCommGroup (E : Type*) extends Norm E, AddCommGroup E, MetricSpace E where
  dist := fun x y => ‖x - y‖
  /-- The distance function is induced by the norm. -/
  dist_eq : ∀ x y, dist x y = ‖x - y‖ := by aesop

Normed Additive Commutative Group

Informal description

A normed additive commutative group is an additive commutative group $E$ endowed with a norm function $\|\cdot\| : E \to \mathbb{R}$ and a metric space structure, where the distance between two elements $x$ and $y$ is given by $\|x - y\|$.

NormedCommGroup structure

(E : Type*) extends Norm E, CommGroup E, MetricSpace E

Full source

/-- A normed group is a group endowed with a norm for which `dist x y = ‖x / y‖` defines a metric
space structure. -/
@[to_additive]
class NormedCommGroup (E : Type*) extends Norm E, CommGroup E, MetricSpace E where
  dist := fun x y => ‖x / y‖
  /-- The distance function is induced by the norm. -/
  dist_eq : ∀ x y, dist x y = ‖x / y‖ := by aesop

Normed commutative group

Informal description

A normed commutative group is a commutative group $E$ endowed with a norm function $\|\cdot\| \colon E \to \mathbb{R}$ and a metric space structure, where the distance between two elements $x$ and $y$ is given by $\|x / y\|$.

NormedGroup.toSeminormedGroup instance

[NormedGroup E] : SeminormedGroup E

Full source

@[to_additive]
instance (priority := 100) NormedGroup.toSeminormedGroup [NormedGroup E] : SeminormedGroup E :=
  { ‹NormedGroup E› with }

Normed Groups are Seminormed Groups

Informal description

Every normed group is a seminormed group.

NormedCommGroup.toSeminormedCommGroup instance

[NormedCommGroup E] : SeminormedCommGroup E

Full source

@[to_additive]
instance (priority := 100) NormedCommGroup.toSeminormedCommGroup [NormedCommGroup E] :
    SeminormedCommGroup E :=
  { ‹NormedCommGroup E› with }

Normed Commutative Groups are Seminormed Commutative Groups

Informal description

Every normed commutative group is a seminormed commutative group.

SeminormedCommGroup.toSeminormedGroup instance

[SeminormedCommGroup E] : SeminormedGroup E

Full source

@[to_additive]
instance (priority := 100) SeminormedCommGroup.toSeminormedGroup [SeminormedCommGroup E] :
    SeminormedGroup E :=
  { ‹SeminormedCommGroup E› with }

Seminormed Commutative Groups are Seminormed Groups

Informal description

Every seminormed commutative group is a seminormed group.

NormedCommGroup.toNormedGroup instance

[NormedCommGroup E] : NormedGroup E

Full source

@[to_additive]
instance (priority := 100) NormedCommGroup.toNormedGroup [NormedCommGroup E] : NormedGroup E :=
  { ‹NormedCommGroup E› with }

Normed Commutative Groups are Normed Groups

Informal description

Every normed commutative group is a normed group.

NormedGroup.ofSeparation abbrev

[SeminormedGroup E] (h : ∀ x : E, ‖x‖ = 0 → x = 1) : NormedGroup E

Full source

/-- Construct a `NormedGroup` from a `SeminormedGroup` satisfying `∀ x, ‖x‖ = 0 → x = 1`. This
avoids having to go back to the `(Pseudo)MetricSpace` level when declaring a `NormedGroup`
instance as a special case of a more general `SeminormedGroup` instance. -/
@[to_additive "Construct a `NormedAddGroup` from a `SeminormedAddGroup`
satisfying `∀ x, ‖x‖ = 0 → x = 0`. This avoids having to go back to the `(Pseudo)MetricSpace`
level when declaring a `NormedAddGroup` instance as a special case of a more general
`SeminormedAddGroup` instance."]
abbrev NormedGroup.ofSeparation [SeminormedGroup E] (h : ∀ x : E, ‖x‖ = 0 → x = 1) :
    NormedGroup E where
  dist_eq := ‹SeminormedGroup E›.dist_eq
  toMetricSpace :=
    { eq_of_dist_eq_zero := fun hxy =>
        div_eq_one.1 <| h _ <| (‹SeminormedGroup E›.dist_eq _ _).symm.trans hxy }

Construction of Normed Group from Seminormed Group with Separation Condition

Informal description

Given a seminormed group $E$ where the norm satisfies the separation condition $\forall x \in E, \|x\| = 0 \implies x = 1$, then $E$ can be endowed with the structure of a normed group.

NormedCommGroup.ofSeparation abbrev

[SeminormedCommGroup E] (h : ∀ x : E, ‖x‖ = 0 → x = 1) : NormedCommGroup E

Full source

/-- Construct a `NormedCommGroup` from a `SeminormedCommGroup` satisfying
`∀ x, ‖x‖ = 0 → x = 1`. This avoids having to go back to the `(Pseudo)MetricSpace` level when
declaring a `NormedCommGroup` instance as a special case of a more general `SeminormedCommGroup`
instance. -/
@[to_additive "Construct a `NormedAddCommGroup` from a
`SeminormedAddCommGroup` satisfying `∀ x, ‖x‖ = 0 → x = 0`. This avoids having to go back to the
`(Pseudo)MetricSpace` level when declaring a `NormedAddCommGroup` instance as a special case
of a more general `SeminormedAddCommGroup` instance."]
abbrev NormedCommGroup.ofSeparation [SeminormedCommGroup E] (h : ∀ x : E, ‖x‖ = 0 → x = 1) :
    NormedCommGroup E :=
  { ‹SeminormedCommGroup E›, NormedGroup.ofSeparation h with }

Construction of Normed Commutative Group from Seminormed Commutative Group with Separation Condition

Informal description

Given a seminormed commutative group $E$ where the norm satisfies the separation condition $\forall x \in E, \|x\| = 0 \implies x = 1$, then $E$ can be endowed with the structure of a normed commutative group.

SeminormedGroup.ofMulDist abbrev

 [Norm E] [Group E] [PseudoMetricSpace E] (h₁ : ∀ x : E, ‖x‖ = dist x 1)
  (h₂ : ∀ x y z : E, dist x y ≤ dist (x * z) (y * z)) : SeminormedGroup E

Full source

/-- Construct a seminormed group from a multiplication-invariant distance. -/
@[to_additive
  "Construct a seminormed group from a translation-invariant distance."]
abbrev SeminormedGroup.ofMulDist [Norm E] [Group E] [PseudoMetricSpace E]
    (h₁ : ∀ x : E, ‖x‖ = dist x 1) (h₂ : ∀ x y z : E, dist x y ≤ dist (x * z) (y * z)) :
    SeminormedGroup E where
  dist_eq x y := by
    rw [h₁]; apply le_antisymm
    · simpa only [div_eq_mul_inv, ← mul_inv_cancel y] using h₂ _ _ _
    · simpa only [div_mul_cancel, one_mul] using h₂ (x / y) 1 y

Construction of Seminormed Group from Multiplication-Invariant Distance

Informal description

Given a group $E$ equipped with a norm function $\|\cdot\| : E \to \mathbb{R}$ and a pseudometric space structure, if the following conditions hold: 1. For every $x \in E$, the norm of $x$ equals the distance from $x$ to the identity element, i.e., $\|x\| = \text{dist}(x, 1)$. 2. For every $x, y, z \in E$, the distance between $x$ and $y$ is less than or equal to the distance between $x \cdot z$ and $y \cdot z$, i.e., $\text{dist}(x, y) \leq \text{dist}(x \cdot z, y \cdot z)$. Then $E$ can be endowed with the structure of a seminormed group, where the distance is given by $\text{dist}(x, y) = \|x / y\|$.

SeminormedGroup.ofMulDist' abbrev

 [Norm E] [Group E] [PseudoMetricSpace E] (h₁ : ∀ x : E, ‖x‖ = dist x 1)
  (h₂ : ∀ x y z : E, dist (x * z) (y * z) ≤ dist x y) : SeminormedGroup E

Full source

/-- Construct a seminormed group from a multiplication-invariant pseudodistance. -/
@[to_additive
  "Construct a seminormed group from a translation-invariant pseudodistance."]
abbrev SeminormedGroup.ofMulDist' [Norm E] [Group E] [PseudoMetricSpace E]
    (h₁ : ∀ x : E, ‖x‖ = dist x 1) (h₂ : ∀ x y z : E, dist (x * z) (y * z) ≤ dist x y) :
    SeminormedGroup E where
  dist_eq x y := by
    rw [h₁]; apply le_antisymm
    · simpa only [div_mul_cancel, one_mul] using h₂ (x / y) 1 y
    · simpa only [div_eq_mul_inv, ← mul_inv_cancel y] using h₂ _ _ _

Construction of Seminormed Group from Right-Multiplication-Invariant Distance

Informal description

Given a group $E$ equipped with a norm function $\|\cdot\| : E \to \mathbb{R}$ and a pseudometric space structure, if the following conditions hold: 1. For every $x \in E$, the norm of $x$ equals the distance from $x$ to the identity element, i.e., $\|x\| = \text{dist}(x, 1)$. 2. For every $x, y, z \in E$, the distance between $x \cdot z$ and $y \cdot z$ is less than or equal to the distance between $x$ and $y$, i.e., $\text{dist}(x \cdot z, y \cdot z) \leq \text{dist}(x, y)$. Then $E$ can be endowed with the structure of a seminormed group, where the distance is given by $\text{dist}(x, y) = \|x / y\|$.

SeminormedCommGroup.ofMulDist abbrev

 [Norm E] [CommGroup E] [PseudoMetricSpace E] (h₁ : ∀ x : E, ‖x‖ = dist x 1)
  (h₂ : ∀ x y z : E, dist x y ≤ dist (x * z) (y * z)) : SeminormedCommGroup E

Full source

/-- Construct a seminormed group from a multiplication-invariant pseudodistance. -/
@[to_additive
  "Construct a seminormed group from a translation-invariant pseudodistance."]
abbrev SeminormedCommGroup.ofMulDist [Norm E] [CommGroup E] [PseudoMetricSpace E]
    (h₁ : ∀ x : E, ‖x‖ = dist x 1) (h₂ : ∀ x y z : E, dist x y ≤ dist (x * z) (y * z)) :
    SeminormedCommGroup E :=
  { SeminormedGroup.ofMulDist h₁ h₂ with
    mul_comm := mul_comm }

Construction of Seminormed Commutative Group from Multiplication-Invariant Distance

Informal description

Given a commutative group $E$ equipped with a norm function $\|\cdot\| : E \to \mathbb{R}$ and a pseudometric space structure, if the following conditions hold: 1. For every $x \in E$, the norm of $x$ equals the distance from $x$ to the identity element, i.e., $\|x\| = \text{dist}(x, 1)$. 2. For every $x, y, z \in E$, the distance between $x$ and $y$ is less than or equal to the distance between $x \cdot z$ and $y \cdot z$, i.e., $\text{dist}(x, y) \leq \text{dist}(x \cdot z, y \cdot z)$. Then $E$ can be endowed with the structure of a seminormed commutative group, where the distance is given by $\text{dist}(x, y) = \|x / y\|$.

SeminormedCommGroup.ofMulDist' abbrev

 [Norm E] [CommGroup E] [PseudoMetricSpace E] (h₁ : ∀ x : E, ‖x‖ = dist x 1)
  (h₂ : ∀ x y z : E, dist (x * z) (y * z) ≤ dist x y) : SeminormedCommGroup E

Full source

/-- Construct a seminormed group from a multiplication-invariant pseudodistance. -/
@[to_additive
  "Construct a seminormed group from a translation-invariant pseudodistance."]
abbrev SeminormedCommGroup.ofMulDist' [Norm E] [CommGroup E] [PseudoMetricSpace E]
    (h₁ : ∀ x : E, ‖x‖ = dist x 1) (h₂ : ∀ x y z : E, dist (x * z) (y * z) ≤ dist x y) :
    SeminormedCommGroup E :=
  { SeminormedGroup.ofMulDist' h₁ h₂ with
    mul_comm := mul_comm }

Construction of Seminormed Commutative Group from Right-Multiplication-Invariant Distance

Informal description

Given a commutative group $E$ equipped with a norm function $\|\cdot\| : E \to \mathbb{R}$ and a pseudometric space structure, if the following conditions hold: 1. For every $x \in E$, the norm of $x$ equals the distance from $x$ to the identity element, i.e., $\|x\| = \text{dist}(x, 1)$. 2. For every $x, y, z \in E$, the distance between $x \cdot z$ and $y \cdot z$ is less than or equal to the distance between $x$ and $y$, i.e., $\text{dist}(x \cdot z, y \cdot z) \leq \text{dist}(x, y)$. Then $E$ can be endowed with the structure of a seminormed commutative group, where the distance is given by $\text{dist}(x, y) = \|x / y\|$.

NormedGroup.ofMulDist abbrev

 [Norm E] [Group E] [MetricSpace E] (h₁ : ∀ x : E, ‖x‖ = dist x 1) (h₂ : ∀ x y z : E, dist x y ≤ dist (x * z) (y * z)) :
  NormedGroup E

Full source

/-- Construct a normed group from a multiplication-invariant distance. -/
@[to_additive
  "Construct a normed group from a translation-invariant distance."]
abbrev NormedGroup.ofMulDist [Norm E] [Group E] [MetricSpace E] (h₁ : ∀ x : E, ‖x‖ = dist x 1)
    (h₂ : ∀ x y z : E, dist x y ≤ dist (x * z) (y * z)) : NormedGroup E :=
  { SeminormedGroup.ofMulDist h₁ h₂ with
    eq_of_dist_eq_zero := eq_of_dist_eq_zero }

Construction of Normed Group from Multiplication-Invariant Distance

Informal description

Given a group $E$ equipped with a norm function $\|\cdot\| : E \to \mathbb{R}$ and a metric space structure, if the following conditions hold: 1. For every $x \in E$, the norm of $x$ equals the distance from $x$ to the identity element, i.e., $\|x\| = \text{dist}(x, 1)$. 2. For every $x, y, z \in E$, the distance between $x$ and $y$ is less than or equal to the distance between $x \cdot z$ and $y \cdot z$, i.e., $\text{dist}(x, y) \leq \text{dist}(x \cdot z, y \cdot z)$. Then $E$ can be endowed with the structure of a normed group, where the distance is given by $\text{dist}(x, y) = \|x / y\|$.

NormedGroup.ofMulDist' abbrev

 [Norm E] [Group E] [MetricSpace E] (h₁ : ∀ x : E, ‖x‖ = dist x 1) (h₂ : ∀ x y z : E, dist (x * z) (y * z) ≤ dist x y) :
  NormedGroup E

Full source

/-- Construct a normed group from a multiplication-invariant pseudodistance. -/
@[to_additive
  "Construct a normed group from a translation-invariant pseudodistance."]
abbrev NormedGroup.ofMulDist' [Norm E] [Group E] [MetricSpace E] (h₁ : ∀ x : E, ‖x‖ = dist x 1)
    (h₂ : ∀ x y z : E, dist (x * z) (y * z) ≤ dist x y) : NormedGroup E :=
  { SeminormedGroup.ofMulDist' h₁ h₂ with
    eq_of_dist_eq_zero := eq_of_dist_eq_zero }

Construction of Normed Group from Right-Multiplication-Invariant Distance

Informal description

Given a group $E$ equipped with a norm function $\|\cdot\| : E \to \mathbb{R}$ and a metric space structure, if the following conditions hold: 1. For every $x \in E$, the norm of $x$ equals the distance from $x$ to the identity element, i.e., $\|x\| = \text{dist}(x, 1)$. 2. For every $x, y, z \in E$, the distance between $x \cdot z$ and $y \cdot z$ is less than or equal to the distance between $x$ and $y$, i.e., $\text{dist}(x \cdot z, y \cdot z) \leq \text{dist}(x, y)$. Then $E$ can be endowed with the structure of a normed group, where the distance is given by $\text{dist}(x, y) = \|x / y\|$.

NormedCommGroup.ofMulDist abbrev

 [Norm E] [CommGroup E] [MetricSpace E] (h₁ : ∀ x : E, ‖x‖ = dist x 1)
  (h₂ : ∀ x y z : E, dist x y ≤ dist (x * z) (y * z)) : NormedCommGroup E

Full source

/-- Construct a normed group from a multiplication-invariant pseudodistance. -/
@[to_additive
"Construct a normed group from a translation-invariant pseudodistance."]
abbrev NormedCommGroup.ofMulDist [Norm E] [CommGroup E] [MetricSpace E]
    (h₁ : ∀ x : E, ‖x‖ = dist x 1) (h₂ : ∀ x y z : E, dist x y ≤ dist (x * z) (y * z)) :
    NormedCommGroup E :=
  { NormedGroup.ofMulDist h₁ h₂ with
    mul_comm := mul_comm }

Construction of Normed Commutative Group from Multiplication-Invariant Distance

Informal description

Let $E$ be a commutative group equipped with a norm function $\|\cdot\| \colon E \to \mathbb{R}$ and a metric space structure. Suppose the following conditions hold: 1. For every $x \in E$, the norm of $x$ equals the distance from $x$ to the identity element, i.e., $\|x\| = \text{dist}(x, 1)$. 2. For every $x, y, z \in E$, the distance between $x$ and $y$ is less than or equal to the distance between $x \cdot z$ and $y \cdot z$, i.e., $\text{dist}(x, y) \leq \text{dist}(x \cdot z, y \cdot z)$. Then $E$ can be endowed with the structure of a normed commutative group, where the distance is given by $\text{dist}(x, y) = \|x / y\|$.

NormedCommGroup.ofMulDist' abbrev

 [Norm E] [CommGroup E] [MetricSpace E] (h₁ : ∀ x : E, ‖x‖ = dist x 1)
  (h₂ : ∀ x y z : E, dist (x * z) (y * z) ≤ dist x y) : NormedCommGroup E

Full source

/-- Construct a normed group from a multiplication-invariant pseudodistance. -/
@[to_additive
  "Construct a normed group from a translation-invariant pseudodistance."]
abbrev NormedCommGroup.ofMulDist' [Norm E] [CommGroup E] [MetricSpace E]
    (h₁ : ∀ x : E, ‖x‖ = dist x 1) (h₂ : ∀ x y z : E, dist (x * z) (y * z) ≤ dist x y) :
    NormedCommGroup E :=
  { NormedGroup.ofMulDist' h₁ h₂ with
    mul_comm := mul_comm }

Construction of Normed Commutative Group from Right-Multiplication-Invariant Distance

Informal description

Given a commutative group $E$ equipped with a norm function $\|\cdot\| \colon E \to \mathbb{R}$ and a metric space structure, if the following conditions hold: 1. For every $x \in E$, the norm of $x$ equals the distance from $x$ to the identity element, i.e., $\|x\| = \text{dist}(x, 1)$. 2. For every $x, y, z \in E$, the distance between $x \cdot z$ and $y \cdot z$ is less than or equal to the distance between $x$ and $y$, i.e., $\text{dist}(x \cdot z, y \cdot z) \leq \text{dist}(x, y)$. Then $E$ can be endowed with the structure of a normed commutative group, where the distance is given by $\text{dist}(x, y) = \|x / y\|$.

GroupSeminorm.toSeminormedGroup abbrev

[Group E] (f : GroupSeminorm E) : SeminormedGroup E

Full source

/-- Construct a seminormed group from a seminorm, i.e., registering the pseudodistance and the
pseudometric space structure from the seminorm properties. Note that in most cases this instance
creates bad definitional equalities (e.g., it does not take into account a possibly existing
`UniformSpace` instance on `E`). -/
@[to_additive
  "Construct a seminormed group from a seminorm, i.e., registering the pseudodistance
and the pseudometric space structure from the seminorm properties. Note that in most cases this
instance creates bad definitional equalities (e.g., it does not take into account a possibly
existing `UniformSpace` instance on `E`)."]
abbrev GroupSeminorm.toSeminormedGroup [Group E] (f : GroupSeminorm E) : SeminormedGroup E where
  dist x y := f (x / y)
  norm := f
  dist_eq _ _ := rfl
  dist_self x := by simp only [div_self', map_one_eq_zero]
  dist_triangle := le_map_div_add_map_div f
  dist_comm := map_div_rev f

-- See note [reducible non-instances]

Construction of Seminormed Group from Group Seminorm

Informal description

Given a group $E$ and a group seminorm $f \colon E \to \mathbb{R}$, the function `GroupSeminorm.toSeminormedGroup` constructs a seminormed group structure on $E$ where the norm is given by $f$ and the pseudometric is defined by $\text{dist}(x, y) = f(x / y)$ for all $x, y \in E$.

GroupSeminorm.toSeminormedCommGroup abbrev

[CommGroup E] (f : GroupSeminorm E) : SeminormedCommGroup E

Full source

/-- Construct a seminormed group from a seminorm, i.e., registering the pseudodistance and the
pseudometric space structure from the seminorm properties. Note that in most cases this instance
creates bad definitional equalities (e.g., it does not take into account a possibly existing
`UniformSpace` instance on `E`). -/
@[to_additive
  "Construct a seminormed group from a seminorm, i.e., registering the pseudodistance
and the pseudometric space structure from the seminorm properties. Note that in most cases this
instance creates bad definitional equalities (e.g., it does not take into account a possibly
existing `UniformSpace` instance on `E`)."]
abbrev GroupSeminorm.toSeminormedCommGroup [CommGroup E] (f : GroupSeminorm E) :
    SeminormedCommGroup E :=
  { f.toSeminormedGroup with
    mul_comm := mul_comm }

Construction of Seminormed Commutative Group from Group Seminorm

Informal description

Given a commutative group $E$ and a group seminorm $f \colon E \to \mathbb{R}$, the function `GroupSeminorm.toSeminormedCommGroup` constructs a seminormed commutative group structure on $E$ where the norm is given by $f$ and the pseudometric is defined by $\text{dist}(x, y) = \|x / y\|$ for all $x, y \in E$.

GroupNorm.toNormedGroup abbrev

[Group E] (f : GroupNorm E) : NormedGroup E

Full source

/-- Construct a normed group from a norm, i.e., registering the distance and the metric space
structure from the norm properties. Note that in most cases this instance creates bad definitional
equalities (e.g., it does not take into account a possibly existing `UniformSpace` instance on
`E`). -/
@[to_additive
  "Construct a normed group from a norm, i.e., registering the distance and the metric
space structure from the norm properties. Note that in most cases this instance creates bad
definitional equalities (e.g., it does not take into account a possibly existing `UniformSpace`
instance on `E`)."]
abbrev GroupNorm.toNormedGroup [Group E] (f : GroupNorm E) : NormedGroup E :=
  { f.toGroupSeminorm.toSeminormedGroup with
    eq_of_dist_eq_zero := fun h => div_eq_one.1 <| eq_one_of_map_eq_zero f h }

Construction of Normed Group from Group Norm

Informal description

Given a group $E$ and a group norm $f \colon E \to \mathbb{R}$, the function `GroupNorm.toNormedGroup` constructs a normed group structure on $E$ where the norm is given by $f$ and the metric is defined by $\text{dist}(x, y) = \|x / y\|$ for all $x, y \in E$.

GroupNorm.toNormedCommGroup abbrev

[CommGroup E] (f : GroupNorm E) : NormedCommGroup E

Full source

/-- Construct a normed group from a norm, i.e., registering the distance and the metric space
structure from the norm properties. Note that in most cases this instance creates bad definitional
equalities (e.g., it does not take into account a possibly existing `UniformSpace` instance on
`E`). -/
@[to_additive
  "Construct a normed group from a norm, i.e., registering the distance and the metric
space structure from the norm properties. Note that in most cases this instance creates bad
definitional equalities (e.g., it does not take into account a possibly existing `UniformSpace`
instance on `E`)."]
abbrev GroupNorm.toNormedCommGroup [CommGroup E] (f : GroupNorm E) : NormedCommGroup E :=
  { f.toNormedGroup with
    mul_comm := mul_comm }

Construction of Normed Commutative Group from Group Norm

Informal description

Given a commutative group $E$ and a group norm $f \colon E \to \mathbb{R}$, the function `GroupNorm.toNormedCommGroup` constructs a normed commutative group structure on $E$ where the norm is given by $f$ and the metric is defined by $\text{dist}(x, y) = \|x / y\|$ for all $x, y \in E$.

dist_eq_norm_div theorem

(a b : E) : dist a b = ‖a / b‖

Full source

@[to_additive]
theorem dist_eq_norm_div (a b : E) : dist a b = ‖a / b‖ :=
  SeminormedGroup.dist_eq _ _

Distance as Norm of Quotient in Seminormed Groups

Informal description

For any elements $a$ and $b$ in a seminormed group $E$, the distance between $a$ and $b$ is equal to the norm of their quotient, i.e., $\text{dist}(a, b) = \|a / b\|$.

dist_eq_norm_div' theorem

(a b : E) : dist a b = ‖b / a‖

Full source

@[to_additive]
theorem dist_eq_norm_div' (a b : E) : dist a b = ‖b / a‖ := by rw [dist_comm, dist_eq_norm_div]

Distance as Norm of Reverse Quotient in Seminormed Groups

Informal description

For any elements $a$ and $b$ in a seminormed group $E$, the distance between $a$ and $b$ is equal to the norm of the quotient $b / a$, i.e., $\text{dist}(a, b) = \|b / a\|$.

DiscreteTopology.of_forall_le_norm' theorem

(hpos : 0 < r) (hr : ∀ x : E, x ≠ 1 → r ≤ ‖x‖) : DiscreteTopology E

Full source

@[to_additive of_forall_le_norm]
lemma DiscreteTopology.of_forall_le_norm' (hpos : 0 < r) (hr : ∀ x : E, x ≠ 1 → r ≤ ‖x‖) :
    DiscreteTopology E :=
  .of_forall_le_dist hpos fun x y hne ↦ by
    simp only [dist_eq_norm_div]
    exact hr _ (div_ne_one.2 hne)

Discrete topology criterion via uniform lower bound on non-identity norms: $\forall x \neq 1, \|x\| \geq r > 0 \Rightarrow \text{DiscreteTopology } E$

Informal description

Let $E$ be a seminormed group. If there exists a positive real number $r > 0$ such that for every non-identity element $x \in E$ the norm satisfies $\|x\| \geq r$, then $E$ has the discrete topology (i.e., every subset of $E$ is open).

dist_one_right theorem

(a : E) : dist a 1 = ‖a‖

Full source

@[to_additive (attr := simp)]
theorem dist_one_right (a : E) : dist a 1 = ‖a‖ := by rw [dist_eq_norm_div, div_one]

Distance to Identity Equals Norm in Seminormed Groups

Informal description

For any element $a$ in a seminormed group $E$, the distance between $a$ and the identity element $1$ is equal to the norm of $a$, i.e., $\text{dist}(a, 1) = \|a\|$.

inseparable_one_iff_norm theorem

{a : E} : Inseparable a 1 ↔ ‖a‖ = 0

Full source

@[to_additive]
theorem inseparable_one_iff_norm {a : E} : InseparableInseparable a 1 ↔ ‖a‖ = 0 := by
  rw [Metric.inseparable_iff, dist_one_right]

Topological Inseparability of Element and Identity Characterized by Norm Vanishing

Informal description

For any element $a$ in a seminormed group $E$, the points $a$ and the identity element $1$ are topologically inseparable if and only if the norm of $a$ is zero, i.e., $\|a\| = 0$.

dist_one_left theorem

(a : E) : dist 1 a = ‖a‖

Full source

@[to_additive]
lemma dist_one_left (a : E) : dist 1 a = ‖a‖ := by rw [dist_comm, dist_one_right]

Distance from Identity Equals Norm in Seminormed Groups

Informal description

For any element $a$ in a seminormed group $E$, the distance between the identity element $1$ and $a$ is equal to the norm of $a$, i.e., $\text{dist}(1, a) = \|a\|$.

dist_one theorem

: dist (1 : E) = norm

Full source

@[to_additive (attr := simp)]
lemma dist_one : dist (1 : E) = norm := funext dist_one_left

Distance from Identity Equals Norm in Seminormed Groups

Informal description

In a seminormed group $E$, the distance function from the identity element $1$ is equal to the norm function, i.e., $\text{dist}(1, \cdot) = \|\cdot\|$.

norm_div_rev theorem

(a b : E) : ‖a / b‖ = ‖b / a‖

Full source

@[to_additive]
theorem norm_div_rev (a b : E) : ‖a / b‖ = ‖b / a‖ := by
  simpa only [dist_eq_norm_div] using dist_comm a b

Norm of Quotient is Symmetric: $\|a / b\| = \|b / a\|$

Informal description

For any elements $a$ and $b$ in a seminormed group $E$, the norm of the quotient $a / b$ is equal to the norm of the quotient $b / a$, i.e., $\|a / b\| = \|b / a\|$.

norm_inv' theorem

(a : E) : ‖a⁻¹‖ = ‖a‖

Full source

@[to_additive (attr := simp) norm_neg]
theorem norm_inv' (a : E) : ‖a⁻¹‖ = ‖a‖ := by simpa using norm_div_rev 1 a

Norm of Inverse Equals Norm: $\|a^{-1}\| = \|a\|$

Informal description

For any element $a$ in a seminormed group $E$, the norm of the inverse $a^{-1}$ is equal to the norm of $a$, i.e., $\|a^{-1}\| = \|a\|$.

norm_zpow_abs theorem

(a : E) (n : ℤ) : ‖a ^ |n|‖ = ‖a ^ n‖

Full source

@[to_additive (attr := simp) norm_abs_zsmul]
theorem norm_zpow_abs (a : E) (n : ℤ) : ‖a ^ |n|‖ = ‖a ^ n‖ := by
  rcases le_total 0 n with hn | hn <;> simp [hn, abs_of_nonneg, abs_of_nonpos]

Norm of Power with Absolute Exponent: $\|a^{|n|}\| = \|a^n\|$

Informal description

For any element $a$ in a seminormed group $E$ and any integer $n$, the norm of $a$ raised to the absolute value of $n$ is equal to the norm of $a$ raised to $n$, i.e., $\|a^{|n|}\| = \|a^n\|$.

norm_pow_natAbs theorem

(a : E) (n : ℤ) : ‖a ^ n.natAbs‖ = ‖a ^ n‖

Full source

@[to_additive (attr := simp) norm_natAbs_smul]
theorem norm_pow_natAbs (a : E) (n : ℤ) : ‖a ^ n.natAbs‖ = ‖a ^ n‖ := by
  rw [← zpow_natCast, ← Int.abs_eq_natAbs, norm_zpow_abs]

Norm of Power with Natural Absolute Value Exponent: $\|a^{\text{natAbs}(n)}\| = \|a^n\|$

Informal description

For any element $a$ in a seminormed group $E$ and any integer $n$, the norm of $a$ raised to the natural number absolute value of $n$ is equal to the norm of $a$ raised to $n$, i.e., $\|a^{\text{natAbs}(n)}\| = \|a^n\|$.

norm_zpow_isUnit theorem

(a : E) {n : ℤ} (hn : IsUnit n) : ‖a ^ n‖ = ‖a‖

Full source

@[to_additive norm_isUnit_zsmul]
theorem norm_zpow_isUnit (a : E) {n : ℤ} (hn : IsUnit n) : ‖a ^ n‖ = ‖a‖ := by
  rw [← norm_pow_natAbs, Int.isUnit_iff_natAbs_eq.mp hn, pow_one]

Norm Preservation under Unit Integer Exponentiation: $\|a^n\| = \|a\|$ for $n = \pm 1$

Informal description

For any element $a$ in a seminormed group $E$ and any integer $n$ that is a unit (i.e., $n = \pm 1$), the norm of $a$ raised to the power $n$ is equal to the norm of $a$, i.e., $\|a^n\| = \|a\|$.

norm_units_zsmul theorem

{E : Type*} [SeminormedAddGroup E] (n : ℤˣ) (a : E) : ‖n • a‖ = ‖a‖

Full source

@[simp]
theorem norm_units_zsmul {E : Type*} [SeminormedAddGroup E] (n : ℤℤˣ) (a : E) : ‖n • a‖ = ‖a‖ :=
  norm_isUnit_zsmul a n.isUnit

Norm Preservation under Scalar Multiplication by Unit Integers: $\|n \cdot a\| = \|a\|$ for $n \in \mathbb{Z}^\times$

Informal description

For any seminormed additive group $E$, any unit integer $n \in \mathbb{Z}^\times$, and any element $a \in E$, the norm of the scalar multiple $n \cdot a$ is equal to the norm of $a$, i.e., $\|n \cdot a\| = \|a\|$.

dist_mulIndicator theorem

 (s t : Set α) (f : α → E) (x : α) : dist (s.mulIndicator f x) (t.mulIndicator f x) = ‖(s ∆ t).mulIndicator f x‖

Full source

@[to_additive]
theorem dist_mulIndicator (s t : Set α) (f : α → E) (x : α) :
    dist (s.mulIndicator f x) (t.mulIndicator f x) = ‖(s ∆ t).mulIndicator f x‖ := by
  rw [dist_eq_norm_div, Set.apply_mulIndicator_symmDiff norm_inv']

Distance Between Multiplicative Indicators Equals Norm on Symmetric Difference: $\text{dist}(\text{mulIndicator}_s f, \text{mulIndicator}_t f) = \|\text{mulIndicator}_{s \Delta t} f\|$

Informal description

For any two sets $s, t \subseteq \alpha$, any function $f \colon \alpha \to E$ into a seminormed group $E$, and any element $x \in \alpha$, the distance between the multiplicative indicators of $f$ on $s$ and $t$ at $x$ is equal to the norm of the multiplicative indicator of $f$ on the symmetric difference $s \Delta t$ at $x$. That is, \[ \text{dist}\big(\text{mulIndicator}_s f(x), \text{mulIndicator}_t f(x)\big) = \|\text{mulIndicator}_{s \Delta t} f(x)\|, \] where $\text{mulIndicator}_s f(x) = f(x)$ if $x \in s$ and $1$ otherwise, and $s \Delta t = (s \setminus t) \cup (t \setminus s)$ is the symmetric difference of $s$ and $t$.

norm_mul_le' theorem

(a b : E) : ‖a * b‖ ≤ ‖a‖ + ‖b‖

Full source

/-- **Triangle inequality** for the norm. -/
@[to_additive norm_add_le "**Triangle inequality** for the norm."]
theorem norm_mul_le' (a b : E) : ‖a * b‖ ≤ ‖a‖ + ‖b‖ := by
  simpa [dist_eq_norm_div] using dist_triangle a 1 b⁻¹

Triangle Inequality for Norm of Product: $\|a \cdot b\| \leq \|a\| + \|b\|$

Informal description

For any two elements $a$ and $b$ in a seminormed group $E$, the norm of their product satisfies the inequality $\|a \cdot b\| \leq \|a\| + \|b\|$.

norm_mul_le_of_le' theorem

(h₁ : ‖a₁‖ ≤ r₁) (h₂ : ‖a₂‖ ≤ r₂) : ‖a₁ * a₂‖ ≤ r₁ + r₂

Full source

/-- **Triangle inequality** for the norm. -/
@[to_additive norm_add_le_of_le "**Triangle inequality** for the norm."]
theorem norm_mul_le_of_le' (h₁ : ‖a₁‖ ≤ r₁) (h₂ : ‖a₂‖ ≤ r₂) : ‖a₁ * a₂‖ ≤ r₁ + r₂ :=
  (norm_mul_le' a₁ a₂).trans <| add_le_add h₁ h₂

Norm of Product Bounded by Sum of Bounds: $\|a_1 \cdot a_2\| \leq r_1 + r_2$

Informal description

norm_mul₃_le' theorem

: ‖a * b * c‖ ≤ ‖a‖ + ‖b‖ + ‖c‖

Full source

/-- **Triangle inequality** for the norm. -/
@[to_additive norm_add₃_le "**Triangle inequality** for the norm."]
lemma norm_mul₃_le' : ‖a * b * c‖ ≤ ‖a‖ + ‖b‖ + ‖c‖ := norm_mul_le_of_le' (norm_mul_le' _ _) le_rfl

Triangle Inequality for Norm of Triple Product: $\|a \cdot b \cdot c\| \leq \|a\| + \|b\| + \|c\|$

Informal description

For any three elements $a$, $b$, and $c$ in a seminormed group $E$, the norm of their product satisfies the inequality $\|a \cdot b \cdot c\| \leq \|a\| + \|b\| + \|c\|$.

norm_div_le_norm_div_add_norm_div theorem

(a b c : E) : ‖a / c‖ ≤ ‖a / b‖ + ‖b / c‖

Full source

@[to_additive]
lemma norm_div_le_norm_div_add_norm_div (a b c : E) : ‖a / c‖ ≤ ‖a / b‖ + ‖b / c‖ := by
  simpa only [dist_eq_norm_div] using dist_triangle a b c

Triangle Inequality for Norm of Quotients in Seminormed Groups

Informal description

For any elements $a$, $b$, and $c$ in a seminormed group $E$, the norm of the quotient $a / c$ satisfies the inequality $\|a / c\| \leq \|a / b\| + \|b / c\|$.

norm_nonneg' theorem

(a : E) : 0 ≤ ‖a‖

Full source

@[to_additive (attr := simp) norm_nonneg]
theorem norm_nonneg' (a : E) : 0 ≤ ‖a‖ := by
  rw [← dist_one_right]
  exact dist_nonneg

Nonnegativity of Norm in Seminormed Groups

Informal description

For any element $a$ in a seminormed group $E$, the norm of $a$ is nonnegative, i.e., $\|a\| \geq 0$.

abs_norm' theorem

(z : E) : |‖z‖| = ‖z‖

Full source

@[to_additive (attr := simp) abs_norm]
theorem abs_norm' (z : E) : |‖z‖| = ‖z‖ := abs_of_nonneg <| norm_nonneg' _

Absolute Value of Norm Equals Norm in Seminormed Groups

Informal description

For any element $z$ in a seminormed group $E$, the absolute value of the norm of $z$ is equal to the norm of $z$, i.e., $|\|z\|| = \|z\|$.

norm_one' theorem

: ‖(1 : E)‖ = 0

Full source

@[to_additive (attr := simp) norm_zero]
theorem norm_one' : ‖(1 : E)‖ = 0 := by rw [← dist_one_right, dist_self]

Norm of Identity is Zero in Seminormed Groups

Informal description

In a seminormed group $E$, the norm of the identity element $1$ is zero, i.e., $\|1\| = 0$.

ne_one_of_norm_ne_zero theorem

: ‖a‖ ≠ 0 → a ≠ 1

Full source

@[to_additive]
theorem ne_one_of_norm_ne_zero : ‖a‖‖a‖ ≠ 0 → a ≠ 1 :=
  mt <| by
    rintro rfl
    exact norm_one'

Non-identity Element Has Nonzero Norm in Seminormed Groups

Informal description

For any element $a$ in a seminormed group $E$, if the norm of $a$ is nonzero, then $a$ is not the identity element, i.e., $\|a\| \neq 0$ implies $a \neq 1$.

norm_of_subsingleton' theorem

[Subsingleton E] (a : E) : ‖a‖ = 0

Full source

@[to_additive (attr := nontriviality) norm_of_subsingleton]
theorem norm_of_subsingleton' [Subsingleton E] (a : E) : ‖a‖ = 0 := by
  rw [Subsingleton.elim a 1, norm_one']

Norm Vanishes on Subsingleton Seminormed Groups

Informal description

For any subsingleton seminormed group $E$ (i.e., a group with at most one element) and any element $a \in E$, the norm of $a$ is zero, i.e., $\|a\| = 0$.

zero_lt_one_add_norm_sq' theorem

(x : E) : 0 < 1 + ‖x‖ ^ 2

Full source

@[to_additive zero_lt_one_add_norm_sq]
theorem zero_lt_one_add_norm_sq' (x : E) : 0 < 1 + ‖x‖ ^ 2 := by
  positivity

Positivity of $1 + \|x\|^2$ in Seminormed Groups

Informal description

For any element $x$ in a seminormed group $E$, the expression $1 + \|x\|^2$ is strictly positive, i.e., $0 < 1 + \|x\|^2$.

norm_div_le theorem

(a b : E) : ‖a / b‖ ≤ ‖a‖ + ‖b‖

Full source

@[to_additive]
theorem norm_div_le (a b : E) : ‖a / b‖ ≤ ‖a‖ + ‖b‖ := by
  simpa [dist_eq_norm_div] using dist_triangle a 1 b

Norm of Quotient Bounded by Sum of Norms

Informal description

For any elements $a$ and $b$ in a seminormed group $E$, the norm of their quotient satisfies the inequality $\|a / b\| \leq \|a\| + \|b\|$.

norm_div_le_of_le theorem

{r₁ r₂ : ℝ} (H₁ : ‖a₁‖ ≤ r₁) (H₂ : ‖a₂‖ ≤ r₂) : ‖a₁ / a₂‖ ≤ r₁ + r₂

Full source

@[to_additive]
theorem norm_div_le_of_le {r₁ r₂ : ℝ} (H₁ : ‖a₁‖ ≤ r₁) (H₂ : ‖a₂‖ ≤ r₂) : ‖a₁ / a₂‖ ≤ r₁ + r₂ :=
  (norm_div_le a₁ a₂).trans <| add_le_add H₁ H₂

Norm of Quotient Bounded by Sum of Norm Bounds

Informal description

For any elements $a_1$ and $a_2$ in a seminormed group $E$, if $\|a_1\| \leq r_1$ and $\|a_2\| \leq r_2$ for some real numbers $r_1, r_2 \in \mathbb{R}$, then the norm of their quotient satisfies $\|a_1 / a_2\| \leq r_1 + r_2$.

dist_le_norm_add_norm' theorem

(a b : E) : dist a b ≤ ‖a‖ + ‖b‖

Full source

@[to_additive dist_le_norm_add_norm]
theorem dist_le_norm_add_norm' (a b : E) : dist a b ≤ ‖a‖ + ‖b‖ := by
  rw [dist_eq_norm_div]
  apply norm_div_le

Distance Bounded by Sum of Norms in Seminormed Groups

Informal description

For any elements $a$ and $b$ in a seminormed group $E$, the distance between $a$ and $b$ is bounded by the sum of their norms, i.e., $\text{dist}(a, b) \leq \|a\| + \|b\|$.

abs_norm_sub_norm_le' theorem

(a b : E) : |‖a‖ - ‖b‖| ≤ ‖a / b‖

Full source

@[to_additive abs_norm_sub_norm_le]
theorem abs_norm_sub_norm_le' (a b : E) : |‖a‖ - ‖b‖| ≤ ‖a / b‖ := by
  simpa [dist_eq_norm_div] using abs_dist_sub_le a b 1

Absolute Difference of Norms Bounded by Quotient Norm in Seminormed Groups

Informal description

For any elements $a$ and $b$ in a seminormed group $E$, the absolute difference between their norms is bounded by the norm of their quotient, i.e., \[ \big| \|a\| - \|b\| \big| \leq \|a / b\|. \]

norm_sub_norm_le' theorem

(a b : E) : ‖a‖ - ‖b‖ ≤ ‖a / b‖

Full source

@[to_additive norm_sub_norm_le]
theorem norm_sub_norm_le' (a b : E) : ‖a‖ - ‖b‖ ≤ ‖a / b‖ :=
  (le_abs_self _).trans (abs_norm_sub_norm_le' a b)

Difference of Norms Bounded by Quotient Norm in Seminormed Groups

Informal description

For any elements $a$ and $b$ in a seminormed group $E$, the difference of their norms is bounded by the norm of their quotient, i.e., \[ \|a\| - \|b\| \leq \|a / b\|. \]

norm_sub_le_norm_mul theorem

(a b : E) : ‖a‖ - ‖b‖ ≤ ‖a * b‖

Full source

@[to_additive (attr := bound)]
theorem norm_sub_le_norm_mul (a b : E) : ‖a‖ - ‖b‖ ≤ ‖a * b‖ := by
  simpa using norm_mul_le' (a * b) (b⁻¹)

Difference of Norms Bounded by Product Norm in Seminormed Groups

Informal description

For any elements $a$ and $b$ in a seminormed group $E$, the difference of their norms is bounded by the norm of their product, i.e., \[ \|a\| - \|b\| \leq \|a \cdot b\|. \]

dist_norm_norm_le' theorem

(a b : E) : dist ‖a‖ ‖b‖ ≤ ‖a / b‖

Full source

@[to_additive dist_norm_norm_le]
theorem dist_norm_norm_le' (a b : E) : dist ‖a‖ ‖b‖ ≤ ‖a / b‖ :=
  abs_norm_sub_norm_le' a b

Distance Between Norms Bounded by Quotient Norm in Seminormed Groups

Informal description

For any elements $a$ and $b$ in a seminormed group $E$, the distance between their norms is bounded by the norm of their quotient, i.e., \[ \text{dist}(\|a\|, \|b\|) \leq \|a / b\|. \]

norm_le_norm_add_norm_div' theorem

(u v : E) : ‖u‖ ≤ ‖v‖ + ‖u / v‖

Full source

@[to_additive]
theorem norm_le_norm_add_norm_div' (u v : E) : ‖u‖ ≤ ‖v‖ + ‖u / v‖ := by
  rw [add_comm]
  refine (norm_mul_le' _ _).trans_eq' ?_
  rw [div_mul_cancel]

Norm Inequality: $\|u\| \leq \|v\| + \|u / v\|$ in Seminormed Groups

Informal description

For any elements $u$ and $v$ in a seminormed group $E$, the norm of $u$ satisfies the inequality $\|u\| \leq \|v\| + \|u / v\|$.

norm_le_norm_add_norm_div theorem

(u v : E) : ‖v‖ ≤ ‖u‖ + ‖u / v‖

Full source

@[to_additive]
theorem norm_le_norm_add_norm_div (u v : E) : ‖v‖ ≤ ‖u‖ + ‖u / v‖ := by
  rw [norm_div_rev]
  exact norm_le_norm_add_norm_div' v u

Norm Inequality: $\|v\| \leq \|u\| + \|u / v\|$ in Seminormed Groups

Informal description

For any elements $u$ and $v$ in a seminormed group $E$, the norm of $v$ satisfies the inequality $\|v\| \leq \|u\| + \|u / v\|$.

norm_le_mul_norm_add theorem

(u v : E) : ‖u‖ ≤ ‖u * v‖ + ‖v‖

Full source

@[to_additive]
theorem norm_le_mul_norm_add (u v : E) : ‖u‖ ≤ ‖u * v‖ + ‖v‖ :=
  calc
    ‖u‖ = ‖u * v / v‖ := by rw [mul_div_cancel_right]
    _ ≤ ‖u * v‖ + ‖v‖ := norm_div_le _ _

Norm Inequality: $\|u\| \leq \|u \cdot v\| + \|v\|$ in Seminormed Groups

Informal description

For any elements $u$ and $v$ in a seminormed group $E$, the norm of $u$ satisfies the inequality $\|u\| \leq \|u \cdot v\| + \|v\|$.

norm_le_mul_norm_add' theorem

(u v : E) : ‖v‖ ≤ ‖u * v‖ + ‖u‖

Full source

/-- An analogue of `norm_le_mul_norm_add` for the multiplication from the left. -/
@[to_additive "An analogue of `norm_le_add_norm_add` for the addition from the left."]
theorem norm_le_mul_norm_add' (u v : E) : ‖v‖ ≤ ‖u * v‖ + ‖u‖ :=
  calc
    ‖v‖ = ‖u⁻¹ * (u * v)‖ := by rw [← mul_assoc, inv_mul_cancel, one_mul]
    _ ≤ ‖u⁻¹‖ + ‖u * v‖ := norm_mul_le' u⁻¹ (u * v)
    _ = ‖u * v‖ + ‖u‖ := by rw [norm_inv', add_comm]

Norm Inequality: $\|v\| \leq \|u \cdot v\| + \|u\|$ in Seminormed Groups

Informal description

For any elements $u$ and $v$ in a seminormed group $E$, the norm of $v$ satisfies the inequality $\|v\| \leq \|u \cdot v\| + \|u\|$.

norm_mul_eq_norm_right theorem

{x : E} (y : E) (h : ‖x‖ = 0) : ‖x * y‖ = ‖y‖

Full source

@[to_additive]
lemma norm_mul_eq_norm_right {x : E} (y : E) (h : ‖x‖ = 0) : ‖x * y‖ = ‖y‖ := by
  apply le_antisymm ?_ ?_
  · simpa [h] using norm_mul_le' x y
  · simpa [h] using norm_le_mul_norm_add' x y

Norm Preservation under Multiplication by Zero-Norm Element: $\|x \cdot y\| = \|y\|$ when $\|x\| = 0$

Informal description

For any element $y$ in a seminormed group $E$ and any element $x \in E$ with $\|x\| = 0$, the norm of the product $x \cdot y$ equals the norm of $y$, i.e., $\|x \cdot y\| = \|y\|$.

norm_mul_eq_norm_left theorem

(x : E) {y : E} (h : ‖y‖ = 0) : ‖x * y‖ = ‖x‖

Full source

@[to_additive]
lemma norm_mul_eq_norm_left (x : E) {y : E} (h : ‖y‖ = 0) : ‖x * y‖ = ‖x‖ := by
  apply le_antisymm ?_ ?_
  · simpa [h] using norm_mul_le' x y
  · simpa [h] using norm_le_mul_norm_add x y

Norm Preservation under Multiplication by Zero-Norm Element: $\|x * y\| = \|x\|$ when $\|y\| = 0$

Informal description

For any element $x$ in a seminormed group $E$ and any element $y \in E$ with $\|y\| = 0$, the norm of the product $x * y$ equals the norm of $x$, i.e., $\|x * y\| = \|x\|$.

norm_div_eq_norm_right theorem

{x : E} (y : E) (h : ‖x‖ = 0) : ‖x / y‖ = ‖y‖

Full source

@[to_additive]
lemma norm_div_eq_norm_right {x : E} (y : E) (h : ‖x‖ = 0) : ‖x / y‖ = ‖y‖ := by
  apply le_antisymm ?_ ?_
  · simpa [h] using norm_div_le x y
  · simpa [h, norm_div_rev x y] using norm_sub_norm_le' y x

Norm of Quotient Equals Norm of Denominator When Numerator Has Zero Norm

Informal description

For any element $y$ in a seminormed group $E$ and any element $x \in E$ with $\|x\| = 0$, the norm of the quotient $x / y$ equals the norm of $y$, i.e., $\|x / y\| = \|y\|$.

norm_div_eq_norm_left theorem

(x : E) {y : E} (h : ‖y‖ = 0) : ‖x / y‖ = ‖x‖

Full source

@[to_additive]
lemma norm_div_eq_norm_left (x : E) {y : E} (h : ‖y‖ = 0) : ‖x / y‖ = ‖x‖ := by
  apply le_antisymm ?_ ?_
  · simpa [h] using norm_div_le x y
  · simpa [h] using norm_sub_norm_le' x y

Norm Preservation under Division by Zero-Norm Element: $\|x / y\| = \|x\|$ when $\|y\| = 0$

Informal description

For any element $x$ in a seminormed group $E$ and any element $y \in E$ with $\|y\| = 0$, the norm of the quotient $x / y$ equals the norm of $x$, i.e., $\|x / y\| = \|x\|$.

ball_eq' theorem

(y : E) (ε : ℝ) : ball y ε = {x | ‖x / y‖ < ε}

Full source

@[to_additive ball_eq]
theorem ball_eq' (y : E) (ε : ℝ) : ball y ε = { x | ‖x / y‖ < ε } :=
  Set.ext fun a => by simp [dist_eq_norm_div]

Open Ball Characterization via Quotient Norm in Seminormed Groups

Informal description

For any element $y$ in a seminormed group $E$ and any positive real number $\varepsilon$, the open ball centered at $y$ with radius $\varepsilon$ is equal to the set of all elements $x \in E$ such that the norm of the quotient $x / y$ is less than $\varepsilon$, i.e., \[ \text{ball}(y, \varepsilon) = \{x \mid \|x / y\| < \varepsilon\}. \]

ball_one_eq theorem

(r : ℝ) : ball (1 : E) r = {x | ‖x‖ < r}

Full source

@[to_additive]
theorem ball_one_eq (r : ℝ) : ball (1 : E) r = { x | ‖x‖ < r } :=
  Set.ext fun a => by simp

Open Ball at Identity Equals Elements with Norm Less Than Radius

Informal description

For any positive real number $r$, the open ball centered at the identity element $1$ of a seminormed group $E$ with radius $r$ is equal to the set of all elements $x \in E$ with norm less than $r$, i.e., \[ \text{ball}(1, r) = \{x \mid \|x\| < r\}. \]

mem_ball_iff_norm'' theorem

: b ∈ ball a r ↔ ‖b / a‖ < r

Full source

@[to_additive mem_ball_iff_norm]
theorem mem_ball_iff_norm'' : b ∈ ball a rb ∈ ball a r ↔ ‖b / a‖ < r := by rw [mem_ball, dist_eq_norm_div]

Open Ball Membership Criterion via Quotient Norm in Seminormed Groups

Informal description

For any elements $a$ and $b$ in a seminormed group $E$ and any positive real number $r$, the element $b$ belongs to the open ball centered at $a$ with radius $r$ if and only if the norm of the quotient $b / a$ is less than $r$, i.e., \[ b \in \text{ball}(a, r) \leftrightarrow \|b / a\| < r. \]

mem_ball_iff_norm''' theorem

: b ∈ ball a r ↔ ‖a / b‖ < r

Full source

@[to_additive mem_ball_iff_norm']
theorem mem_ball_iff_norm''' : b ∈ ball a rb ∈ ball a r ↔ ‖a / b‖ < r := by rw [mem_ball', dist_eq_norm_div]

Open Ball Membership Criterion via Norm of Reverse Quotient in Seminormed Groups

Informal description

For any elements $a$ and $b$ in a seminormed group $E$ and any positive real number $r$, the element $b$ belongs to the open ball centered at $a$ with radius $r$ if and only if the norm of the quotient $a / b$ is less than $r$, i.e., \[ b \in \text{ball}(a, r) \leftrightarrow \|a / b\| < r. \]

mem_ball_one_iff theorem

: a ∈ ball (1 : E) r ↔ ‖a‖ < r

Full source

@[to_additive]
theorem mem_ball_one_iff : a ∈ ball (1 : E) ra ∈ ball (1 : E) r ↔ ‖a‖ < r := by rw [mem_ball, dist_one_right]

Open Ball at Identity Characterization via Norm: $\|a\| < r \leftrightarrow a \in B(1, r)$

Informal description

For any element $a$ in a seminormed group $E$ and any positive real number $r$, the element $a$ belongs to the open ball centered at the identity element $1$ with radius $r$ if and only if the norm of $a$ is strictly less than $r$, i.e., \[ a \in \text{ball}(1, r) \leftrightarrow \|a\| < r. \]

mem_closedBall_iff_norm'' theorem

: b ∈ closedBall a r ↔ ‖b / a‖ ≤ r

Full source

@[to_additive mem_closedBall_iff_norm]
theorem mem_closedBall_iff_norm'' : b ∈ closedBall a rb ∈ closedBall a r ↔ ‖b / a‖ ≤ r := by
  rw [mem_closedBall, dist_eq_norm_div]

Closed Ball Membership Criterion via Norm of Quotient in Seminormed Groups

Informal description

For any elements $a$ and $b$ in a seminormed group $E$, the point $b$ belongs to the closed ball centered at $a$ with radius $r$ if and only if the norm of $b / a$ is less than or equal to $r$, i.e., $b \in \overline{B}(a, r) \leftrightarrow \|b / a\| \leq r$.

mem_closedBall_one_iff theorem

: a ∈ closedBall (1 : E) r ↔ ‖a‖ ≤ r

Full source

@[to_additive]
theorem mem_closedBall_one_iff : a ∈ closedBall (1 : E) ra ∈ closedBall (1 : E) r ↔ ‖a‖ ≤ r := by
  rw [mem_closedBall, dist_one_right]

Closed Ball Membership at Identity via Norm in Seminormed Groups

Informal description

For any element $a$ in a seminormed group $E$ and any non-negative real number $r$, the element $a$ belongs to the closed ball centered at the identity element $1$ with radius $r$ if and only if the norm of $a$ is less than or equal to $r$, i.e., $a \in \overline{B}(1, r) \leftrightarrow \|a\| \leq r$.

mem_closedBall_iff_norm''' theorem

: b ∈ closedBall a r ↔ ‖a / b‖ ≤ r

Full source

@[to_additive mem_closedBall_iff_norm']
theorem mem_closedBall_iff_norm''' : b ∈ closedBall a rb ∈ closedBall a r ↔ ‖a / b‖ ≤ r := by
  rw [mem_closedBall', dist_eq_norm_div]

Closed Ball Membership via Norm of Quotient in Seminormed Groups

Informal description

For any elements $a$ and $b$ in a seminormed group $E$, the point $b$ belongs to the closed ball centered at $a$ with radius $r$ if and only if the norm of $a / b$ is less than or equal to $r$, i.e., $b \in \overline{B}(a, r) \leftrightarrow \|a / b\| \leq r$.

norm_le_of_mem_closedBall' theorem

(h : b ∈ closedBall a r) : ‖b‖ ≤ ‖a‖ + r

Full source

@[to_additive norm_le_of_mem_closedBall]
theorem norm_le_of_mem_closedBall' (h : b ∈ closedBall a r) : ‖b‖ ≤ ‖a‖ + r :=
  (norm_le_norm_add_norm_div' _ _).trans <| add_le_add_left (by rwa [← dist_eq_norm_div]) _

Norm Bound in Closed Ball: $\|b\| \leq \|a\| + r$ when $b \in \overline{B}(a, r)$

Informal description

For any elements $a$ and $b$ in a seminormed group $E$, if $b$ belongs to the closed ball centered at $a$ with radius $r$, then the norm of $b$ is bounded by the norm of $a$ plus $r$, i.e., $\|b\| \leq \|a\| + r$.

norm_le_norm_add_const_of_dist_le' theorem

: dist a b ≤ r → ‖a‖ ≤ ‖b‖ + r

Full source

@[to_additive norm_le_norm_add_const_of_dist_le]
theorem norm_le_norm_add_const_of_dist_le' : dist a b ≤ r → ‖a‖ ≤ ‖b‖ + r :=
  norm_le_of_mem_closedBall'

Norm Bound from Distance: $\|a\| \leq \|b\| + r$ when $\text{dist}(a, b) \leq r$

Informal description

For any elements $a$ and $b$ in a seminormed group $E$, if the distance between $a$ and $b$ is at most $r$, then the norm of $a$ is bounded by the norm of $b$ plus $r$, i.e., $\|a\| \leq \|b\| + r$.

norm_lt_of_mem_ball' theorem

(h : b ∈ ball a r) : ‖b‖ < ‖a‖ + r

Full source

@[to_additive norm_lt_of_mem_ball]
theorem norm_lt_of_mem_ball' (h : b ∈ ball a r) : ‖b‖ < ‖a‖ + r :=
  (norm_le_norm_add_norm_div' _ _).trans_lt <| add_lt_add_left (by rwa [← dist_eq_norm_div]) _

Norm Bound in Open Ball: $\|b\| < \|a\| + r$ when $b \in B(a, r)$

Informal description

For any elements $a$ and $b$ in a seminormed group $E$, if $b$ belongs to the open ball centered at $a$ with radius $r$, then the norm of $b$ is strictly less than the norm of $a$ plus $r$, i.e., $\|b\| < \|a\| + r$.

norm_div_sub_norm_div_le_norm_div theorem

(u v w : E) : ‖u / w‖ - ‖v / w‖ ≤ ‖u / v‖

Full source

@[to_additive]
theorem norm_div_sub_norm_div_le_norm_div (u v w : E) : ‖u / w‖ - ‖v / w‖ ≤ ‖u / v‖ := by
  simpa only [div_div_div_cancel_right] using norm_sub_norm_le' (u / w) (v / w)

Difference of Quotient Norms Bounded by Quotient Norm: $\|u/w\| - \|v/w\| \leq \|u/v\|$

Informal description

For any elements $u, v, w$ in a seminormed group $E$, the difference of the norms of $u/w$ and $v/w$ is bounded by the norm of $u/v$, i.e., \[ \|u / w\| - \|v / w\| \leq \|u / v\|. \]

mem_sphere_iff_norm' theorem

: b ∈ sphere a r ↔ ‖b / a‖ = r

Full source

@[to_additive (attr := simp 1001) mem_sphere_iff_norm]
-- Porting note: increase priority so the left-hand side doesn't reduce
theorem mem_sphere_iff_norm' : b ∈ sphere a rb ∈ sphere a r ↔ ‖b / a‖ = r := by simp [dist_eq_norm_div]

Sphere Membership Criterion via Quotient Norm: $\text{sphere}(a, r) = \{b \mid \|b/a\| = r\}$

Informal description

For elements $a$ and $b$ in a seminormed group $E$ and a non-negative real number $r$, $b$ belongs to the sphere centered at $a$ with radius $r$ if and only if the norm of the quotient $b/a$ equals $r$, i.e., $b \in \text{sphere}(a, r) \leftrightarrow \|b / a\| = r$.

mem_sphere_one_iff_norm theorem

: a ∈ sphere (1 : E) r ↔ ‖a‖ = r

Full source

@[to_additive] -- `simp` can prove this
theorem mem_sphere_one_iff_norm : a ∈ sphere (1 : E) ra ∈ sphere (1 : E) r ↔ ‖a‖ = r := by simp [dist_eq_norm_div]

Characterization of Sphere Membership via Norm: $\text{sphere}(1, r) = \{a \mid \|a\| = r\}$

Informal description

For an element $a$ in a seminormed group $E$ and a non-negative real number $r$, $a$ belongs to the sphere centered at the identity element $1$ with radius $r$ if and only if the norm of $a$ equals $r$, i.e., $a \in \text{sphere}(1, r) \leftrightarrow \|a\| = r$.

norm_eq_of_mem_sphere' theorem

(x : sphere (1 : E) r) : ‖(x : E)‖ = r

Full source

@[to_additive (attr := simp) norm_eq_of_mem_sphere]
theorem norm_eq_of_mem_sphere' (x : sphere (1 : E) r) : ‖(x : E)‖ = r :=
  mem_sphere_one_iff_norm.mp x.2

Norm Equality for Elements in the Sphere Centered at Identity

Informal description

For any element $x$ in the sphere centered at the identity element $1$ with radius $r$ in a seminormed group $E$, the norm of $x$ is equal to $r$, i.e., $\|x\| = r$.

ne_one_of_mem_sphere theorem

(hr : r ≠ 0) (x : sphere (1 : E) r) : (x : E) ≠ 1

Full source

@[to_additive]
theorem ne_one_of_mem_sphere (hr : r ≠ 0) (x : sphere (1 : E) r) : (x : E) ≠ 1 :=
  ne_one_of_norm_ne_zero <| by rwa [norm_eq_of_mem_sphere' x]

Non-identity Elements in Nonzero Radius Spheres in Seminormed Groups

Informal description

For any nonzero radius $r$ in a seminormed group $E$, if an element $x$ belongs to the sphere centered at the identity element $1$ with radius $r$, then $x$ is not equal to the identity element, i.e., $x \neq 1$.

ne_one_of_mem_unit_sphere theorem

(x : sphere (1 : E) 1) : (x : E) ≠ 1

Full source

@[to_additive ne_zero_of_mem_unit_sphere]
theorem ne_one_of_mem_unit_sphere (x : sphere (1 : E) 1) : (x : E) ≠ 1 :=
  ne_one_of_mem_sphere one_ne_zero _

Non-identity Elements in Unit Sphere of Seminormed Group

Informal description

For any element $x$ in the unit sphere centered at the identity element $1$ of a seminormed group $E$, we have $x \neq 1$.

normGroupSeminorm definition

: GroupSeminorm E

Full source

/-- The norm of a seminormed group as a group seminorm. -/
@[to_additive "The norm of a seminormed group as an additive group seminorm."]
def normGroupSeminorm : GroupSeminorm E :=
  ⟨norm, norm_one', norm_mul_le', norm_inv'⟩

Norm as a group seminorm

Informal description

The function that assigns to each element $x$ of a seminormed group $E$ its norm $\|x\|$ is a group seminorm, meaning it satisfies the following properties: 1. $\|1\| = 0$ (the norm of the identity is zero) 2. $\|x \cdot y\| \leq \|x\| + \|y\|$ for all $x, y \in E$ (subadditivity) 3. $\|x^{-1}\| = \|x\|$ for all $x \in E$ (inverse-invariance)

coe_normGroupSeminorm theorem

: ⇑(normGroupSeminorm E) = norm

Full source

@[to_additive (attr := simp)]
theorem coe_normGroupSeminorm : ⇑(normGroupSeminorm E) = norm :=
  rfl

Group Seminorm Coincides with Norm Function

Informal description

The function associated with the group seminorm structure on a seminormed group $E$ coincides with the norm function, i.e., for any $x \in E$, the evaluation of the group seminorm at $x$ equals the norm of $x$.

NormedCommGroup.tendsto_nhds_one theorem

{f : α → E} {l : Filter α} : Tendsto f l (𝓝 1) ↔ ∀ ε > 0, ∀ᶠ x in l, ‖f x‖ < ε

Full source

@[to_additive]
theorem NormedCommGroup.tendsto_nhds_one {f : α → E} {l : Filter α} :
    TendstoTendsto f l (𝓝 1) ↔ ∀ ε > 0, ∀ᶠ x in l, ‖f x‖ < ε :=
  Metric.tendsto_nhds.trans <| by simp only [dist_one_right]

Convergence to Identity in Normed Commutative Groups via Norm Condition

Informal description

Let $E$ be a normed commutative group. A function $f : \alpha \to E$ converges to the identity element $1$ along a filter $l$ if and only if for every $\varepsilon > 0$, the set $\{x \in \alpha \mid \|f(x)\| < \varepsilon\}$ is eventually in $l$.

NormedCommGroup.tendsto_nhds_nhds theorem

 {f : E → F} {x : E} {y : F} : Tendsto f (𝓝 x) (𝓝 y) ↔ ∀ ε > 0, ∃ δ > 0, ∀ x', ‖x' / x‖ < δ → ‖f x' / y‖ < ε

Full source

@[to_additive]
theorem NormedCommGroup.tendsto_nhds_nhds {f : E → F} {x : E} {y : F} :
    TendstoTendsto f (𝓝 x) (𝓝 y) ↔ ∀ ε > 0, ∃ δ > 0, ∀ x', ‖x' / x‖ < δ → ‖f x' / y‖ < ε := by
  simp_rw [Metric.tendsto_nhds_nhds, dist_eq_norm_div]

Limit Characterization in Normed Commutative Groups via Quotient Norms

Informal description

Let $E$ and $F$ be normed commutative groups. A function $f: E \to F$ tends to $y$ at $x$ (i.e., $\lim_{x' \to x} f(x') = y$) if and only if for every $\varepsilon > 0$, there exists $\delta > 0$ such that for all $x' \in E$, if $\|x' / x\| < \delta$, then $\|f(x') / y\| < \varepsilon$.

NormedCommGroup.nhds_basis_norm_lt theorem

(x : E) : (𝓝 x).HasBasis (fun ε : ℝ => 0 < ε) fun ε => {y | ‖y / x‖ < ε}

Full source

@[to_additive]
theorem NormedCommGroup.nhds_basis_norm_lt (x : E) :
    (𝓝 x).HasBasis (fun ε : ℝ => 0 < ε) fun ε => { y | ‖y / x‖ < ε } := by
  simp_rw [← ball_eq']
  exact Metric.nhds_basis_ball

Basis of Neighborhoods via Norm of Quotient in Normed Commutative Groups

Informal description

For any element $x$ in a normed commutative group $E$, the neighborhood filter $\mathcal{N}(x)$ has a basis consisting of sets of the form $\{ y \mid \|y / x\| < \varepsilon \}$ for all $\varepsilon > 0$.

NormedCommGroup.nhds_one_basis_norm_lt theorem

: (𝓝 (1 : E)).HasBasis (fun ε : ℝ => 0 < ε) fun ε => {y | ‖y‖ < ε}

Full source

@[to_additive]
theorem NormedCommGroup.nhds_one_basis_norm_lt :
    (𝓝 (1 : E)).HasBasis (fun ε : ℝ => 0 < ε) fun ε => { y | ‖y‖ < ε } := by
  convert NormedCommGroup.nhds_basis_norm_lt (1 : E)
  simp

Basis of Neighborhoods of Identity via Norm in Normed Commutative Groups

Informal description

The neighborhood filter $\mathcal{N}(1)$ of the identity element in a normed commutative group $E$ has a basis consisting of sets of the form $\{ y \mid \|y\| < \varepsilon \}$ for all $\varepsilon > 0$.

NormedCommGroup.uniformity_basis_dist theorem

: (𝓤 E).HasBasis (fun ε : ℝ => 0 < ε) fun ε => {p : E × E | ‖p.fst / p.snd‖ < ε}

Full source

@[to_additive]
theorem NormedCommGroup.uniformity_basis_dist :
    (𝓤 E).HasBasis (fun ε : ℝ => 0 < ε) fun ε => { p : E × E | ‖p.fst / p.snd‖ < ε } := by
  convert Metric.uniformity_basis_dist (α := E) using 1
  simp [dist_eq_norm_div]

Basis for Uniformity Filter via Norm of Quotient in Normed Commutative Groups

Informal description

The uniformity filter $\mathfrak{U}(E)$ of a normed commutative group $E$ has a basis consisting of the sets $\{(x, y) \mid \|x / y\| < \varepsilon\}$ for all positive real numbers $\varepsilon > 0$.

SeminormedGroup.toNNNorm instance

: NNNorm E

Full source

@[to_additive]
instance (priority := 100) SeminormedGroup.toNNNorm : NNNorm E :=
  ⟨fun a => ⟨‖a‖, norm_nonneg' a⟩⟩

Non-negative Norm on Seminormed Groups

Informal description

Every seminormed group $E$ can be endowed with a non-negative norm function $\|\cdot\|₊ : E \to \mathbb{R}_{\geq 0}$, where $\|x\|₊$ is defined as the norm $\|x\|$ of $x$ in $E$.

coe_nnnorm' theorem

(a : E) : (‖a‖₊ : ℝ) = ‖a‖

Full source

@[to_additive (attr := simp, norm_cast) coe_nnnorm]
theorem coe_nnnorm' (a : E) : (‖a‖₊ : ℝ) = ‖a‖ := rfl

Equality of Norm and Non-Negative Norm in Seminormed Groups

Informal description

For any element $a$ in a seminormed group $E$, the real-valued norm $\|a\|$ is equal to the non-negative real-valued norm $\|a\|₊$ when viewed as a real number, i.e., $(\|a\|₊ : \mathbb{R}) = \|a\|$.

coe_comp_nnnorm' theorem

: (toReal : ℝ≥0 → ℝ) ∘ (nnnorm : E → ℝ≥0) = norm

Full source

@[to_additive (attr := simp) coe_comp_nnnorm]
theorem coe_comp_nnnorm' : (toReal : ℝ≥0 → ℝ)(toReal : ℝ≥0 → ℝ) ∘ (nnnorm : E → ℝ≥0) = norm :=
  rfl

Equality of Norm Compositions in Seminormed Groups

Informal description

For any seminormed group $E$, the composition of the non-negative norm function $\|\cdot\|₊ : E \to \mathbb{R}_{\geq 0}$ with the canonical embedding $\mathbb{R}_{\geq 0} \to \mathbb{R}$ equals the norm function $\|\cdot\| : E \to \mathbb{R}$. In other words, for any $x \in E$, we have $\|x\|₊ = \|x\|$ when viewed as real numbers.

norm_toNNReal' theorem

: ‖a‖.toNNReal = ‖a‖₊

Full source

@[to_additive (attr := simp) norm_toNNReal]
theorem norm_toNNReal' : ‖a‖.toNNReal = ‖a‖₊ :=
  @Real.toNNReal_coe ‖a‖₊

Equality of Truncated Norm and Non-Negative Norm in Seminormed Groups

Informal description

For any element $a$ in a seminormed group $E$, the non-negative real number obtained by truncating the norm $\|a\|$ to $\mathbb{R}_{\geq 0}$ equals the non-negative norm $\|a\|₊$ of $a$.

toReal_enorm' theorem

(x : E) : ‖x‖ₑ.toReal = ‖x‖

Full source

@[to_additive (attr := simp) toReal_enorm]
lemma toReal_enorm' (x : E) : ‖x‖ₑ.toReal = ‖x‖ := by simp [enorm]

Equality of Extended Norm's Real Value and Norm in Seminormed Groups

Informal description

For any element $x$ in a seminormed group $E$, the real value of the extended norm $\|x\|_e$ equals the norm $\|x\|$ of $x$.

ofReal_norm' theorem

(x : E) : .ofReal ‖x‖ = ‖x‖ₑ

Full source

@[to_additive (attr := simp) ofReal_norm]
lemma ofReal_norm' (x : E) : .ofReal ‖x‖ = ‖x‖ₑ := by
  simp [enorm, ENNReal.ofReal, Real.toNNReal, nnnorm]

Embedding of Norm into Extended Nonnegative Reals: $\text{ofReal}(\|x\|) = \|x\|_e$

Informal description

For any element $x$ in a seminormed group $E$, the extended nonnegative real number obtained by embedding the norm $\|x\|$ via the function $\mathbb{R} \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ is equal to the extended norm $\|x\|_e$ of $x$.

enorm'_eq_iff_norm_eq theorem

{x : E} {y : F} : ‖x‖ₑ = ‖y‖ₑ ↔ ‖x‖ = ‖y‖

Full source

@[to_additive enorm_eq_iff_norm_eq]
theorem enorm'_eq_iff_norm_eq {x : E} {y : F} : ‖x‖ₑ‖x‖ₑ = ‖y‖ₑ ↔ ‖x‖ = ‖y‖ := by
  simp only [← ofReal_norm']
  refine ⟨fun h ↦ ?_, fun h ↦ by congr⟩
  exact (Real.toNNReal_eq_toNNReal_iff (norm_nonneg' _) (norm_nonneg' _)).mp (ENNReal.coe_inj.mp h)

Equality of Extended Norms vs. Standard Norms in Seminormed Groups

Informal description

For elements $x$ in a seminormed group $E$ and $y$ in a seminormed group $F$, the extended norms $\|x\|_e$ and $\|y\|_e$ are equal if and only if the standard norms $\|x\|$ and $\|y\|$ are equal.

enorm'_le_iff_norm_le theorem

{x : E} {y : F} : ‖x‖ₑ ≤ ‖y‖ₑ ↔ ‖x‖ ≤ ‖y‖

Full source

@[to_additive enorm_le_iff_norm_le]
theorem enorm'_le_iff_norm_le {x : E} {y : F} : ‖x‖ₑ‖x‖ₑ ≤ ‖y‖ₑ ↔ ‖x‖ ≤ ‖y‖ := by
  simp only [← ofReal_norm']
  refine ⟨fun h ↦ ?_, fun h ↦ by gcongr⟩
  rw [ENNReal.ofReal_le_ofReal_iff (norm_nonneg' _)] at h
  exact h

Extended Norm Inequality Equivalence: $\|x\|_e \leq \|y\|_e \leftrightarrow \|x\| \leq \|y\|$

Informal description

For elements $x$ in a seminormed group $E$ and $y$ in a seminormed group $F$, the extended norm inequality $\|x\|_e \leq \|y\|_e$ holds if and only if the standard norm inequality $\|x\| \leq \|y\|$ holds.

nndist_eq_nnnorm_div theorem

(a b : E) : nndist a b = ‖a / b‖₊

Full source

@[to_additive]
theorem nndist_eq_nnnorm_div (a b : E) : nndist a b = ‖a / b‖₊ :=
  NNReal.eq <| dist_eq_norm_div _ _

Non-negative Distance as Quotient Norm in Seminormed Groups

Informal description

For any elements $a$ and $b$ in a seminormed group $E$, the non-negative distance between $a$ and $b$ is equal to the non-negative norm of their quotient, i.e., $\text{nndist}(a, b) = \|a / b\|₊$.

nndist_one_right theorem

(a : E) : nndist a 1 = ‖a‖₊

Full source

@[to_additive (attr := simp)]
theorem nndist_one_right (a : E) : nndist a 1 = ‖a‖₊ := by simp [nndist_eq_nnnorm_div]

Non-negative Distance to Identity Equals Norm in Seminormed Groups

Informal description

For any element $a$ in a seminormed group $E$, the non-negative distance between $a$ and the identity element $1$ is equal to the non-negative norm of $a$, i.e., $\text{nndist}(a, 1) = \|a\|₊$.

edist_one_right theorem

(a : E) : edist a 1 = ‖a‖ₑ

Full source

@[to_additive (attr := simp)]
lemma edist_one_right (a : E) : edist a 1 = ‖a‖ₑ := by simp [edist_nndist, nndist_one_right, enorm]

Extended Distance to Identity Equals Extended Norm in Seminormed Groups

Informal description

For any element $a$ in a seminormed group $E$, the extended distance between $a$ and the identity element $1$ is equal to the extended norm of $a$, i.e., $\text{edist}(a, 1) = \|a\|_e$.

nnnorm_one' theorem

: ‖(1 : E)‖₊ = 0

Full source

@[to_additive (attr := simp) nnnorm_zero]
theorem nnnorm_one' : ‖(1 : E)‖₊ = 0 := NNReal.eq norm_one'

Non-negative Norm of Identity is Zero in Seminormed Groups

Informal description

In a seminormed group $E$, the non-negative norm of the identity element $1$ is zero, i.e., $\|1\|₊ = 0$.

ne_one_of_nnnorm_ne_zero theorem

{a : E} : ‖a‖₊ ≠ 0 → a ≠ 1

Full source

@[to_additive]
theorem ne_one_of_nnnorm_ne_zero {a : E} : ‖a‖₊‖a‖₊ ≠ 0 → a ≠ 1 :=
  mt <| by
    rintro rfl
    exact nnnorm_one'

Non-zero norm implies non-identity: $\|a\|₊ \neq 0 \Rightarrow a \neq 1$

Informal description

For any element $a$ in a seminormed group $E$, if the non-negative norm $\|a\|₊$ is not zero, then $a$ is not the identity element $1$.

nnnorm_mul_le' theorem

(a b : E) : ‖a * b‖₊ ≤ ‖a‖₊ + ‖b‖₊

Full source

@[to_additive nnnorm_add_le]
theorem nnnorm_mul_le' (a b : E) : ‖a * b‖₊ ≤ ‖a‖₊ + ‖b‖₊ :=
  NNReal.coe_le_coe.1 <| norm_mul_le' a b

Triangle Inequality for Non-Negative Norm of Product: $\|a \cdot b\|₊ \leq \|a\|₊ + \|b\|₊$

Informal description

For any two elements $a$ and $b$ in a seminormed group $E$, the non-negative norm of their product satisfies the inequality $\|a \cdot b\|₊ \leq \|a\|₊ + \|b\|₊$.

norm_pow_le_mul_norm theorem

: ∀ {n : ℕ}, ‖a ^ n‖ ≤ n * ‖a‖

Full source

@[to_additive norm_nsmul_le]
lemma norm_pow_le_mul_norm : ∀ {n : ℕ}, ‖a ^ n‖ ≤ n * ‖a‖
  | 0 => by simp
  | n + 1 => by simpa [pow_succ, add_mul] using norm_mul_le_of_le' norm_pow_le_mul_norm le_rfl

Norm of Power Bounded by Multiple of Norm: $\|a^n\| \leq n \cdot \|a\|$

Informal description

For any element $a$ in a seminormed group $E$ and any natural number $n$, the norm of $a^n$ satisfies $\|a^n\| \leq n \cdot \|a\|$.

nnnorm_pow_le_mul_norm theorem

{n : ℕ} : ‖a ^ n‖₊ ≤ n * ‖a‖₊

Full source

@[to_additive nnnorm_nsmul_le]
lemma nnnorm_pow_le_mul_norm {n : ℕ} : ‖a ^ n‖₊ ≤ n * ‖a‖₊ := by
  simpa only [← NNReal.coe_le_coe, NNReal.coe_mul, NNReal.coe_natCast] using norm_pow_le_mul_norm

Non-negative Norm of Power Bounded by Multiple of Norm: $\|a^n\|₊ \leq n \cdot \|a\|₊$

Informal description

For any element $a$ in a seminormed group $E$ and any natural number $n$, the non-negative norm of $a^n$ satisfies $\|a^n\|₊ \leq n \cdot \|a\|₊$.

nnnorm_inv' theorem

(a : E) : ‖a⁻¹‖₊ = ‖a‖₊

Full source

@[to_additive (attr := simp) nnnorm_neg]
theorem nnnorm_inv' (a : E) : ‖a⁻¹‖₊ = ‖a‖₊ :=
  NNReal.eq <| norm_inv' a

Non-negative Norm Identity: $\|a^{-1}\|₊ = \|a\|₊$

Informal description

For any element $a$ in a seminormed group $E$, the non-negative norm of the inverse $a^{-1}$ is equal to the non-negative norm of $a$, i.e., $\|a^{-1}\|₊ = \|a\|₊$.

nnnorm_zpow_abs theorem

(a : E) (n : ℤ) : ‖a ^ |n|‖₊ = ‖a ^ n‖₊

Full source

@[to_additive (attr := simp) nnnorm_abs_zsmul]
theorem nnnorm_zpow_abs (a : E) (n : ℤ) : ‖a ^ |n|‖₊ = ‖a ^ n‖₊ :=
  NNReal.eq <| norm_zpow_abs a n

Non-negative Norm Identity: $\|a^{|n|}\|₊ = \|a^n\|₊$

Informal description

For any element $a$ in a seminormed group $E$ and any integer $n$, the non-negative norm of $a$ raised to the absolute value of $n$ is equal to the non-negative norm of $a$ raised to $n$, i.e., $\|a^{|n|}\|₊ = \|a^n\|₊$.

nnnorm_pow_natAbs theorem

(a : E) (n : ℤ) : ‖a ^ n.natAbs‖₊ = ‖a ^ n‖₊

Full source

@[to_additive (attr := simp) nnnorm_natAbs_smul]
theorem nnnorm_pow_natAbs (a : E) (n : ℤ) : ‖a ^ n.natAbs‖₊ = ‖a ^ n‖₊ :=
  NNReal.eq <| norm_pow_natAbs a n

Non-negative Norm Identity: $\|a^{\text{natAbs}(n)}\|₊ = \|a^n\|₊$

Informal description

For any element $a$ in a seminormed group $E$ and any integer $n$, the non-negative norm of $a$ raised to the natural number absolute value of $n$ is equal to the non-negative norm of $a$ raised to $n$, i.e., $\|a^{\text{natAbs}(n)}\|₊ = \|a^n\|₊$.

nnnorm_zpow_isUnit theorem

(a : E) {n : ℤ} (hn : IsUnit n) : ‖a ^ n‖₊ = ‖a‖₊

Full source

@[to_additive nnnorm_isUnit_zsmul]
theorem nnnorm_zpow_isUnit (a : E) {n : ℤ} (hn : IsUnit n) : ‖a ^ n‖₊ = ‖a‖₊ :=
  NNReal.eq <| norm_zpow_isUnit a hn

Non-negative norm identity: $\|a^n\|₊ = \|a\|₊$ for $n = \pm 1$

Informal description

For any element $a$ in a seminormed group $E$ and any integer $n$ that is a unit (i.e., $n = \pm 1$), the non-negative norm of $a^n$ equals the non-negative norm of $a$, i.e., $\|a^n\|₊ = \|a\|₊$.

nnnorm_units_zsmul theorem

{E : Type*} [SeminormedAddGroup E] (n : ℤˣ) (a : E) : ‖n • a‖₊ = ‖a‖₊

Full source

@[simp]
theorem nnnorm_units_zsmul {E : Type*} [SeminormedAddGroup E] (n : ℤℤˣ) (a : E) : ‖n • a‖₊ = ‖a‖₊ :=
  NNReal.eq <| norm_isUnit_zsmul a n.isUnit

Non-negative Norm Invariance under Integer Unit Scalar Multiplication: $\|n \cdot a\|₊ = \|a\|₊$ for $n = \pm 1$

Informal description

For any seminormed additive group $E$ and any unit $n$ in the integers (i.e., $n = \pm 1$), the non-negative norm of the scalar multiple $n \cdot a$ is equal to the non-negative norm of $a$, i.e., $\|n \cdot a\|₊ = \|a\|₊$.

nndist_one_left theorem

(a : E) : nndist 1 a = ‖a‖₊

Full source

@[to_additive (attr := simp)]
theorem nndist_one_left (a : E) : nndist 1 a = ‖a‖₊ := by simp [nndist_eq_nnnorm_div]

Distance from Identity Equals Norm: $\text{nndist}(1, a) = \|a\|₊$

Informal description

For any element $a$ in a seminormed group $E$, the non-negative distance between the identity element $1$ and $a$ is equal to the non-negative norm of $a$, i.e., $\text{nndist}(1, a) = \|a\|₊$.

edist_one_left theorem

(a : E) : edist 1 a = ‖a‖₊

Full source

@[to_additive (attr := simp)]
theorem edist_one_left (a : E) : edist 1 a = ‖a‖₊ := by
  rw [edist_nndist, nndist_one_left]

Extended Distance from Identity Equals Norm: $\text{edist}(1, a) = \|a\|₊$

Informal description

For any element $a$ in a seminormed group $E$, the extended distance between the identity element $1$ and $a$ is equal to the non-negative norm of $a$, i.e., $\text{edist}(1, a) = \|a\|₊$.

nndist_mulIndicator theorem

 (s t : Set α) (f : α → E) (x : α) : nndist (s.mulIndicator f x) (t.mulIndicator f x) = ‖(s ∆ t).mulIndicator f x‖₊

Full source

@[to_additive]
theorem nndist_mulIndicator (s t : Set α) (f : α → E) (x : α) :
    nndist (s.mulIndicator f x) (t.mulIndicator f x) = ‖(s ∆ t).mulIndicator f x‖₊ :=
  NNReal.eq <| dist_mulIndicator s t f x

Non-negative Distance Between Multiplicative Indicators Equals Non-negative Norm on Symmetric Difference

Informal description

For any two sets $s, t \subseteq \alpha$, any function $f \colon \alpha \to E$ into a seminormed group $E$, and any element $x \in \alpha$, the non-negative distance between the multiplicative indicators of $f$ on $s$ and $t$ at $x$ is equal to the non-negative norm of the multiplicative indicator of $f$ on the symmetric difference $s \Delta t$ at $x$. That is, \[ \text{nndist}\big(\text{mulIndicator}_s f(x), \text{mulIndicator}_t f(x)\big) = \|\text{mulIndicator}_{s \Delta t} f(x)\|₊, \] where $\text{mulIndicator}_s f(x) = f(x)$ if $x \in s$ and $1$ otherwise, and $s \Delta t = (s \setminus t) \cup (t \setminus s)$ is the symmetric difference of $s$ and $t$.

nnnorm_div_le theorem

(a b : E) : ‖a / b‖₊ ≤ ‖a‖₊ + ‖b‖₊

Full source

@[to_additive]
theorem nnnorm_div_le (a b : E) : ‖a / b‖₊ ≤ ‖a‖₊ + ‖b‖₊ :=
  NNReal.coe_le_coe.1 <| norm_div_le _ _

Non-negative Norm Inequality for Quotient in Seminormed Groups: $\|a / b\|₊ \leq \|a\|₊ + \|b\|₊$

Informal description

For any elements $a$ and $b$ in a seminormed group $E$, the non-negative norm of their quotient satisfies the inequality $\|a / b\|₊ \leq \|a\|₊ + \|b\|₊$.

enorm_div_le theorem

: ‖a / b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ

Full source

@[to_additive]
lemma enorm_div_le : ‖a / b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ := by
  simpa [enorm, ← ENNReal.coe_add] using nnnorm_div_le a b

Extended Norm Inequality for Quotient: $\|a / b\|_e \leq \|a\|_e + \|b\|_e$

Informal description

For any elements $a$ and $b$ in a seminormed group $E$, the extended norm of their quotient satisfies the inequality $\|a / b\|_e \leq \|a\|_e + \|b\|_e$, where $\|\cdot\|_e$ denotes the extended norm mapping to $\mathbb{R}_{\geq 0} \cup \{\infty\}$.

nndist_nnnorm_nnnorm_le' theorem

(a b : E) : nndist ‖a‖₊ ‖b‖₊ ≤ ‖a / b‖₊

Full source

@[to_additive nndist_nnnorm_nnnorm_le]
theorem nndist_nnnorm_nnnorm_le' (a b : E) : nndist ‖a‖₊ ‖b‖₊ ≤ ‖a / b‖₊ :=
  NNReal.coe_le_coe.1 <| dist_norm_norm_le' a b

Non-negative Distance Between Norms Bounded by Quotient Norm in Seminormed Groups

Informal description

For any elements $a$ and $b$ in a seminormed group $E$, the non-negative distance between their non-negative norms is bounded by the non-negative norm of their quotient, i.e., \[ \text{dist}(\|a\|₊, \|b\|₊) \leq \|a / b\|₊. \]

nnnorm_le_nnnorm_add_nnnorm_div theorem

(a b : E) : ‖b‖₊ ≤ ‖a‖₊ + ‖a / b‖₊

Full source

@[to_additive]
theorem nnnorm_le_nnnorm_add_nnnorm_div (a b : E) : ‖b‖₊ ≤ ‖a‖₊ + ‖a / b‖₊ :=
  norm_le_norm_add_norm_div _ _

Non-negative norm inequality: $\|b\|₊ \leq \|a\|₊ + \|a / b\|₊$ in seminormed groups

Informal description

For any elements $a$ and $b$ in a seminormed group $E$, the non-negative norm of $b$ satisfies the inequality $\|b\|₊ \leq \|a\|₊ + \|a / b\|₊$, where $\|\cdot\|₊$ denotes the non-negative norm function mapping to $\mathbb{R}_{\geq 0}$.

nnnorm_le_nnnorm_add_nnnorm_div' theorem

(a b : E) : ‖a‖₊ ≤ ‖b‖₊ + ‖a / b‖₊

Full source

@[to_additive]
theorem nnnorm_le_nnnorm_add_nnnorm_div' (a b : E) : ‖a‖₊ ≤ ‖b‖₊ + ‖a / b‖₊ :=
  norm_le_norm_add_norm_div' _ _

Non-negative Norm Inequality: $\|a\|₊ \leq \|b\|₊ + \|a / b\|₊$ in Seminormed Groups

Informal description

For any elements $a$ and $b$ in a seminormed group $E$, the non-negative norm of $a$ satisfies the inequality $\|a\|₊ \leq \|b\|₊ + \|a / b\|₊$.

nnnorm_le_mul_nnnorm_add theorem

(a b : E) : ‖a‖₊ ≤ ‖a * b‖₊ + ‖b‖₊

Full source

@[to_additive]
theorem nnnorm_le_mul_nnnorm_add (a b : E) : ‖a‖₊ ≤ ‖a * b‖₊ + ‖b‖₊ :=
  norm_le_mul_norm_add _ _

Non-negative Norm Inequality: $\|a\|₊ \leq \|a \cdot b\|₊ + \|b\|₊$ in Seminormed Groups

Informal description

For any elements $a$ and $b$ in a seminormed group $E$, the non-negative norm of $a$ satisfies the inequality $\|a\|₊ \leq \|a \cdot b\|₊ + \|b\|₊$.

nnnorm_le_mul_nnnorm_add' theorem

(a b : E) : ‖b‖₊ ≤ ‖a * b‖₊ + ‖a‖₊

Full source

/-- An analogue of `nnnorm_le_mul_nnnorm_add` for the multiplication from the left. -/
@[to_additive "An analogue of `nnnorm_le_add_nnnorm_add` for the addition from the left."]
theorem nnnorm_le_mul_nnnorm_add' (a b : E) : ‖b‖₊ ≤ ‖a * b‖₊ + ‖a‖₊ :=
  norm_le_mul_norm_add' _ _

Non-negative Norm Inequality: $\|b\|₊ \leq \|a \cdot b\|₊ + \|a\|₊$ in Seminormed Groups

Informal description

For any elements $a$ and $b$ in a seminormed group $E$, the non-negative norm of $b$ satisfies the inequality $\|b\|₊ \leq \|a \cdot b\|₊ + \|a\|₊$.

nnnorm_mul_eq_nnnorm_right theorem

{x : E} (y : E) (h : ‖x‖₊ = 0) : ‖x * y‖₊ = ‖y‖₊

Full source

@[to_additive]
lemma nnnorm_mul_eq_nnnorm_right {x : E} (y : E) (h : ‖x‖₊ = 0) : ‖x * y‖₊ = ‖y‖₊ :=
  NNReal.eq <| norm_mul_eq_norm_right _ <| congr_arg NNReal.toReal h

Non-negative Norm Preservation under Right Multiplication by Zero-Norm Element: $\|x \cdot y\|₊ = \|y\|₊$ when $\|x\|₊ = 0$

Informal description

For any element $y$ in a seminormed group $E$ and any element $x \in E$ with $\|x\|₊ = 0$, the non-negative norm of the product $x \cdot y$ equals the non-negative norm of $y$, i.e., $\|x \cdot y\|₊ = \|y\|₊$.

nnnorm_mul_eq_nnnorm_left theorem

(x : E) {y : E} (h : ‖y‖₊ = 0) : ‖x * y‖₊ = ‖x‖₊

Full source

@[to_additive]
lemma nnnorm_mul_eq_nnnorm_left (x : E) {y : E} (h : ‖y‖₊ = 0) : ‖x * y‖₊ = ‖x‖₊ :=
  NNReal.eq <| norm_mul_eq_norm_left _ <| congr_arg NNReal.toReal h

Non-negative Norm Preservation under Multiplication by Zero-Norm Element: $\|x * y\|₊ = \|x\|₊$ when $\|y\|₊ = 0$

Informal description

For any element $x$ in a seminormed group $E$ and any element $y \in E$ with $\|y\|₊ = 0$, the non-negative norm of the product $x * y$ equals the non-negative norm of $x$, i.e., $\|x * y\|₊ = \|x\|₊$.

nnnorm_div_eq_nnnorm_right theorem

{x : E} (y : E) (h : ‖x‖₊ = 0) : ‖x / y‖₊ = ‖y‖₊

Full source

@[to_additive]
lemma nnnorm_div_eq_nnnorm_right {x : E} (y : E) (h : ‖x‖₊ = 0) : ‖x / y‖₊ = ‖y‖₊ :=
  NNReal.eq <| norm_div_eq_norm_right _ <| congr_arg NNReal.toReal h

Non-negative Norm of Quotient Equals Norm of Denominator When Numerator Has Zero Norm

Informal description

For any element $y$ in a seminormed group $E$ and any element $x \in E$ with $\|x\|₊ = 0$, the non-negative norm of the quotient $x / y$ equals the non-negative norm of $y$, i.e., $\|x / y\|₊ = \|y\|₊$.

nnnorm_div_eq_nnnorm_left theorem

(x : E) {y : E} (h : ‖y‖₊ = 0) : ‖x / y‖₊ = ‖x‖₊

Full source

@[to_additive]
lemma nnnorm_div_eq_nnnorm_left (x : E) {y : E} (h : ‖y‖₊ = 0) : ‖x / y‖₊ = ‖x‖₊ :=
  NNReal.eq <| norm_div_eq_norm_left _ <| congr_arg NNReal.toReal h

Non-negative Norm Preservation under Division by Zero-Norm Element: $\|x / y\|₊ = \|x\|₊$ when $\|y\|₊ = 0$

Informal description

For any element $x$ in a seminormed group $E$ and any element $y \in E$ with $\|y\|₊ = 0$, the non-negative norm of the quotient $x / y$ equals the non-negative norm of $x$, i.e., $\|x / y\|₊ = \|x\|₊$.

toReal_coe_nnnorm' theorem

(a : E) : (‖a‖₊ : ℝ≥0∞).toReal = ‖a‖

Full source

/-- The non negative norm seen as an `ENNReal` and then as a `Real` is equal to the norm. -/
@[to_additive toReal_coe_nnnorm "The non negative norm seen as an `ENNReal` and
then as a `Real` is equal to the norm."]
theorem toReal_coe_nnnorm' (a : E) : (‖a‖₊ : ℝ≥0∞).toReal = ‖a‖ := rfl

Equality of Norm Conversions: $(\|a\|₊ : \mathbb{R}_{\geq 0} \cup \{\infty\}).\text{toReal} = \|a\|$

Informal description

For any element $a$ in a seminormed group $E$, the real number obtained by first taking the non-negative norm $\|a\|₊$ of $a$, casting it to an extended non-negative real number, and then converting it back to a real number, equals the norm $\|a\|$ of $a$.

edist_mulIndicator theorem

 (s t : Set α) (f : α → E) (x : α) : edist (s.mulIndicator f x) (t.mulIndicator f x) = ‖(s ∆ t).mulIndicator f x‖₊

Full source

@[to_additive]
theorem edist_mulIndicator (s t : Set α) (f : α → E) (x : α) :
    edist (s.mulIndicator f x) (t.mulIndicator f x) = ‖(s ∆ t).mulIndicator f x‖₊ := by
  rw [edist_nndist, nndist_mulIndicator]

Extended Distance Between Multiplicative Indicators Equals Non-negative Norm on Symmetric Difference

Informal description

For any two sets $s, t \subseteq \alpha$, any function $f \colon \alpha \to E$ into a seminormed group $E$, and any element $x \in \alpha$, the extended distance between the multiplicative indicators of $f$ on $s$ and $t$ at $x$ is equal to the non-negative norm of the multiplicative indicator of $f$ on the symmetric difference $s \Delta t$ at $x$. That is, \[ \text{edist}\big(\text{mulIndicator}_s f(x), \text{mulIndicator}_t f(x)\big) = \|\text{mulIndicator}_{s \Delta t} f(x)\|₊, \] where $\text{mulIndicator}_s f(x) = f(x)$ if $x \in s$ and $1$ otherwise, and $s \Delta t = (s \setminus t) \cup (t \setminus s)$ is the symmetric difference of $s$ and $t$.

enorm_one' theorem

{E : Type*} [TopologicalSpace E] [ENormedMonoid E] : ‖(1 : E)‖ₑ = 0

Full source

@[to_additive (attr := simp) enorm_zero]
lemma enorm_one' {E : Type*} [TopologicalSpace E] [ENormedMonoid E] : ‖(1 : E)‖ₑ = 0 := by
  rw [ENormedMonoid.enorm_eq_zero]

Enorm of Identity in Enormed Monoid is Zero

Informal description

For any topological space $E$ endowed with an enormed monoid structure, the enorm of the multiplicative identity element $1 \in E$ is zero, i.e., $\|1\|_e = 0$.

exists_enorm_lt' theorem

 (E : Type*) [TopologicalSpace E] [ENormedMonoid E] [hbot : NeBot (𝓝[≠] (1 : E))] {c : ℝ≥0∞} (hc : c ≠ 0) :
  ∃ x ≠ (1 : E), ‖x‖ₑ < c

Full source

@[to_additive exists_enorm_lt]
lemma exists_enorm_lt' (E : Type*) [TopologicalSpace E] [ENormedMonoid E]
    [hbot : NeBot (𝓝[≠] (1 : E))] {c : ℝ≥0∞} (hc : c ≠ 0) : ∃ x ≠ (1 : E), ‖x‖ₑ < c :=
  frequently_iff_neBot.mpr hbot |>.and_eventually
    (ContinuousENorm.continuous_enorm.tendsto' 1 0 (by simp) |>.eventually_lt_const hc.bot_lt)
    |>.exists

Existence of Non-Identity Elements with Arbitrarily Small Extended Norm in Enormed Monoids

Informal description

Let $E$ be a topological space endowed with an enormed monoid structure, and suppose the punctured neighborhood filter at the identity element $1 \in E$ is non-trivial. For any nonzero extended nonnegative real number $c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, there exists an element $x \in E$ distinct from $1$ such that the extended norm of $x$ is less than $c$, i.e., $\|x\|_e < c$.

enorm_inv' theorem

(a : E) : ‖a⁻¹‖ₑ = ‖a‖ₑ

Full source

@[to_additive (attr := simp) enorm_neg]
lemma enorm_inv' (a : E) : ‖a⁻¹‖ₑ = ‖a‖ₑ := by simp [enorm]

Extended Norm Identity: $\|a^{-1}\|_e = \|a\|_e$

Informal description

For any element $a$ in a seminormed group $E$, the extended norm of the inverse $a^{-1}$ is equal to the extended norm of $a$, i.e., $\|a^{-1}\|_e = \|a\|_e$.

ofReal_norm_eq_enorm' theorem

(a : E) : .ofReal ‖a‖ = ‖a‖ₑ

Full source

@[to_additive ofReal_norm_eq_enorm]
lemma ofReal_norm_eq_enorm' (a : E) : .ofReal ‖a‖ = ‖a‖ₑ := ENNReal.ofReal_eq_coe_nnreal _

Equality of Extended Real Embedding and Extended Norm: $\text{ofReal}(\|a\|) = \|a\|_e$

Informal description

For any element $a$ in a seminormed group $E$, the extended nonnegative real number obtained by applying `ENNReal.ofReal` to the norm $\|a\|$ is equal to the extended norm $\|a\|_e$ of $a$.

instENormENNReal instance

: ENorm ℝ≥0∞

Full source

instance : ENorm ℝ≥0∞ where
  enorm x := x

The Extended Norm Structure on Extended Nonnegative Real Numbers

Informal description

The extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ are equipped with a canonical extended norm structure, where the norm of an element is the element itself.

enorm_eq_self theorem

(x : ℝ≥0∞) : ‖x‖ₑ = x

Full source

@[simp] lemma enorm_eq_self (x : ℝ≥0∞) : ‖x‖ₑ = x := rfl

Extended Norm Identity: $\|x\|_e = x$ for $x \in \mathbb{R}_{\geq 0} \cup \{\infty\}$

Informal description

For any extended nonnegative real number $x \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the extended norm $\|x\|_e$ equals $x$ itself.

edist_eq_enorm_div theorem

(a b : E) : edist a b = ‖a / b‖ₑ

Full source

@[to_additive]
theorem edist_eq_enorm_div (a b : E) : edist a b = ‖a / b‖ₑ := by
  rw [edist_dist, dist_eq_norm_div, ofReal_norm_eq_enorm']

Extended Distance as Extended Norm of Quotient in Seminormed Groups

Informal description

For any elements $a$ and $b$ in a seminormed group $E$, the extended distance between $a$ and $b$ is equal to the extended norm of their quotient, i.e., $\text{edist}(a, b) = \|a / b\|_e$.

edist_one_eq_enorm theorem

(x : E) : edist x 1 = ‖x‖ₑ

Full source

@[to_additive]
theorem edist_one_eq_enorm (x : E) : edist x 1 = ‖x‖ₑ := by rw [edist_eq_enorm_div, div_one]

Extended Distance to Identity Equals Extended Norm: $\text{edist}(x, 1) = \|x\|_e$

Informal description

For any element $x$ in a seminormed group $E$, the extended distance between $x$ and the identity element $1$ is equal to the extended norm of $x$, i.e., $\text{edist}(x, 1) = \|x\|_e$.

mem_emetric_ball_one_iff theorem

{r : ℝ≥0∞} : a ∈ EMetric.ball 1 r ↔ ‖a‖ₑ < r

Full source

@[to_additive]
theorem mem_emetric_ball_one_iff {r : ℝ≥0∞} : a ∈ EMetric.ball 1 ra ∈ EMetric.ball 1 r ↔ ‖a‖ₑ < r := by
  rw [EMetric.mem_ball, edist_one_eq_enorm]

Characterization of Extended Metric Ball at Identity via Extended Norm: $a \in B(1, r) \leftrightarrow \|a\|_e < r$

Informal description

For any element $a$ in a seminormed group $E$ and any extended nonnegative real number $r$, $a$ belongs to the extended metric ball centered at the identity element $1$ with radius $r$ if and only if the extended norm of $a$ is strictly less than $r$, i.e., $a \in \text{EMetric.ball}(1, r) \leftrightarrow \|a\|_e < r$.

continuous_enorm theorem

: Continuous fun a : E ↦ ‖a‖ₑ

Full source

@[continuity, fun_prop]
lemma continuous_enorm : Continuous fun a : E ↦ ‖a‖ₑ := ContinuousENorm.continuous_enorm

Continuity of the Extended Norm Function

Informal description

The extended norm function $\| \cdot \|_e : E \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ is continuous on the topological space $E$.

Continuous.enorm theorem

: Continuous f → Continuous (‖f ·‖ₑ)

Full source

@[fun_prop]
lemma Continuous.enorm : Continuous f → Continuous (‖f ·‖ₑ) :=
  continuous_enorm.comp

Continuity of Extended Norm under Continuous Maps

Informal description

If a function $f : X \to E$ is continuous, then the composition $\|f(\cdot)\|_e : X \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ is also continuous.

ContinuousAt.enorm theorem

{a : X} (h : ContinuousAt f a) : ContinuousAt (‖f ·‖ₑ) a

Full source

lemma ContinuousAt.enorm {a : X} (h : ContinuousAt f a) : ContinuousAt (‖f ·‖ₑ) a := by fun_prop

Continuity of Extended Norm at a Point

Informal description

Let $X$ and $E$ be topological spaces, and let $f : X \to E$ be a function. If $f$ is continuous at a point $a \in X$, then the extended norm function $x \mapsto \|f(x)\|_e$ is also continuous at $a$.

ContinuousWithinAt.enorm theorem

{s : Set X} {a : X} (h : ContinuousWithinAt f s a) : ContinuousWithinAt (‖f ·‖ₑ) s a

Full source

@[fun_prop]
lemma ContinuousWithinAt.enorm {s : Set X} {a : X} (h : ContinuousWithinAt f s a) :
    ContinuousWithinAt (‖f ·‖ₑ) s a :=
  (ContinuousENorm.continuous_enorm.continuousWithinAt).comp (t := Set.univ) h
    (fun _ _ ↦ by trivial)

Continuity of Extended Norm Within a Subset at a Point

Informal description

Let $X$ and $E$ be topological spaces, $f : X \to E$ a function, $s \subseteq X$ a subset, and $a \in X$ a point. If $f$ is continuous within $s$ at $a$, then the extended norm function $x \mapsto \|f(x)\|_e$ is also continuous within $s$ at $a$.

ContinuousOn.enorm theorem

(h : ContinuousOn f s) : ContinuousOn (‖f ·‖ₑ) s

Full source

@[fun_prop]
lemma ContinuousOn.enorm (h : ContinuousOn f s) : ContinuousOn (‖f ·‖ₑ) s :=
  (ContinuousENorm.continuous_enorm.continuousOn).comp (t := Set.univ) h <| Set.mapsTo_univ _ _

Continuity of Extended Norm under Continuous Functions on Subsets

Informal description

Let $f \colon X \to E$ be a function from a topological space $X$ to an enormed monoid $E$, and let $s \subseteq X$ be a subset. If $f$ is continuous on $s$, then the extended norm function $\|f(\cdot)\|_e \colon X \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ is also continuous on $s$.

enorm_mul_le' theorem

(a b : E) : ‖a * b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ

Full source

@[to_additive enorm_add_le]
lemma enorm_mul_le' (a b : E) : ‖a * b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ := ENormedMonoid.enorm_mul_le a b

Subadditivity of Extended Norm in Enormed Monoid

Informal description

For any elements $a$ and $b$ in an enormed monoid $E$, the extended norm of their product satisfies the inequality $\|a \cdot b\|_e \leq \|a\|_e + \|b\|_e$.

enorm_eq_zero' theorem

{a : E} : ‖a‖ₑ = 0 ↔ a = 1

Full source

@[to_additive (attr := simp) enorm_eq_zero]
lemma enorm_eq_zero' {a : E} : ‖a‖ₑ‖a‖ₑ = 0 ↔ a = 1 := by
  simp [enorm, ENormedMonoid.enorm_eq_zero]

Extended Norm Vanishes at Identity in Enormed Monoid

Informal description

For any element $a$ in an enormed monoid $E$, the extended norm $\|a\|_e$ equals zero if and only if $a$ is the identity element of the monoid, i.e., $\|a\|_e = 0 \leftrightarrow a = 1$.

enorm_ne_zero' theorem

{a : E} : ‖a‖ₑ ≠ 0 ↔ a ≠ 1

Full source

@[to_additive enorm_ne_zero]
lemma enorm_ne_zero' {a : E} : ‖a‖ₑ‖a‖ₑ ≠ 0‖a‖ₑ ≠ 0 ↔ a ≠ 1 :=
  enorm_eq_zero'.ne

Nonzero Extended Norm Characterizes Non-Identity Elements

Informal description

For any element $a$ in an enormed monoid $E$, the extended norm $\|a\|_e$ is nonzero if and only if $a$ is not the identity element of the monoid, i.e., $\|a\|_e \neq 0 \leftrightarrow a \neq 1$.

enorm_pos' theorem

{a : E} : 0 < ‖a‖ₑ ↔ a ≠ 1

Full source

@[to_additive (attr := simp) enorm_pos]
lemma enorm_pos' {a : E} : 0 < ‖a‖ₑ ↔ a ≠ 1 :=
  pos_iff_ne_zero.trans enorm_ne_zero'

Positivity of Extended Norm Characterizes Non-Identity Elements

Informal description

For any element $a$ in an enormed monoid $E$, the extended norm $\|a\|_e$ is strictly positive if and only if $a$ is not the identity element of the monoid, i.e., $0 < \|a\|_e \leftrightarrow a \neq 1$.

instENormedAddCommMonoidENNReal instance

: ENormedAddCommMonoid ℝ≥0∞

Full source

instance : ENormedAddCommMonoid ℝ≥0∞ where
  continuous_enorm := continuous_id
  enorm_eq_zero := by simp
  enorm_add_le := by simp

The Enormed Additive Commutative Monoid Structure on Extended Nonnegative Reals

Informal description

The extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ form an enormed additive commutative monoid, where the addition operation is commutative and the topology is compatible with the extended norm structure.

SeminormedGroup.disjoint_nhds theorem

(x : E) (f : Filter E) : Disjoint (𝓝 x) f ↔ ∃ δ > 0, ∀ᶠ y in f, δ ≤ ‖y / x‖

Full source

@[to_additive]
lemma SeminormedGroup.disjoint_nhds (x : E) (f : Filter E) :
    DisjointDisjoint (𝓝 x) f ↔ ∃ δ > 0, ∀ᶠ y in f, δ ≤ ‖y / x‖ := by
  simp [NormedCommGroup.nhds_basis_norm_lt x |>.disjoint_iff_left, compl_setOf, eventually_iff]

Disjointness Criterion for Neighborhood Filters in Seminormed Groups

Informal description

Let $E$ be a seminormed group. For any element $x \in E$ and any filter $f$ on $E$, the neighborhood filter $\mathcal{N}(x)$ is disjoint from $f$ if and only if there exists $\delta > 0$ such that for eventually all $y$ in $f$, the norm of $y / x$ is at least $\delta$, i.e., $\delta \leq \|y / x\|$.

SeminormedGroup.disjoint_nhds_one theorem

(f : Filter E) : Disjoint (𝓝 1) f ↔ ∃ δ > 0, ∀ᶠ y in f, δ ≤ ‖y‖

Full source

@[to_additive]
lemma SeminormedGroup.disjoint_nhds_one (f : Filter E) :
    DisjointDisjoint (𝓝 1) f ↔ ∃ δ > 0, ∀ᶠ y in f, δ ≤ ‖y‖ := by
  simpa using disjoint_nhds 1 f

Disjointness Criterion for Identity Neighborhood Filter in Seminormed Groups: $\mathcal{N}(1) \perp f \leftrightarrow \exists \delta > 0, \forall^\ast y \in f, \delta \leq \|y\|$

Informal description

Let $E$ be a seminormed group. For any filter $f$ on $E$, the neighborhood filter of the identity element $\mathcal{N}(1)$ is disjoint from $f$ if and only if there exists $\delta > 0$ such that for eventually all $y$ in $f$, the norm of $y$ is at least $\delta$, i.e., $\delta \leq \|y\|$.

SeminormedGroup.induced abbrev

[Group E] [SeminormedGroup F] [MonoidHomClass 𝓕 E F] (f : 𝓕) : SeminormedGroup E

Full source

/-- A group homomorphism from a `Group` to a `SeminormedGroup` induces a `SeminormedGroup`
structure on the domain. -/
@[to_additive "A group homomorphism from an `AddGroup` to a
`SeminormedAddGroup` induces a `SeminormedAddGroup` structure on the domain."]
abbrev SeminormedGroup.induced [Group E] [SeminormedGroup F] [MonoidHomClass 𝓕 E F] (f : 𝓕) :
    SeminormedGroup E :=
  { PseudoMetricSpace.induced f toPseudoMetricSpace with
    norm := fun x => ‖f x‖
    dist_eq := fun x y => by simp only [map_div, ← dist_eq_norm_div]; rfl }

Induced Seminormed Group via Monoid Homomorphism

Informal description

Given a group $E$, a seminormed group $F$, and a monoid homomorphism class $\mathcal{F}$ from $E$ to $F$, any homomorphism $f \in \mathcal{F}$ induces a seminormed group structure on $E$ where the distance between elements $x, y \in E$ is defined as $\|f(x) / f(y)\|$.

SeminormedCommGroup.induced abbrev

[CommGroup E] [SeminormedGroup F] [MonoidHomClass 𝓕 E F] (f : 𝓕) : SeminormedCommGroup E

Full source

/-- A group homomorphism from a `CommGroup` to a `SeminormedGroup` induces a
`SeminormedCommGroup` structure on the domain. -/
@[to_additive "A group homomorphism from an `AddCommGroup` to a
`SeminormedAddGroup` induces a `SeminormedAddCommGroup` structure on the domain."]
abbrev SeminormedCommGroup.induced
    [CommGroup E] [SeminormedGroup F] [MonoidHomClass 𝓕 E F] (f : 𝓕) :
    SeminormedCommGroup E :=
  { SeminormedGroup.induced E F f with
    mul_comm := mul_comm }

Induced Seminormed Commutative Group via Monoid Homomorphism

Informal description

Given a commutative group $E$, a seminormed group $F$, and a monoid homomorphism class $\mathcal{F}$ from $E$ to $F$, any homomorphism $f \in \mathcal{F}$ induces a seminormed commutative group structure on $E$ where the distance between elements $x, y \in E$ is defined as $\|f(x) / f(y)\|$.

NormedGroup.induced abbrev

[Group E] [NormedGroup F] [MonoidHomClass 𝓕 E F] (f : 𝓕) (h : Injective f) : NormedGroup E

Full source

/-- An injective group homomorphism from a `Group` to a `NormedGroup` induces a `NormedGroup`
structure on the domain. -/
@[to_additive "An injective group homomorphism from an `AddGroup` to a
`NormedAddGroup` induces a `NormedAddGroup` structure on the domain."]
abbrev NormedGroup.induced
    [Group E] [NormedGroup F] [MonoidHomClass 𝓕 E F] (f : 𝓕) (h : Injective f) :
    NormedGroup E :=
  { SeminormedGroup.induced E F f, MetricSpace.induced f h _ with }

Induced Normed Group Structure via Injective Monoid Homomorphism

Informal description

Let $E$ be a group and $F$ a normed group. Given an injective monoid homomorphism $f \colon E \to F$, the group $E$ can be endowed with a normed group structure where the distance between elements $x, y \in E$ is defined as $\|f(x) / f(y)\|$.

NormedCommGroup.induced abbrev

[CommGroup E] [NormedGroup F] [MonoidHomClass 𝓕 E F] (f : 𝓕) (h : Injective f) : NormedCommGroup E

Full source

/-- An injective group homomorphism from a `CommGroup` to a `NormedGroup` induces a
`NormedCommGroup` structure on the domain. -/
@[to_additive "An injective group homomorphism from a `CommGroup` to a
`NormedCommGroup` induces a `NormedCommGroup` structure on the domain."]
abbrev NormedCommGroup.induced [CommGroup E] [NormedGroup F] [MonoidHomClass 𝓕 E F] (f : 𝓕)
    (h : Injective f) : NormedCommGroup E :=
  { SeminormedGroup.induced E F f, MetricSpace.induced f h _ with
    mul_comm := mul_comm }

Induced Normed Commutative Group via Injective Homomorphism

Informal description

Let $E$ be a commutative group and $F$ a normed group. Given an injective group homomorphism $f \colon E \to F$ (where $f$ belongs to a monoid homomorphism class $\mathcal{F}$), the group $E$ can be endowed with a normed commutative group structure where the distance between elements $x, y \in E$ is defined as $\|f(x) / f(y)\|$.

Real.norm instance

: Norm ℝ

Full source

instance norm : Norm ℝ where
  norm r := |r|

The Norm Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ are endowed with a norm structure, where the norm of a real number $x$ is given by its absolute value $\|x\| = |x|$.

Real.norm_eq_abs theorem

(r : ℝ) : ‖r‖ = |r|

Full source

@[simp]
theorem norm_eq_abs (r : ℝ) : ‖r‖ = |r| :=
  rfl

Norm Equals Absolute Value in Real Numbers

Informal description

For any real number $r$, its norm $\|r\|$ is equal to its absolute value $|r|$.

Real.normedAddCommGroup instance

: NormedAddCommGroup ℝ

Full source

instance normedAddCommGroup : NormedAddCommGroup ℝ :=
  ⟨fun _r _y => rfl⟩

The Normed Additive Commutative Group Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ form a normed additive commutative group, where the norm of a real number $x$ is given by its absolute value $\|x\| = |x|$ and the distance between two real numbers $x$ and $y$ is given by $\|x - y\|$.

Real.norm_of_nonneg theorem

(hr : 0 ≤ r) : ‖r‖ = r

Full source

theorem norm_of_nonneg (hr : 0 ≤ r) : ‖r‖ = r :=
  abs_of_nonneg hr

Norm of Nonnegative Real Number Equals Itself

Informal description

For any real number $r$ such that $r \geq 0$, the norm of $r$ equals $r$, i.e., $\|r\| = r$.

Real.norm_of_nonpos theorem

(hr : r ≤ 0) : ‖r‖ = -r

Full source

theorem norm_of_nonpos (hr : r ≤ 0) : ‖r‖ = -r :=
  abs_of_nonpos hr

Norm of Nonpositive Real Number: $\|r\| = -r$ for $r \leq 0$

Informal description

For any real number $r$ such that $r \leq 0$, the norm of $r$ is equal to $-r$, i.e., $\|r\| = -r$.

Real.le_norm_self theorem

(r : ℝ) : r ≤ ‖r‖

Full source

theorem le_norm_self (r : ℝ) : r ≤ ‖r‖ :=
  le_abs_self r

Self-Norm Lower Bound: $r \leq \|r\|$ for Real Numbers

Informal description

For any real number $r$, we have $r \leq \|r\|$, where $\|r\|$ denotes the norm of $r$.

Real.norm_natCast theorem

(n : ℕ) : ‖(n : ℝ)‖ = n

Full source

@[simp 1100] lemma norm_natCast (n : ℕ) : ‖(n : ℝ)‖ = n := abs_of_nonneg n.cast_nonneg

Norm of Natural Number Cast: $\|n\| = n$ for $n \in \mathbb{N}$

Informal description

For any natural number $n$, the norm of its canonical embedding in the real numbers is equal to $n$ itself, i.e., $\|(n : \mathbb{R})\| = n$.

Real.nnnorm_natCast theorem

(n : ℕ) : ‖(n : ℝ)‖₊ = n

Full source

@[simp 1100] lemma nnnorm_natCast (n : ℕ) : ‖(n : ℝ)‖₊ = n := NNReal.eq <| norm_natCast _

Nonnegative Norm of Natural Number Cast: $\|n\|_{\mathbb{R}_{\geq 0}} = n$

Informal description

For any natural number $n$, the nonnegative norm of its canonical embedding in the real numbers is equal to $n$ itself, i.e., $\|(n : \mathbb{R})\|_{\mathbb{R}_{\geq 0}} = n$.

Real.enorm_natCast theorem

(n : ℕ) : ‖(n : ℝ)‖ₑ = n

Full source

@[simp 1100] lemma enorm_natCast (n : ℕ) : ‖(n : ℝ)‖ₑ = n := by simp [enorm]

Extended Norm of Natural Number Cast: $\|n\|_e = n$

Informal description

For any natural number $n$, the extended norm of its canonical embedding in the real numbers is equal to $n$ itself, i.e., $\|(n : \mathbb{R})\|_e = n$.

Real.norm_ofNat theorem

(n : ℕ) [n.AtLeastTwo] : ‖(ofNat(n) : ℝ)‖ = ofNat(n)

Full source

@[simp 1100] lemma norm_ofNat (n : ℕ) [n.AtLeastTwo] :
    ‖(ofNat(n) : ℝ)‖ = ofNat(n) := norm_natCast n

Norm of Numerals $\geq 2$ in Real Numbers: $\|n\| = n$ for $n \geq 2$

Informal description

For any natural number $n \geq 2$, the norm of its canonical embedding in the real numbers is equal to $n$ itself, i.e., $\|n\| = n$.

Real.nnnorm_ofNat theorem

(n : ℕ) [n.AtLeastTwo] : ‖(ofNat(n) : ℝ)‖₊ = ofNat(n)

Full source

@[simp 1100] lemma nnnorm_ofNat (n : ℕ) [n.AtLeastTwo] :
    ‖(ofNat(n) : ℝ)‖₊ = ofNat(n) := nnnorm_natCast n

Nonnegative Norm of Numerals $\geq 2$ in Real Numbers: $\|n\|_{\mathbb{R}_{\geq 0}} = n$ for $n \geq 2$

Informal description

For any natural number $n \geq 2$, the nonnegative norm of its canonical embedding in the real numbers is equal to $n$ itself, i.e., $\|n\|_{\mathbb{R}_{\geq 0}} = n$.

Real.norm_two theorem

: ‖(2 : ℝ)‖ = 2

Full source

lemma norm_two : ‖(2 : ℝ)‖ = 2 := abs_of_pos zero_lt_two

Norm of Two in Real Numbers: $\|2\| = 2$

Informal description

The norm of the real number $2$ is equal to $2$, i.e., $\|2\| = 2$.

Real.nnnorm_two theorem

: ‖(2 : ℝ)‖₊ = 2

Full source

lemma nnnorm_two : ‖(2 : ℝ)‖₊ = 2 := NNReal.eq <| by simp

Nonnegative Norm of Two: $\|2\|_{\mathbb{R}_{\geq 0}} = 2$

Informal description

The nonnegative norm of the real number $2$ is equal to $2$, i.e., $\|2\|_{\mathbb{R}_{\geq 0}} = 2$.

Real.norm_nnratCast theorem

(q : ℚ≥0) : ‖(q : ℝ)‖ = q

Full source

@[simp 1100, norm_cast]
lemma norm_nnratCast (q : ℚ≥0) : ‖(q : ℝ)‖ = q := norm_of_nonneg q.cast_nonneg

Norm of Nonnegative Rational Cast: $\|q\| = q$

Informal description

For any nonnegative rational number $q \in \mathbb{Q}_{\geq 0}$, the norm of its canonical embedding into the real numbers equals $q$, i.e., $\|q\| = q$.

Real.nnnorm_nnratCast theorem

(q : ℚ≥0) : ‖(q : ℝ)‖₊ = q

Full source

@[simp 1100, norm_cast]
lemma nnnorm_nnratCast (q : ℚ≥0) : ‖(q : ℝ)‖₊ = q := by simp [nnnorm, -norm_eq_abs]

Nonnegative Norm Identity for Nonnegative Rationals: $\|q\|_{\mathbb{R}_{\geq 0}} = q$

Informal description

For any nonnegative rational number $q \in \mathbb{Q}_{\geq 0}$, the nonnegative norm of its canonical embedding into the real numbers equals $q$, i.e., $\|q\|_{\mathbb{R}_{\geq 0}} = q$.

Real.nnnorm_of_nonneg theorem

(hr : 0 ≤ r) : ‖r‖₊ = ⟨r, hr⟩

Full source

theorem nnnorm_of_nonneg (hr : 0 ≤ r) : ‖r‖₊ = ⟨r, hr⟩ :=
  NNReal.eq <| norm_of_nonneg hr

Nonnegative Norm of Nonnegative Real Number Equals Its Canonical Embedding

Informal description

For any real number $r$ such that $r \geq 0$, the nonnegative norm of $r$ is equal to the pair $\langle r, hr \rangle$, where $hr$ is the proof that $r \geq 0$.

Real.enorm_of_nonneg theorem

(hr : 0 ≤ r) : ‖r‖ₑ = .ofReal r

Full source

lemma enorm_of_nonneg (hr : 0 ≤ r) : ‖r‖ₑ = .ofReal r := by
  simp [enorm, nnnorm_of_nonneg hr, ENNReal.ofReal, toNNReal, hr]

Extended Norm of Nonnegative Real Number Equals Its Embedding

Informal description

For any real number $r$ such that $r \geq 0$, the extended norm $\|r\|_e$ is equal to the extended nonnegative real number obtained by embedding $r$ via the `ofReal` function.

Real.nnnorm_abs theorem

(r : ℝ) : ‖|r|‖₊ = ‖r‖₊

Full source

@[simp] lemma nnnorm_abs (r : ℝ) : ‖|r|‖₊ = ‖r‖₊ := by simp [nnnorm]

Nonnegative Norm of Absolute Value Equals Nonnegative Norm

Informal description

For any real number $r$, the nonnegative norm of the absolute value of $r$ is equal to the nonnegative norm of $r$, i.e., $\||r|\|₊ = \|r\|₊$.

Real.enorm_abs theorem

(r : ℝ) : ‖|r|‖ₑ = ‖r‖ₑ

Full source

@[simp] lemma enorm_abs (r : ℝ) : ‖|r|‖ₑ = ‖r‖ₑ := by simp [enorm]

Extended Norm of Absolute Value Equals Extended Norm for Real Numbers

Informal description

For any real number $r$, the extended norm of the absolute value of $r$ is equal to the extended norm of $r$, i.e., $\||r|\|_e = \|r\|_e$.

Real.enorm_eq_ofReal theorem

(hr : 0 ≤ r) : ‖r‖ₑ = .ofReal r

Full source

theorem enorm_eq_ofReal (hr : 0 ≤ r) : ‖r‖ₑ = .ofReal r := by
  rw [← ofReal_norm_eq_enorm, norm_of_nonneg hr]

Extended Norm of Nonnegative Real Equals Its Embedding

Informal description

For any real number $r$ such that $r \geq 0$, the extended norm $\|r\|_e$ equals the extended nonnegative real embedding of $r$, i.e., $\|r\|_e = \text{ofReal}(r)$.

Real.enorm_eq_ofReal_abs theorem

(r : ℝ) : ‖r‖ₑ = ENNReal.ofReal |r|

Full source

theorem enorm_eq_ofReal_abs (r : ℝ) : ‖r‖ₑ = ENNReal.ofReal |r| := by
  rw [← enorm_eq_ofReal (abs_nonneg _), enorm_abs]

Extended Norm Equals Embedding of Absolute Value for Real Numbers

Informal description

For any real number $r$, the extended norm $\|r\|_e$ is equal to the extended nonnegative real embedding of the absolute value of $r$, i.e., $\|r\|_e = \text{ofReal}(|r|)$.

Real.toNNReal_eq_nnnorm_of_nonneg theorem

(hr : 0 ≤ r) : r.toNNReal = ‖r‖₊

Full source

theorem toNNReal_eq_nnnorm_of_nonneg (hr : 0 ≤ r) : r.toNNReal = ‖r‖₊ := by
  rw [Real.toNNReal_of_nonneg hr]
  ext
  rw [coe_mk, coe_nnnorm r, Real.norm_eq_abs r, abs_of_nonneg hr]

Non-negative Real Conversion Equals Non-negative Norm for Non-negative Reals

Informal description

For any real number $r$ such that $r \geq 0$, the canonical conversion of $r$ to a non-negative real number equals its non-negative norm, i.e., $\text{toNNReal}(r) = \|r\|₊$.

Real.ofReal_le_enorm theorem

(r : ℝ) : ENNReal.ofReal r ≤ ‖r‖ₑ

Full source

theorem ofReal_le_enorm (r : ℝ) : ENNReal.ofReal r ≤ ‖r‖ₑ := by
  rw [enorm_eq_ofReal_abs]; gcongr; exact le_abs_self _

Extended Nonnegative Real Embedding Bounded by Extended Norm

Informal description

For any real number $r$, the extended nonnegative real number obtained by applying the `ENNReal.ofReal` function to $r$ is less than or equal to the extended norm of $r$, i.e., $\text{ofReal}(r) \leq \|r\|_e$.

NNReal.instNNNorm instance

: NNNorm ℝ≥0

Full source

instance : NNNorm ℝ≥0 where
  nnnorm x := x

Non-negative Norm Structure on Non-negative Reals

Informal description

The non-negative real numbers $\mathbb{R}_{\geq 0}$ are equipped with a canonical non-negative norm structure, where the norm of an element $x$ is $x$ itself.

NNReal.nnnorm_eq_self theorem

(x : ℝ≥0) : ‖x‖₊ = x

Full source

@[simp] lemma nnnorm_eq_self (x : ℝ≥0) : ‖x‖₊ = x := rfl

Non-negative Norm Equals Itself on Non-negative Reals

Informal description

For any non-negative real number $x \in \mathbb{R}_{\geq 0}$, the non-negative norm $\|x\|_{\!+}$ is equal to $x$ itself.

dist_inv theorem

(x y : E) : dist x⁻¹ y = dist x y⁻¹

Full source

@[to_additive]
theorem dist_inv (x y : E) : dist x⁻¹ y = dist x y⁻¹ := by
  simp_rw [dist_eq_norm_div, ← norm_inv' (x⁻¹ / y), inv_div, div_inv_eq_mul, mul_comm]

Distance Invariance under Inversion: $\text{dist}(x^{-1}, y) = \text{dist}(x, y^{-1})$

Informal description

For any elements $x$ and $y$ in a seminormed group $E$, the distance between $x^{-1}$ and $y$ is equal to the distance between $x$ and $y^{-1}$, i.e., $\text{dist}(x^{-1}, y) = \text{dist}(x, y^{-1})$.

norm_multiset_sum_le theorem

{E} [SeminormedAddCommGroup E] (m : Multiset E) : ‖m.sum‖ ≤ (m.map fun x => ‖x‖).sum

Full source

theorem norm_multiset_sum_le {E} [SeminormedAddCommGroup E] (m : Multiset E) :
    ‖m.sum‖ ≤ (m.map fun x => ‖x‖).sum :=
  m.le_sum_of_subadditive norm norm_zero norm_add_le

Norm of Multiset Sum is Bounded by Sum of Norms

Informal description

Let $E$ be a seminormed additive commutative group. For any multiset $m$ of elements in $E$, the norm of the sum of the elements in $m$ is less than or equal to the sum of the norms of the elements in $m$, i.e., \[ \left\| \sum_{x \in m} x \right\| \leq \sum_{x \in m} \|x\|. \]

norm_multiset_prod_le theorem

(m : Multiset E) : ‖m.prod‖ ≤ (m.map fun x => ‖x‖).sum

Full source

@[to_additive existing]
theorem norm_multiset_prod_le (m : Multiset E) : ‖m.prod‖ ≤ (m.map fun x => ‖x‖).sum := by
  rw [← Multiplicative.ofAdd_le, ofAdd_multiset_prod, Multiset.map_map]
  refine Multiset.le_prod_of_submultiplicative (Multiplicative.ofAddMultiplicative.ofAdd ∘ norm) ?_ (fun x y => ?_) _
  · simp only [comp_apply, norm_one', ofAdd_zero]
  · exact norm_mul_le' x y

Norm of Multiset Product Bounded by Sum of Norms

Informal description

For any multiset $m$ of elements in a seminormed commutative group $E$, the norm of the product of all elements in $m$ is less than or equal to the sum of the norms of the elements in $m$, i.e., \[ \left\| \prod_{x \in m} x \right\| \leq \sum_{x \in m} \|x\|. \]

norm_sum_le theorem

{ι E} [SeminormedAddCommGroup E] (s : Finset ι) (f : ι → E) : ‖∑ i ∈ s, f i‖ ≤ ∑ i ∈ s, ‖f i‖

Full source

@[bound]
theorem norm_sum_le {ι E} [SeminormedAddCommGroup E] (s : Finset ι) (f : ι → E) :
    ‖∑ i ∈ s, f i‖ ≤ ∑ i ∈ s, ‖f i‖ :=
  s.le_sum_of_subadditive norm norm_zero norm_add_le f

Norm of Sum is Bounded by Sum of Norms in Seminormed Additive Commutative Groups

Informal description

Let $E$ be a seminormed additive commutative group and let $s$ be a finite set indexed by $\iota$. For any function $f \colon \iota \to E$, the norm of the sum of $f$ over $s$ is bounded by the sum of the norms of $f$ over $s$, i.e., \[ \left\|\sum_{i \in s} f(i)\right\| \leq \sum_{i \in s} \|f(i)\|. \]

norm_prod_le theorem

(s : Finset ι) (f : ι → E) : ‖∏ i ∈ s, f i‖ ≤ ∑ i ∈ s, ‖f i‖

Full source

@[to_additive existing]
theorem norm_prod_le (s : Finset ι) (f : ι → E) : ‖∏ i ∈ s, f i‖ ≤ ∑ i ∈ s, ‖f i‖ := by
  rw [← Multiplicative.ofAdd_le, ofAdd_sum]
  refine Finset.le_prod_of_submultiplicative (Multiplicative.ofAddMultiplicative.ofAdd ∘ norm) ?_ (fun x y => ?_) _ _
  · simp only [comp_apply, norm_one', ofAdd_zero]
  · exact norm_mul_le' x y

Norm of Product Bounded by Sum of Norms in Seminormed Commutative Groups

Informal description

For any finite set $s$ and any family of elements $(f_i)_{i \in s}$ in a seminormed commutative group $E$, the norm of the product of the elements is bounded by the sum of their norms: \[ \left\|\prod_{i \in s} f_i\right\| \leq \sum_{i \in s} \|f_i\|. \]

norm_prod_le_of_le theorem

 (s : Finset ι) {f : ι → E} {n : ι → ℝ} (h : ∀ b ∈ s, ‖f b‖ ≤ n b) : ‖∏ b ∈ s, f b‖ ≤ ∑ b ∈ s, n b

Full source

@[to_additive]
theorem norm_prod_le_of_le (s : Finset ι) {f : ι → E} {n : ι → ℝ} (h : ∀ b ∈ s, ‖f b‖ ≤ n b) :
    ‖∏ b ∈ s, f b‖ ≤ ∑ b ∈ s, n b :=
  (norm_prod_le s f).trans <| Finset.sum_le_sum h

Norm of Product Bounded by Sum of Element-wise Bounds in Seminormed Commutative Groups

Informal description

For any finite set $s$ and any family of elements $(f_i)_{i \in s}$ in a seminormed commutative group $E$, if each element $f_i$ satisfies $\|f_i\| \leq n_i$ for some real numbers $(n_i)_{i \in s}$, then the norm of the product of the elements is bounded by the sum of the $n_i$: \[ \left\|\prod_{i \in s} f_i\right\| \leq \sum_{i \in s} n_i. \]

dist_prod_prod_le_of_le theorem

 (s : Finset ι) {f a : ι → E} {d : ι → ℝ} (h : ∀ b ∈ s, dist (f b) (a b) ≤ d b) :
  dist (∏ b ∈ s, f b) (∏ b ∈ s, a b) ≤ ∑ b ∈ s, d b

Full source

@[to_additive]
theorem dist_prod_prod_le_of_le (s : Finset ι) {f a : ι → E} {d : ι → ℝ}
    (h : ∀ b ∈ s, dist (f b) (a b) ≤ d b) :
    dist (∏ b ∈ s, f b) (∏ b ∈ s, a b) ≤ ∑ b ∈ s, d b := by
  simp only [dist_eq_norm_div, ← Finset.prod_div_distrib] at *
  exact norm_prod_le_of_le s h

Distance Between Products Bounded by Sum of Component-wise Distances in Seminormed Commutative Groups

Informal description

For any finite set $s$ and any families of elements $(f_i)_{i \in s}$ and $(a_i)_{i \in s}$ in a seminormed commutative group $E$, if for each $i \in s$ the distance between $f_i$ and $a_i$ satisfies $\text{dist}(f_i, a_i) \leq d_i$ for some real numbers $(d_i)_{i \in s}$, then the distance between the products $\prod_{i \in s} f_i$ and $\prod_{i \in s} a_i$ is bounded by the sum of the $d_i$: \[ \text{dist}\left(\prod_{i \in s} f_i, \prod_{i \in s} a_i\right) \leq \sum_{i \in s} d_i. \]

dist_prod_prod_le theorem

(s : Finset ι) (f a : ι → E) : dist (∏ b ∈ s, f b) (∏ b ∈ s, a b) ≤ ∑ b ∈ s, dist (f b) (a b)

Full source

@[to_additive]
theorem dist_prod_prod_le (s : Finset ι) (f a : ι → E) :
    dist (∏ b ∈ s, f b) (∏ b ∈ s, a b) ≤ ∑ b ∈ s, dist (f b) (a b) :=
  dist_prod_prod_le_of_le s fun _ _ => le_rfl

Distance Between Products Bounded by Sum of Component-wise Distances in Seminormed Commutative Groups

Informal description

For any finite set $s$ and any families of elements $(f_i)_{i \in s}$ and $(a_i)_{i \in s}$ in a seminormed commutative group $E$, the distance between the products $\prod_{i \in s} f_i$ and $\prod_{i \in s} a_i$ is bounded by the sum of the distances between corresponding elements: \[ \text{dist}\left(\prod_{i \in s} f_i, \prod_{i \in s} a_i\right) \leq \sum_{i \in s} \text{dist}(f_i, a_i). \]

mul_mem_ball_iff_norm theorem

: a * b ∈ ball a r ↔ ‖b‖ < r

Full source

@[to_additive]
theorem mul_mem_ball_iff_norm : a * b ∈ ball a ra * b ∈ ball a r ↔ ‖b‖ < r := by
  rw [mem_ball_iff_norm'', mul_div_cancel_left]

Product Membership in Open Ball via Norm: $a * b \in \text{ball}(a, r) \leftrightarrow \|b\| < r$

Informal description

For any elements $a$ and $b$ in a seminormed group $E$ and any positive real number $r$, the product $a * b$ belongs to the open ball centered at $a$ with radius $r$ if and only if the norm of $b$ is less than $r$, i.e., \[ a * b \in \text{ball}(a, r) \leftrightarrow \|b\| < r. \]

mul_mem_closedBall_iff_norm theorem

: a * b ∈ closedBall a r ↔ ‖b‖ ≤ r

Full source

@[to_additive]
theorem mul_mem_closedBall_iff_norm : a * b ∈ closedBall a ra * b ∈ closedBall a r ↔ ‖b‖ ≤ r := by
  rw [mem_closedBall_iff_norm'', mul_div_cancel_left]

Closed Ball Membership Criterion via Norm under Left Multiplication: $a \cdot b \in \overline{B}(a, r) \leftrightarrow \|b\| \leq r$

Informal description

For any elements $a, b$ in a seminormed group $E$ and any non-negative real number $r$, the product $a \cdot b$ belongs to the closed ball centered at $a$ with radius $r$ if and only if the norm of $b$ is less than or equal to $r$, i.e., $a \cdot b \in \overline{B}(a, r) \leftrightarrow \|b\| \leq r$.

preimage_mul_ball theorem

(a b : E) (r : ℝ) : (b * ·) ⁻¹' ball a r = ball (a / b) r

Full source

@[to_additive (attr := simp 1001)]
-- Porting note: increase priority so that the left-hand side doesn't simplify
theorem preimage_mul_ball (a b : E) (r : ℝ) : (b * ·) ⁻¹' ball a r = ball (a / b) r := by
  ext c
  simp only [dist_eq_norm_div, Set.mem_preimage, mem_ball, div_div_eq_mul_div, mul_comm]

Preimage of Open Ball under Left Multiplication in Seminormed Groups

Informal description

For any elements $a, b$ in a seminormed group $E$ and any positive real number $r$, the preimage of the open ball $\text{ball}(a, r)$ under the left multiplication map $x \mapsto b \cdot x$ is equal to the open ball $\text{ball}(a / b, r)$. In other words, $$ (b \cdot \cdot)^{-1}(\text{ball}(a, r)) = \text{ball}(a / b, r). $$

preimage_mul_closedBall theorem

(a b : E) (r : ℝ) : (b * ·) ⁻¹' closedBall a r = closedBall (a / b) r

Full source

@[to_additive (attr := simp 1001)]
-- Porting note: increase priority so that the left-hand side doesn't simplify
theorem preimage_mul_closedBall (a b : E) (r : ℝ) :
    (b * ·) ⁻¹' closedBall a r = closedBall (a / b) r := by
  ext c
  simp only [dist_eq_norm_div, Set.mem_preimage, mem_closedBall, div_div_eq_mul_div, mul_comm]

Preimage of Closed Ball under Left Multiplication in Seminormed Groups

Informal description

For any elements $a, b$ in a seminormed group $E$ and any non-negative real number $r$, the preimage of the closed ball $\overline{B}(a, r)$ under the left multiplication map $x \mapsto b \cdot x$ is equal to the closed ball $\overline{B}(a / b, r)$. In other words, $$ (b \cdot \cdot)^{-1}(\overline{B}(a, r)) = \overline{B}(a / b, r). $$

preimage_mul_sphere theorem

(a b : E) (r : ℝ) : (b * ·) ⁻¹' sphere a r = sphere (a / b) r

Full source

@[to_additive (attr := simp)]
theorem preimage_mul_sphere (a b : E) (r : ℝ) : (b * ·) ⁻¹' sphere a r = sphere (a / b) r := by
  ext c
  simp only [Set.mem_preimage, mem_sphere_iff_norm', div_div_eq_mul_div, mul_comm]

Preimage of Sphere under Left Multiplication in Seminormed Commutative Groups

Informal description

For any elements $a, b$ in a seminormed commutative group $E$ and any non-negative real number $r$, the preimage of the sphere $\{x \in E \mid \|x - a\| = r\}$ under the left multiplication map $x \mapsto b \cdot x$ is equal to the sphere $\{x \in E \mid \|x - (a / b)\| = r\}$. In other words, $$ (b \cdot \cdot)^{-1}(\{x \in E \mid \|x - a\| = r\}) = \{x \in E \mid \|x - (a / b)\| = r\}. $$

pow_mem_closedBall theorem

{n : ℕ} (h : a ∈ closedBall b r) : a ^ n ∈ closedBall (b ^ n) (n • r)

Full source

@[to_additive]
theorem pow_mem_closedBall {n : ℕ} (h : a ∈ closedBall b r) :
    a ^ n ∈ closedBall (b ^ n) (n • r) := by
  simp only [mem_closedBall, dist_eq_norm_div, ← div_pow] at h ⊢
  refine norm_pow_le_mul_norm.trans ?_
  simpa only [nsmul_eq_mul] using mul_le_mul_of_nonneg_left h n.cast_nonneg

Powers Preserve Closed Ball Membership: $a \in \overline{B}(b, r) \implies a^n \in \overline{B}(b^n, n \cdot r)$

Informal description

For any natural number $n$ and elements $a, b$ in a seminormed commutative group $E$, if $a$ belongs to the closed ball $\overline{B}(b, r)$ centered at $b$ with radius $r$, then the $n$-th power $a^n$ belongs to the closed ball $\overline{B}(b^n, n \cdot r)$ centered at $b^n$ with radius $n \cdot r$.

pow_mem_ball theorem

{n : ℕ} (hn : 0 < n) (h : a ∈ ball b r) : a ^ n ∈ ball (b ^ n) (n • r)

Full source

@[to_additive]
theorem pow_mem_ball {n : ℕ} (hn : 0 < n) (h : a ∈ ball b r) : a ^ n ∈ ball (b ^ n) (n • r) := by
  simp only [mem_ball, dist_eq_norm_div, ← div_pow] at h ⊢
  refine lt_of_le_of_lt norm_pow_le_mul_norm ?_
  replace hn : 0 < (n : ℝ) := by norm_cast
  rw [nsmul_eq_mul]
  nlinarith

Powers Preserve Open Ball Membership in Seminormed Commutative Groups

Informal description

For any elements $a, b$ in a seminormed commutative group $E$, any positive natural number $n > 0$, and any positive real number $r > 0$, if $a$ belongs to the open ball centered at $b$ with radius $r$, then the $n$-th power $a^n$ belongs to the open ball centered at $b^n$ with radius $n \cdot r$. In other words: $$a \in B(b, r) \implies a^n \in B(b^n, n \cdot r).$$

mul_mem_closedBall_mul_iff theorem

{c : E} : a * c ∈ closedBall (b * c) r ↔ a ∈ closedBall b r

Full source

@[to_additive]
theorem mul_mem_closedBall_mul_iff {c : E} : a * c ∈ closedBall (b * c) ra * c ∈ closedBall (b * c) r ↔ a ∈ closedBall b r := by
  simp only [mem_closedBall, dist_eq_norm_div, mul_div_mul_right_eq_div]

Multiplication Preserves Closed Ball Membership in Seminormed Commutative Groups

Informal description

For any elements $a, b, c$ in a seminormed commutative group $E$ and any non-negative real number $r$, the product $a \cdot c$ belongs to the closed ball centered at $b \cdot c$ with radius $r$ if and only if $a$ belongs to the closed ball centered at $b$ with radius $r$. In other words: $$a \cdot c \in \overline{B}(b \cdot c, r) \leftrightarrow a \in \overline{B}(b, r)$$

mul_mem_ball_mul_iff theorem

{c : E} : a * c ∈ ball (b * c) r ↔ a ∈ ball b r

Full source

@[to_additive]
theorem mul_mem_ball_mul_iff {c : E} : a * c ∈ ball (b * c) ra * c ∈ ball (b * c) r ↔ a ∈ ball b r := by
  simp only [mem_ball, dist_eq_norm_div, mul_div_mul_right_eq_div]

Multiplication Preserves Open Ball Membership in Seminormed Commutative Groups

Informal description

For any elements $a, b, c$ in a seminormed commutative group $E$ and any positive real number $r$, the product $a \cdot c$ belongs to the open ball centered at $b \cdot c$ with radius $r$ if and only if $a$ belongs to the open ball centered at $b$ with radius $r$. In other words: $$a \cdot c \in B(b \cdot c, r) \leftrightarrow a \in B(b, r)$$

smul_closedBall'' theorem

: a • closedBall b r = closedBall (a • b) r

Full source

@[to_additive]
theorem smul_closedBall'' : a • closedBall b r = closedBall (a • b) r := by
  ext
  simp [mem_closedBall, Set.mem_smul_set, dist_eq_norm_div, div_eq_inv_mul, ←
    eq_inv_mul_iff_mul_eq, mul_assoc]

Scalar Multiplication Preserves Closed Balls in Seminormed Commutative Groups

Informal description

For any element $a$ in a seminormed commutative group $E$, any element $b \in E$, and any non-negative real number $r$, the left scalar multiplication of $a$ on the closed ball centered at $b$ with radius $r$ is equal to the closed ball centered at $a \cdot b$ with radius $r$, i.e., $a \cdot \overline{B}(b, r) = \overline{B}(a \cdot b, r)$.

smul_ball'' theorem

: a • ball b r = ball (a • b) r

Full source

@[to_additive]
theorem smul_ball'' : a • ball b r = ball (a • b) r := by
  ext
  simp [mem_ball, Set.mem_smul_set, dist_eq_norm_div, _root_.div_eq_inv_mul,
    ← eq_inv_mul_iff_mul_eq, mul_assoc]

Scalar Multiplication Preserves Open Balls in Seminormed Commutative Groups

Informal description

For any element $a$ in a seminormed commutative group $E$, any element $b \in E$, and any positive real number $r$, the left scalar multiplication of $a$ on the open ball centered at $b$ with radius $r$ is equal to the open ball centered at $a \cdot b$ with radius $r$, i.e., $a \cdot \text{ball}(b, r) = \text{ball}(a \cdot b, r)$.

nnnorm_multiset_prod_le theorem

(m : Multiset E) : ‖m.prod‖₊ ≤ (m.map fun x => ‖x‖₊).sum

Full source

@[to_additive]
theorem nnnorm_multiset_prod_le (m : Multiset E) : ‖m.prod‖₊ ≤ (m.map fun x => ‖x‖₊).sum :=
  NNReal.coe_le_coe.1 <| by
    push_cast
    rw [Multiset.map_map]
    exact norm_multiset_prod_le _

Non-negative norm bound for multiset products in seminormed commutative groups

Informal description

For any multiset $m$ of elements in a seminormed commutative group $E$, the non-negative norm of the product of all elements in $m$ is less than or equal to the sum of the non-negative norms of the elements in $m$, i.e., \[ \left\| \prod_{x \in m} x \right\|₊ \leq \sum_{x \in m} \|x\|₊. \]

nnnorm_prod_le theorem

(s : Finset ι) (f : ι → E) : ‖∏ a ∈ s, f a‖₊ ≤ ∑ a ∈ s, ‖f a‖₊

Full source

@[to_additive]
theorem nnnorm_prod_le (s : Finset ι) (f : ι → E) : ‖∏ a ∈ s, f a‖₊ ≤ ∑ a ∈ s, ‖f a‖₊ :=
  NNReal.coe_le_coe.1 <| by
    push_cast
    exact norm_prod_le _ _

Non-negative norm of product bounded by sum of non-negative norms in seminormed commutative groups

Informal description

For any finite set $s$ and any family of elements $(f_i)_{i \in s}$ in a seminormed commutative group $E$, the non-negative norm of the product of the elements is bounded by the sum of their non-negative norms: \[ \left\|\prod_{i \in s} f_i\right\|₊ \leq \sum_{i \in s} \|f_i\|₊. \]

nnnorm_prod_le_of_le theorem

 (s : Finset ι) {f : ι → E} {n : ι → ℝ≥0} (h : ∀ b ∈ s, ‖f b‖₊ ≤ n b) : ‖∏ b ∈ s, f b‖₊ ≤ ∑ b ∈ s, n b

Full source

@[to_additive]
theorem nnnorm_prod_le_of_le (s : Finset ι) {f : ι → E} {n : ι → ℝ≥0} (h : ∀ b ∈ s, ‖f b‖₊ ≤ n b) :
    ‖∏ b ∈ s, f b‖₊ ≤ ∑ b ∈ s, n b :=
  (norm_prod_le_of_le s h).trans_eq (NNReal.coe_sum ..).symm

Non-negative norm of product bounded by sum of element-wise bounds in seminormed commutative groups

Informal description

For any finite set $s$ and any family of elements $(f_i)_{i \in s}$ in a seminormed commutative group $E$, if each element $f_i$ satisfies $\|f_i\|₊ \leq n_i$ for some non-negative real numbers $(n_i)_{i \in s}$, then the non-negative norm of the product of the elements is bounded by the sum of the $n_i$: \[ \left\|\prod_{i \in s} f_i\right\|₊ \leq \sum_{i \in s} n_i. \]

norm_norm' theorem

(x : E) : ‖‖x‖‖ = ‖x‖

Full source

@[to_additive (attr := simp 1001) norm_norm]
lemma norm_norm' (x : E) : ‖‖x‖‖ = ‖x‖ := Real.norm_of_nonneg (norm_nonneg' _)

Norm of Norm Equals Norm

Informal description

For any element $x$ in a seminormed group $E$, the norm of the norm of $x$ equals the norm of $x$, i.e., $\|\|x\|\| = \|x\|$.

nnnorm_norm' theorem

(x : E) : ‖‖x‖‖₊ = ‖x‖₊

Full source

@[to_additive (attr := simp) nnnorm_norm]
lemma nnnorm_norm' (x : E) : ‖‖x‖‖₊ = ‖x‖₊ := by simp [nnnorm]

Non-negative Norm Identity: $\|\|x\|\|₊ = \|x\|₊$

Informal description

For any element $x$ in a seminormed group $E$, the non-negative norm of the norm of $x$ equals the non-negative norm of $x$, i.e., $\|\|x\|\|₊ = \|x\|₊$.

enorm_norm' theorem

(x : E) : ‖‖x‖‖ₑ = ‖x‖ₑ

Full source

@[to_additive (attr := simp) enorm_norm]
lemma enorm_norm' (x : E) : ‖‖x‖‖ₑ = ‖x‖ₑ := by simp [enorm]

Extended Norm Identity: $\|\|x\|\|_e = \|x\|_e$

Informal description

For any element $x$ in a seminormed group $E$, the extended norm of the norm of $x$ equals the extended norm of $x$, i.e., $\|\|x\|\|_e = \|x\|_e$.

enorm_enorm theorem

{ε : Type*} [ENorm ε] (x : ε) : ‖‖x‖ₑ‖ₑ = ‖x‖ₑ

Full source

lemma enorm_enorm {ε : Type*} [ENorm ε] (x : ε) : ‖‖x‖ₑ‖ₑ = ‖x‖ₑ := by simp [enorm]

Extended Norm Idempotence: $\| \|x\|_e \|_e = \|x\|_e$

Informal description

For any type $\varepsilon$ equipped with an extended norm structure and any element $x \in \varepsilon$, the extended norm of the extended norm of $x$ is equal to the extended norm of $x$, i.e., $\| \|x\|_e \|_e = \|x\|_e$.

norm_le_zero_iff' theorem

: ‖a‖ ≤ 0 ↔ a = 1

Full source

@[to_additive (attr := simp) norm_le_zero_iff]
lemma norm_le_zero_iff' : ‖a‖‖a‖ ≤ 0 ↔ a = 1 := by rw [← dist_one_right, dist_le_zero]

Norm Nonpositivity Criterion in Seminormed Groups: $\|a\| \leq 0 \leftrightarrow a = 1$

Informal description

For any element $a$ in a seminormed group, the norm of $a$ is less than or equal to zero if and only if $a$ is the identity element, i.e., $\|a\| \leq 0 \leftrightarrow a = 1$.

norm_pos_iff' theorem

: 0 < ‖a‖ ↔ a ≠ 1

Full source

@[to_additive (attr := simp) norm_pos_iff]
lemma norm_pos_iff' : 0 < ‖a‖ ↔ a ≠ 1 := by rw [← not_le, norm_le_zero_iff']

Positivity of Norm in Seminormed Groups: $0 < \|a\| \leftrightarrow a \neq 1$

Informal description

For any element $a$ in a seminormed group, the norm of $a$ is strictly positive if and only if $a$ is not the identity element, i.e., $0 < \|a\| \leftrightarrow a \neq 1$.

norm_eq_zero' theorem

: ‖a‖ = 0 ↔ a = 1

Full source

@[to_additive (attr := simp) norm_eq_zero]
lemma norm_eq_zero' : ‖a‖‖a‖ = 0 ↔ a = 1 := (norm_nonneg' a).le_iff_eq.symm.trans norm_le_zero_iff'

Norm Vanishing Criterion in Seminormed Groups: $\|a\| = 0 \leftrightarrow a = 1$

Informal description

For any element $a$ in a seminormed group, the norm of $a$ is zero if and only if $a$ is the identity element, i.e., $\|a\| = 0 \leftrightarrow a = 1$.

norm_ne_zero_iff' theorem

: ‖a‖ ≠ 0 ↔ a ≠ 1

Full source

@[to_additive norm_ne_zero_iff]
lemma norm_ne_zero_iff' : ‖a‖‖a‖ ≠ 0‖a‖ ≠ 0 ↔ a ≠ 1 := norm_eq_zero'.not

Nonzero Norm Criterion in Seminormed Groups: $\|a\| \neq 0 \leftrightarrow a \neq 1$

Informal description

For any element $a$ in a seminormed group, the norm of $a$ is nonzero if and only if $a$ is not the identity element, i.e., $\|a\| \neq 0 \leftrightarrow a \neq 1$.

norm_div_eq_zero_iff theorem

: ‖a / b‖ = 0 ↔ a = b

Full source

@[to_additive]
theorem norm_div_eq_zero_iff : ‖a / b‖‖a / b‖ = 0 ↔ a = b := by rw [norm_eq_zero', div_eq_one]

Norm of Quotient Vanishes iff Elements Are Equal: $\|a / b\| = 0 \leftrightarrow a = b$

Informal description

For any elements $a$ and $b$ in a seminormed group, the norm of their quotient $\|a / b\|$ is zero if and only if $a$ equals $b$.

norm_div_pos_iff theorem

: 0 < ‖a / b‖ ↔ a ≠ b

Full source

@[to_additive]
theorem norm_div_pos_iff : 0 < ‖a / b‖ ↔ a ≠ b := by
  rw [(norm_nonneg' _).lt_iff_ne, ne_comm]
  exact norm_div_eq_zero_iff.not

Positivity of Norm of Quotient Characterizes Inequality: $0 < \|a / b\| \leftrightarrow a \neq b$

Informal description

For any elements $a$ and $b$ in a seminormed group, the norm of their quotient $\|a / b\|$ is strictly positive if and only if $a$ is not equal to $b$, i.e., $0 < \|a / b\| \leftrightarrow a \neq b$.

nnnorm_eq_zero' theorem

: ‖a‖₊ = 0 ↔ a = 1

Full source

@[to_additive (attr := simp) nnnorm_eq_zero]
theorem nnnorm_eq_zero' : ‖a‖₊‖a‖₊ = 0 ↔ a = 1 := by
  rw [← NNReal.coe_eq_zero, coe_nnnorm', norm_eq_zero']

Vanishing Non-Negative Norm Criterion in Seminormed Groups: $\|a\|₊ = 0 \leftrightarrow a = 1$

Informal description

For any element $a$ in a seminormed group, the non-negative norm $\|a\|₊$ is zero if and only if $a$ is the identity element, i.e., $\|a\|₊ = 0 \leftrightarrow a = 1$.

nnnorm_ne_zero_iff' theorem

: ‖a‖₊ ≠ 0 ↔ a ≠ 1

Full source

@[to_additive nnnorm_ne_zero_iff]
theorem nnnorm_ne_zero_iff' : ‖a‖₊‖a‖₊ ≠ 0‖a‖₊ ≠ 0 ↔ a ≠ 1 :=
  nnnorm_eq_zero'.not

Nonzero Non-Negative Norm Criterion in Seminormed Groups: $\|a\|₊ \neq 0 \leftrightarrow a \neq 1$

Informal description

For any element $a$ in a seminormed group, the non-negative norm $\|a\|₊$ is nonzero if and only if $a$ is not the identity element, i.e., $\|a\|₊ \neq 0 \leftrightarrow a \neq 1$.

nnnorm_pos' theorem

: 0 < ‖a‖₊ ↔ a ≠ 1

Full source

@[to_additive (attr := simp) nnnorm_pos]
lemma nnnorm_pos' : 0 < ‖a‖₊ ↔ a ≠ 1 := pos_iff_ne_zero.trans nnnorm_ne_zero_iff'

Positivity of Non-Negative Norm in Seminormed Groups: $0 < \|a\|₊ \leftrightarrow a \neq 1$

Informal description

For any element $a$ in a seminormed group, the non-negative norm $\|a\|₊$ is strictly positive if and only if $a$ is not the identity element, i.e., $0 < \|a\|₊ \leftrightarrow a \neq 1$.

normGroupNorm definition

: GroupNorm E

Full source

/-- The norm of a normed group as a group norm. -/
@[to_additive "The norm of a normed group as an additive group norm."]
def normGroupNorm : GroupNorm E :=
  { normGroupSeminorm _ with eq_one_of_map_eq_zero' := fun _ => norm_eq_zero'.1 }

Norm as a group norm

Informal description

The function that assigns to each element $x$ of a normed group $E$ its norm $\|x\|$ is a group norm, meaning it satisfies the following properties: 1. $\|1\| = 0$ (the norm of the identity is zero), 2. $\|x\| \geq 0$ for all $x \in E$ (nonnegativity), 3. $\|x \cdot y\| \leq \|x\| + \|y\|$ for all $x, y \in E$ (subadditivity), 4. $\|x^{-1}\| = \|x\|$ for all $x \in E$ (inverse-invariance), and 5. $\|x\| = 0$ implies $x = 1$ (definiteness).

coe_normGroupNorm theorem

: ⇑(normGroupNorm E) = norm

Full source

@[simp]
theorem coe_normGroupNorm : ⇑(normGroupNorm E) = norm :=
  rfl

Group Norm Function Coincides with Norm

Informal description

The canonical function associated with the group norm structure on a normed group $E$ coincides with the norm function $\|\cdot\|$ on $E$.

hasCompactSupport_norm_iff theorem

: (HasCompactSupport fun x => ‖f x‖) ↔ HasCompactSupport f

Full source

theorem hasCompactSupport_norm_iff : (HasCompactSupport fun x => ‖f x‖) ↔ HasCompactSupport f :=
  hasCompactSupport_comp_left norm_eq_zero

Compact Support of Norm Equivalence

Informal description

For a function $f$, the norm $\|f(x)\|$ has compact support if and only if $f$ itself has compact support.

tendsto_norm_atTop_atTop theorem

: Tendsto (norm : ℝ → ℝ) atTop atTop

Full source

lemma tendsto_norm_atTop_atTop : Tendsto (norm : ℝ → ℝ) atTop atTop := tendsto_abs_atTop_atTop

Absolute Value Tends to Infinity at Infinity

Informal description

The function $\| \cdot \| : \mathbb{R} \to \mathbb{R}$, which maps a real number to its absolute value, tends to infinity as its input tends to infinity. That is, $\lim_{x \to \infty} \|x\| = \infty$.

Mathlib.Meta.Positivity.evalMulNorm definition

: PositivityExt

Full source

/-- Extension for the `positivity` tactic: multiplicative norms are always nonnegative, and positive
on non-one inputs. -/
@[positivity ‖_‖]
def evalMulNorm : PositivityExt where eval {u α} _ _ e := do
  match u, α, e with
  | 0, ~q(ℝ), ~q(@Norm.norm $E $_n $a) =>
    let _seminormedGroup_E ← synthInstanceQ q(SeminormedGroup $E)
    assertInstancesCommute
    -- Check whether we are in a normed group and whether the context contains a `a ≠ 1` assumption
    let o : Option (Q(NormedGroup $E) × Q($a ≠ 1)) := ← do
      let .some normedGroup_E ← trySynthInstanceQ q(NormedGroup $E) | return none
      let some pa ← findLocalDeclWithTypeQ? q($a ≠ 1) | return none
      return some (normedGroup_E, pa)
    match o with
    -- If so, return a proof of `0 < ‖a‖`
    | some (_normedGroup_E, pa) =>
      assertInstancesCommute
      return .positive q(norm_pos_iff'.2 $pa)
    -- Else, return a proof of `0 ≤ ‖a‖`
    | none => return .nonnegative q(norm_nonneg' $a)
  | _, _, _ => throwError "not `‖·‖`"

Positivity of Multiplicative Norms

Informal description

The `evalMulNorm` function is an extension for the `positivity` tactic that handles multiplicative norms. It proves that for any element $a$ in a seminormed group $E$, the norm $\|a\|$ is nonnegative. Additionally, if $E$ is a normed group and $a \neq 1$, it proves that $\|a\|$ is positive.

Mathlib.Meta.Positivity.evalAddNorm definition

: PositivityExt

Full source

/-- Extension for the `positivity` tactic: additive norms are always nonnegative, and positive
on non-zero inputs. -/
@[positivity ‖_‖]
def evalAddNorm : PositivityExt where eval {u α} _ _ e := do
  match u, α, e with
  | 0, ~q(ℝ), ~q(@Norm.norm $E $_n $a) =>
    let _seminormedAddGroup_E ← synthInstanceQ q(SeminormedAddGroup $E)
    assertInstancesCommute
    -- Check whether we are in a normed group and whether the context contains a `a ≠ 0` assumption
    let o : Option (Q(NormedAddGroup $E) × Q($a ≠ 0)) := ← do
      let .some normedAddGroup_E ← trySynthInstanceQ q(NormedAddGroup $E) | return none
      let some pa ← findLocalDeclWithTypeQ? q($a ≠ 0) | return none
      return some (normedAddGroup_E, pa)
    match o with
    -- If so, return a proof of `0 < ‖a‖`
    | some (_normedAddGroup_E, pa) =>
      assertInstancesCommute
      return .positive q(norm_pos_iff.2 $pa)
    -- Else, return a proof of `0 ≤ ‖a‖`
    | none => return .nonnegative q(norm_nonneg $a)
  | _, _, _ => throwError "not `‖·‖`"

Positivity of additive norms

Informal description

The `positivity` tactic extension for additive norms states that for any element $a$ in a seminormed additive group $E$, the norm $\|a\|$ is always nonnegative. If $E$ is a normed additive group and $a$ is nonzero, then $\|a\|$ is positive.

Mathlib.Analysis.Normed.Group.Basic

Notes

Tags