Norms on ℝ and ℝ≥0

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

Tags

normed group

@[instance_reducible]

instance NNReal.instNNNorm : NNNorm NNReal

Equations

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

@[simp]

theorem NNReal.nnnorm_eq_self (x : NNReal) : ‖x‖₊ = x

@[instance_reducible]

instance instENormENNReal : ENorm ENNReal

Equations

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

@[simp]

theorem enorm_eq_self (x : ENNReal) : ‖x‖ₑ = x

@[instance_reducible]

noncomputable instance instENormedAddCommMonoidENNReal : ENormedAddCommMonoid ENNReal

Equations

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

@[instance_reducible]

instance Real.norm : Norm ℝ

Equations

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

@[simp]

theorem Real.norm_eq_abs (r : ℝ) : ‖r‖ = |r|

@[instance_reducible]

instance Real.normedAddCommGroup : NormedAddCommGroup ℝ

Equations

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

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

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

theorem Real.le_norm_self (r : ℝ) : r ≤ ‖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 : ‖2‖ = 2

theorem Real.nnnorm_two : ‖2‖₊ = 2

@[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‖₊ = NNReal.mk 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

@[simp]

theorem Real.enorm_toReal {a : ENNReal} (ha : a ≠ ⊤) : ‖a.toReal‖ₑ = a

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