Mathlib.Analysis.Normed.Group.Int

Int.instNormedAddCommGroup instance

: NormedAddCommGroup ℤ

Full source

instance instNormedAddCommGroup : NormedAddCommGroup ℤ where
  norm n := ‖(n : ℝ)‖
  dist_eq m n := by simp only [Int.dist_eq, norm, Int.cast_sub]

The Normed Additive Commutative Group Structure on Integers

Informal description

The integers $\mathbb{Z}$ form a normed additive commutative group, where the norm of an integer $n$ is given by the absolute value of its real number embedding, $\|n\| = |(n : \mathbb{R})|$.

Int.norm_cast_real theorem

(m : ℤ) : ‖(m : ℝ)‖ = ‖m‖

Full source

@[norm_cast]
theorem norm_cast_real (m : ℤ) : ‖(m : ℝ)‖ = ‖m‖ :=
  rfl

Norm Preservation of Integer Cast to Real Numbers

Informal description

For any integer $m \in \mathbb{Z}$, the norm of its real embedding equals its integer norm, i.e., $\|(m : \mathbb{R})\| = \|m\|$.

Int.norm_eq_abs theorem

(n : ℤ) : ‖n‖ = |(n : ℝ)|

Full source

theorem norm_eq_abs (n : ℤ) : ‖n‖ = |(n : ℝ)| :=
  rfl

Norm of Integer Equals Absolute Value of its Real Embedding

Informal description

For any integer $n \in \mathbb{Z}$, the norm of $n$ is equal to the absolute value of its embedding in the real numbers, i.e., $\|n\| = |(n : \mathbb{R})|$.

Int.norm_natCast theorem

(n : ℕ) : ‖(n : ℤ)‖ = n

Full source

@[simp]
theorem norm_natCast (n : ℕ) : ‖(n : ℤ)‖ = n := by simp [Int.norm_eq_abs]

Norm of Natural Number Embedding in Integers: $\|(n : \mathbb{Z})\| = n$

Informal description

For any natural number $n$, the norm of its embedding in the integers equals $n$, i.e., $\|(n : \mathbb{Z})\| = n$.

NNReal.natCast_natAbs theorem

(n : ℤ) : (n.natAbs : ℝ≥0) = ‖n‖₊

Full source

theorem _root_.NNReal.natCast_natAbs (n : ℤ) : (n.natAbs : ℝ≥0) = ‖n‖₊ :=
  NNReal.eq <|
    calc
      ((n.natAbs : ℝ≥0) : ℝ) = (n.natAbs : ℤ) := by simp only [Int.cast_natCast, NNReal.coe_natCast]
      _ = |(n : ℝ)| := by simp only [Int.natCast_natAbs, Int.cast_abs]
      _ = ‖n‖ := (norm_eq_abs n).symm

Embedding of Natural Absolute Value Equals Seminorm of Integer

Informal description

For any integer $n \in \mathbb{Z}$, the canonical embedding of its natural absolute value into the nonnegative real numbers equals the seminorm of $n$, i.e., $(\text{natAbs}(n) : \mathbb{R}_{\geq 0}) = \|n\|_+$.

Int.abs_le_floor_nnreal_iff theorem

(z : ℤ) (c : ℝ≥0) : |z| ≤ ⌊c⌋₊ ↔ ‖z‖₊ ≤ c

Full source

theorem abs_le_floor_nnreal_iff (z : ℤ) (c : ℝ≥0) : |z||z| ≤ ⌊c⌋₊ ↔ ‖z‖₊ ≤ c := by
  rw [Int.abs_eq_natAbs, Int.ofNat_le, Nat.le_floor_iff (zero_le c), NNReal.natCast_natAbs z]

Equivalence of Integer Absolute Value Bound and Seminorm Bound via Natural Floor

Informal description

For any integer $z$ and nonnegative real number $c$, the absolute value of $z$ is less than or equal to the natural floor of $c$ if and only if the seminorm of $z$ is less than or equal to $c$. In other words: $$|z| \leq \lfloor c \rfloor_\mathbb{N} \leftrightarrow \|z\|_+ \leq c$$

norm_zpow_le_mul_norm theorem

(n : ℤ) (a : α) : ‖a ^ n‖ ≤ ‖n‖ * ‖a‖

Full source

@[to_additive norm_zsmul_le]
theorem norm_zpow_le_mul_norm (n : ℤ) (a : α) : ‖a ^ n‖ ≤ ‖n‖ * ‖a‖ := by
  rcases n.eq_nat_or_neg with ⟨n, rfl | rfl⟩ <;> simpa using norm_pow_le_mul_norm

Norm of Integer Power Bounded by Product of Norms: $\|a^n\| \leq |n| \cdot \|a\|$

Informal description

For any element $a$ in a seminormed group $\alpha$ and any integer $n$, the norm of $a^n$ satisfies $\|a^n\| \leq \|n\| \cdot \|a\|$, where $\|n\|$ denotes the norm of $n$ in $\mathbb{Z}$ (which is equal to $|n|$).

nnnorm_zpow_le_mul_norm theorem

(n : ℤ) (a : α) : ‖a ^ n‖₊ ≤ ‖n‖₊ * ‖a‖₊

Full source

@[to_additive nnnorm_zsmul_le]
theorem nnnorm_zpow_le_mul_norm (n : ℤ) (a : α) : ‖a ^ n‖₊ ≤ ‖n‖₊ * ‖a‖₊ := by
  simpa only [← NNReal.coe_le_coe, NNReal.coe_mul] using norm_zpow_le_mul_norm n a

Non-negative norm bound for integer powers: $\|a^n\|_+ \leq |n| \cdot \|a\|_+$

Informal description

For any integer $n$ and any element $a$ in a seminormed commutative group $\alpha$, the non-negative norm of $a^n$ satisfies $\|a^n\|_+ \leq \|n\|_+ \cdot \|a\|_+$, where $\|n\|_+$ denotes the non-negative norm of $n$ (which is equal to $|n|$ when viewed as a real number).