Documentation

Mathlib.Analysis.Normed.Group.Real

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

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

Tags #

normed group

instance NNReal.instNNNorm :

Equations

@[simp]

theorem NNReal.nnnorm_eq_self (x : NNReal) :

instance instENormENNReal :

Equations

@[simp]

theorem enorm_eq_self (x : ENNReal) :

instance instENormedAddCommMonoidENNReal :

ENormedAddCommMonoid ENNReal

Equations

instance Real.norm :

Equations

@[simp]

theorem Real.norm_eq_abs (r : ℝ) :

instance Real.normedAddCommGroup :

NormedAddCommGroup ℝ

Equations

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

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

theorem Real.le_norm_self (r : ℝ) :

theorem Real.norm_natCast (n : ℕ) :

‖↑n‖ = ↑n

@[simp]

theorem Real.nnnorm_natCast (n : ℕ) :

‖↑n‖₊ = ↑n

@[simp]

theorem Real.enorm_natCast (n : ℕ) :

‖↑n‖ₑ = ↑n

@[simp]

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

‖OfNat.ofNat n‖ = OfNat.ofNat n

@[simp]

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

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

theorem Real.norm_two :

theorem Real.nnnorm_two :

@[simp]

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

‖↑q‖ = ↑q

@[simp]

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

‖↑q‖₊ = ↑q

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

‖r‖₊ = ⟨r, hr⟩

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

‖r‖ₑ = ENNReal.ofReal r

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

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

@[simp]

theorem Real.nnnorm_abs (r : ℝ) :

‖|r|‖₊ = ‖r‖₊

@[simp]

theorem Real.enorm_abs (r : ℝ) :

‖|r|‖ₑ = ‖r‖ₑ

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

‖r‖ₑ = ENNReal.ofReal r

theorem Real.enorm_eq_ofReal_abs (r : ℝ) :

‖r‖ₑ = ENNReal.ofReal |r|

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

r.toNNReal = ‖r‖₊

theorem Real.ofReal_le_enorm (r : ℝ) :

ENNReal.ofReal r ≤ ‖r‖ₑ

@[simp]

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

‖‖x‖‖ = ‖x‖

@[simp]

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

‖‖x‖‖ = ‖x‖

@[simp]

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

‖‖x‖‖₊ = ‖x‖₊

@[simp]

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

‖‖x‖‖₊ = ‖x‖₊

@[simp]

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

‖‖x‖‖ₑ = ‖x‖ₑ

@[simp]

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

‖‖x‖‖ₑ = ‖x‖ₑ

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

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

theorem tendsto_norm_atTop_atTop :

Filter.Tendsto norm Filter.atTop Filter.atTop