Documentation

Mathlib.Analysis.Normed.Group.Real

Norms on ℝ and ℝ≥0 #

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

Tags #

normed group

source
instance NNReal.instNNNorm :
NNNorm NNReal
Equations
    source
    @[simp]
    theorem NNReal.nnnorm_eq_self (x : NNReal) :
    ‖x‖₊ = x
    source
    instance instENormENNReal :
    ENorm ENNReal
    Equations
      source
      @[simp]
      theorem enorm_eq_self (x : ENNReal) :
      ‖x‖ₑ = x
      source
      instance instENormedAddCommMonoidENNReal :
      ENormedAddCommMonoid ENNReal
      Equations
        source
        instance Real.norm :
        Norm ℝ
        Equations
          source
          @[simp]
          theorem Real.norm_eq_abs (r : ℝ) :
          ‖r‖ = |r|
          source
          instance Real.normedAddCommGroup :
          NormedAddCommGroup ℝ
          Equations
            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
            @[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
            theorem Real.norm_two :
            ‖2‖ = 2
            source
            theorem Real.nnnorm_two :
            ‖2‖₊ = 2
            source
            @[simp]
            theorem Real.norm_nnratCast (q : ℚ≥0) :
            ‖↑q‖ = ↑q
            source
            @[simp]
            theorem Real.nnnorm_nnratCast (q : ℚ≥0) :
            ‖↑q‖₊ = ↑q
            source
            theorem Real.nnnorm_of_nonneg {r : ℝ} (hr : 0 ≤ r) :
            ‖r‖₊ = ⟨r, hr⟩
            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
            theorem Real.enorm_eq_ofReal {r : ℝ} (hr : 0 ≤ r) :
            ‖r‖ₑ = ENNReal.ofReal r
            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
            theorem Real.ofReal_le_enorm (r : ℝ) :
            ENNReal.ofReal r ≤ ‖r‖ₑ
            source
            @[simp]
            theorem norm_norm' {E : Type u_5} [SeminormedCommGroup E] (x : E) :
            ‖‖x‖‖ = ‖x‖
            source
            @[simp]
            theorem norm_norm {E : Type u_5} [SeminormedAddCommGroup E] (x : E) :
            ‖‖x‖‖ = ‖x‖
            source
            @[simp]
            theorem nnnorm_norm' {E : Type u_5} [SeminormedCommGroup E] (x : E) :
            ‖‖x‖‖₊ = ‖x‖₊
            source
            @[simp]
            theorem nnnorm_norm {E : Type u_5} [SeminormedAddCommGroup E] (x : E) :
            ‖‖x‖‖₊ = ‖x‖₊
            source
            @[simp]
            theorem enorm_norm' {E : Type u_5} [SeminormedCommGroup E] (x : E) :
            ‖‖x‖‖ₑ = ‖x‖ₑ
            source
            @[simp]
            theorem enorm_norm {E : Type u_5} [SeminormedAddCommGroup E] (x : E) :
            ‖‖x‖‖ₑ = ‖x‖ₑ
            source
            theorem enorm_enorm {ε : Type u_9} [ENorm ε] (x : ε) :
            ‖‖x‖ₑ‖ₑ = ‖x‖ₑ
            source
            theorem tendsto_norm_atTop_atTop :
            Filter.Tendsto norm Filter.atTop Filter.atTop