Norms on `ℝ` and `ℝ≥0` #

We equip ℝ, ℝ≥0, and ℝ≥0∞ with their natural norms / enorms.

Tags #

normed group

source

@[instance_reducible]

instance NNReal.instNNNorm :

NNNorm NNReal

Equations

NNReal.instNNNorm = { nnNorm := fun (x : NNReal) => x }

source

@[simp]

theorem NNReal.nnNorm_eq_self (x : NNReal) :

‖x‖₊ = x

source

@[deprecated NNReal.nnNorm_eq_self (since := "2026-10-31")]

theorem NNReal.nnnorm_eq_self (x : NNReal) :

‖x‖₊ = x

Alias of NNReal.nnNorm_eq_self.

source

@[simp]

theorem NNReal.enorm_eq_coe (x : NNReal) :

‖x‖ₑ = ↑x

source

@[instance_reducible]

instance instENormENNReal :

ENorm ENNReal

Equations

instENormENNReal = { enorm := fun (x : ENNReal) => x }

source

@[simp]

theorem enorm_eq_self (x : ENNReal) :

‖x‖ₑ = x

source

@[instance_reducible]

noncomputable instance instENormedAddCommMonoidENNReal :

ENormedAddCommMonoid ENNReal

Equations

One or more equations did not get rendered due to their size.

source

@[instance_reducible]

instance Real.norm :

Norm ℝ

Equations

Real.norm = { norm := fun (r : ℝ) => |r| }

source

@[simp]

theorem Real.norm_eq_abs (r : ℝ) :

‖r‖ = |r|

source

@[instance_reducible]

instance Real.normedAddCommGroup :

NormedAddCommGroup ℝ

Equations

Real.normedAddCommGroup = { toNorm := Real.norm, toAddCommGroup := Real.instAddCommGroup, toMetricSpace := Real.metricSpace, dist_eq := ⋯ }

source

theorem Real.norm_of_nonneg {r : ℝ} (hr : 0 ≤ r) :

‖r‖ = r

source

theorem Real.norm_of_nonpos {r : ℝ} (hr : r ≤ 0) :

‖r‖ = -r

source

theorem Real.le_norm_self (r : ℝ) :

r ≤ ‖r‖

source

theorem Real.norm_natCast (n : ℕ) :

‖↑n‖ = ↑n

source

@[simp]

theorem Real.nnNorm_natCast (n : ℕ) :

‖↑n‖₊ = ↑n

source

@[simp]

theorem Real.enorm_natCast (n : ℕ) :

‖↑n‖ₑ = ↑n

source

@[deprecated Real.nnNorm_natCast (since := "2026-10-31")]

theorem Real.nnnorm_natCast (n : ℕ) :

‖↑n‖₊ = ↑n

Alias of Real.nnNorm_natCast.

source

@[simp]

theorem Real.norm_ofNat (n : ℕ) [n.AtLeastTwo] :

‖OfNat.ofNat n‖ = OfNat.ofNat n

source

@[simp]

theorem Real.nnNorm_ofNat (n : ℕ) [n.AtLeastTwo] :

‖OfNat.ofNat n‖₊ = OfNat.ofNat n

source

@[deprecated Real.nnNorm_ofNat (since := "2026-10-31")]

theorem Real.nnnorm_ofNat (n : ℕ) [n.AtLeastTwo] :

‖OfNat.ofNat n‖₊ = OfNat.ofNat n

Alias of Real.nnNorm_ofNat.

source

theorem Real.norm_two :

‖2‖ = 2

source

theorem Real.nnNorm_two :

‖2‖₊ = 2

source

@[deprecated Real.nnNorm_two (since := "2026-10-31")]

theorem Real.nnnorm_two :

‖2‖₊ = 2

Alias of Real.nnNorm_two.

source

@[simp]

theorem Real.norm_nnratCast (q : ℚ≥0) :

‖↑q‖ = ↑q

source

@[simp]

theorem Real.nnNorm_nnRatCast (q : ℚ≥0) :

‖↑q‖₊ = ↑q

source

@[deprecated Real.nnNorm_nnRatCast (since := "2026-10-31")]

theorem Real.nnnorm_nnratCast (q : ℚ≥0) :

‖↑q‖₊ = ↑q

Alias of Real.nnNorm_nnRatCast.

source

theorem Real.nnNorm_of_nonneg {r : ℝ} (hr : 0 ≤ r) :

‖r‖₊ = NNReal.mk r hr

source

@[deprecated Real.nnNorm_of_nonneg (since := "2026-10-31")]

theorem Real.nnnorm_of_nonneg {r : ℝ} (hr : 0 ≤ r) :

‖r‖₊ = NNReal.mk r hr

Alias of Real.nnNorm_of_nonneg.

source

theorem Real.enorm_of_nonneg {r : ℝ} (hr : 0 ≤ r) :

‖r‖ₑ = ENNReal.ofReal r

source

theorem Real.enorm_ofReal_of_nonneg {a : ℝ} (ha : 0 ≤ a) :

‖ENNReal.ofReal a‖ₑ = ‖a‖ₑ

source

@[simp]

theorem Real.nnNorm_abs (r : ℝ) :

‖|r|‖₊ = ‖r‖₊

source

@[simp]

theorem Real.enorm_abs (r : ℝ) :

‖|r|‖ₑ = ‖r‖ₑ

source

@[deprecated Real.nnNorm_abs (since := "2026-10-31")]

theorem Real.nnnorm_abs (r : ℝ) :

‖|r|‖₊ = ‖r‖₊

Alias of Real.nnNorm_abs.

source

theorem Real.enorm_eq_ofReal {r : ℝ} (hr : 0 ≤ r) :

‖r‖ₑ = ENNReal.ofReal r

source

@[simp]

theorem Real.enorm_toReal {a : ENNReal} (ha : a ≠ ⊤) :

‖a.toReal‖ₑ = a

source

theorem Real.enorm_eq_ofReal_abs (r : ℝ) :

‖r‖ₑ = ENNReal.ofReal |r|

source

theorem Real.toNNReal_eq_nnNorm_of_nonneg {r : ℝ} (hr : 0 ≤ r) :

r.toNNReal = ‖r‖₊

source

@[deprecated Real.toNNReal_eq_nnNorm_of_nonneg (since := "2026-10-31")]

theorem Real.toNNReal_eq_nnnorm_of_nonneg {r : ℝ} (hr : 0 ≤ r) :

r.toNNReal = ‖r‖₊

Alias of Real.toNNReal_eq_nnNorm_of_nonneg.

source

theorem Real.ofReal_le_enorm (r : ℝ) :

ENNReal.ofReal r ≤ ‖r‖ₑ

source

@[simp]

theorem norm_norm' {E : Type u_1} [SeminormedCommGroup E] (x : E) :

‖‖x‖‖ = ‖x‖

source

@[simp]

theorem norm_norm {E : Type u_1} [SeminormedAddCommGroup E] (x : E) :

‖‖x‖‖ = ‖x‖

source

@[simp]

theorem nnNorm_norm' {E : Type u_1} [SeminormedCommGroup E] (x : E) :

‖‖x‖‖₊ = ‖x‖₊

source

@[simp]

theorem nnNorm_norm {E : Type u_1} [SeminormedAddCommGroup E] (x : E) :

‖‖x‖‖₊ = ‖x‖₊

source

@[deprecated nnNorm_norm' (since := "2026-10-31")]

theorem nnnorm_norm' {E : Type u_1} [SeminormedCommGroup E] (x : E) :

‖‖x‖‖₊ = ‖x‖₊

Alias of nnNorm_norm'.

source

@[deprecated nnNorm_norm (since := "2026-10-31")]

theorem nnnorm_norm {E : Type u_1} [SeminormedAddCommGroup E] (x : E) :

‖‖x‖‖₊ = ‖x‖₊

Alias of nnNorm_norm.

source

@[simp]

theorem enorm_norm' {E : Type u_1} [SeminormedCommGroup E] (x : E) :

‖‖x‖‖ₑ = ‖x‖ₑ

source

@[simp]

theorem enorm_norm {E : Type u_1} [SeminormedAddCommGroup E] (x : E) :

‖‖x‖‖ₑ = ‖x‖ₑ

source

theorem enorm_enorm {ε : Type u_3} [ENorm ε] (x : ε) :

‖‖x‖ₑ ‖ₑ = ‖x‖ₑ

source

theorem tendsto_norm_atTop_atTop :

Filter.Tendsto norm Filter.atTop Filter.atTop

Documentation

Mathlib.Analysis.Normed.Group.Real

Norms on `ℝ` and `ℝ≥0` #

Tags #

Norms on ℝ and ℝ≥0 #

Tags #

Norms on `ℝ` and `ℝ≥0` #