Documentation

Mathlib.Data.NNReal.Defs

Nonnegative real numbers #

In this file we define NNReal (notation: ℝ≥0) to be the type of non-negative real numbers, a.k.a. the interval [0, ∞). We also define the following operations and structures on ℝ≥0:

We also define an instance CanLift ℝ ℝ≥0. This instance can be used by the lift tactic to replace x : ℝ and hx : 0 ≤ x in the proof context with x : ℝ≥0 while replacing all occurrences of x with ↑x. This tactic also works for a function f : α → ℝ with a hypothesis hf : ∀ x, 0 ≤ f x.

Notations #

This file defines ℝ≥0 as a localized notation for NNReal.

Nonnegative real numbers, denoted as ℝ≥0 withinin the NNReal namespace

Equations
Instances For

    Nonnegative real numbers, denoted as ℝ≥0 withinin the NNReal namespace

    Equations
    Instances For
      Equations

      Coercion ℝ≥0 → ℝ.

      Equations
      Instances For
        @[simp]
        theorem NNReal.val_eq_coe (n : NNReal) :
        n = n
        instance NNReal.canLift :
        CanLift NNReal toReal fun (r : ) => 0 r
        theorem NNReal.eq {n m : NNReal} :
        n = mn = m
        theorem NNReal.ne_iff {x y : NNReal} :
        x y x y
        theorem NNReal.forall {p : NNRealProp} :
        (∀ (x : NNReal), p x) ∀ (x : ) (hx : 0 x), p x, hx
        theorem NNReal.exists {p : NNRealProp} :
        (∃ (x : NNReal), p x) ∃ (x : ) (hx : 0 x), p x, hx

        Reinterpret a real number r as a non-negative real number. Returns 0 if r < 0.

        Equations
        Instances For
          theorem Real.coe_toNNReal (r : ) (hr : 0 r) :
          r.toNNReal = r
          theorem Real.toNNReal_of_nonneg {r : } (hr : 0 r) :
          r.toNNReal = r, hr
          theorem NNReal.coe_nonneg (r : NNReal) :
          0 r
          @[simp]
          theorem NNReal.coe_mk (a : ) (ha : 0 a) :
          a, ha = a
          @[simp]
          theorem NNReal.coe_inj {r₁ r₂ : NNReal} :
          r₁ = r₂ r₁ = r₂
          @[simp]
          theorem NNReal.coe_zero :
          0 = 0
          @[simp]
          theorem NNReal.coe_one :
          1 = 1
          @[simp]
          theorem NNReal.mk_zero :
          0, = 0
          @[simp]
          theorem NNReal.mk_one :
          1, = 1
          @[simp]
          theorem NNReal.coe_add (r₁ r₂ : NNReal) :
          ↑(r₁ + r₂) = r₁ + r₂
          @[simp]
          theorem NNReal.coe_mul (r₁ r₂ : NNReal) :
          ↑(r₁ * r₂) = r₁ * r₂
          @[simp]
          theorem NNReal.coe_inv (r : NNReal) :
          r⁻¹ = (↑r)⁻¹
          @[simp]
          theorem NNReal.coe_div (r₁ r₂ : NNReal) :
          ↑(r₁ / r₂) = r₁ / r₂
          theorem NNReal.coe_two :
          2 = 2
          @[simp]
          theorem NNReal.coe_sub {r₁ r₂ : NNReal} (h : r₂ r₁) :
          ↑(r₁ - r₂) = r₁ - r₂
          @[simp]
          theorem NNReal.coe_eq_zero {r : NNReal} :
          r = 0 r = 0
          @[simp]
          theorem NNReal.coe_eq_one {r : NNReal} :
          r = 1 r = 1
          theorem NNReal.coe_ne_zero {r : NNReal} :
          r 0 r 0
          theorem NNReal.coe_ne_one {r : NNReal} :
          r 1 r 1

          Coercion ℝ≥0 → ℝ as a RingHom.

          Porting note (https://github.com/leanprover-community/mathlib4/issues/11215): TODO: what if we define Coe ℝ≥0 ℝ using this function?

          Equations
          Instances For
            theorem NNReal.smul_def {M : Type u_1} [MulAction M] (c : NNReal) (x : M) :
            c x = c x

            A Module over restricts to a Module over ℝ≥0.

            Equations

            An Algebra over restricts to an Algebra over ℝ≥0.

            Equations
            @[simp]
            theorem NNReal.coe_pow (r : NNReal) (n : ) :
            ↑(r ^ n) = r ^ n
            @[simp]
            theorem NNReal.coe_zpow (r : NNReal) (n : ) :
            ↑(r ^ n) = r ^ n
            @[simp]
            theorem NNReal.coe_nsmul (r : NNReal) (n : ) :
            ↑(n r) = n r
            @[simp]
            theorem NNReal.coe_nnqsmul (q : ℚ≥0) (x : NNReal) :
            ↑(q x) = q x
            @[simp]
            theorem NNReal.coe_natCast (n : ) :
            n = n
            @[simp]
            @[simp]
            theorem NNReal.coe_le_coe {r₁ r₂ : NNReal} :
            r₁ r₂ r₁ r₂
            @[simp]
            theorem NNReal.coe_lt_coe {r₁ r₂ : NNReal} :
            r₁ < r₂ r₁ < r₂
            @[simp]
            theorem NNReal.coe_pos {r : NNReal} :
            0 < r 0 < r
            @[simp]
            theorem NNReal.one_le_coe {r : NNReal} :
            1 r 1 r
            @[simp]
            theorem NNReal.one_lt_coe {r : NNReal} :
            1 < r 1 < r
            @[simp]
            theorem NNReal.coe_le_one {r : NNReal} :
            r 1 r 1
            @[simp]
            theorem NNReal.coe_lt_one {r : NNReal} :
            r < 1 r < 1
            theorem NNReal.GCongr.toReal_le_toReal {r₁ r₂ : NNReal} :
            r₁ r₂r₁ r₂

            Alias for the use of gcongr

            @[simp]
            theorem Real.toNNReal_coe {r : NNReal} :
            (↑r).toNNReal = r
            @[simp]
            theorem NNReal.mk_natCast (n : ) :
            n, = n
            @[simp]
            theorem NNReal.toNNReal_coe_nat (n : ) :
            (↑n).toNNReal = n
            def NNReal.orderIsoIccZeroCoe (a : NNReal) :
            (Set.Icc 0 a) ≃o (Set.Iic a)

            If a is a nonnegative real number, then the closed interval [0, a] in is order isomorphic to the interval Set.Iic a.

            Equations
            Instances For
              @[simp]
              theorem NNReal.orderIsoIccZeroCoe_apply_coe_coe (a : NNReal) (b : (Set.Icc 0 a)) :
              (a.orderIsoIccZeroCoe b) = b
              @[simp]
              theorem NNReal.coe_image {s : Set NNReal} :
              toReal '' s = {x : | ∃ (h : 0 x), x, h s}
              theorem NNReal.coe_sSup (s : Set NNReal) :
              (sSup s) = sSup (toReal '' s)
              @[simp]
              theorem NNReal.coe_iSup {ι : Sort u_2} (s : ιNNReal) :
              (⨆ (i : ι), s i) = ⨆ (i : ι), (s i)
              theorem NNReal.coe_sInf (s : Set NNReal) :
              (sInf s) = sInf (toReal '' s)
              @[simp]
              theorem NNReal.coe_iInf {ι : Sort u_2} (s : ιNNReal) :
              (⨅ (i : ι), s i) = ⨅ (i : ι), (s i)
              @[deprecated le_of_forall_pos_le_add (since := "2024-10-17")]
              theorem NNReal.le_of_forall_pos_le_add {a b : NNReal} (h : ∀ (ε : NNReal), 0 < εa b + ε) :
              a b
              theorem NNReal.lt_iff_exists_rat_btwn (a b : NNReal) :
              a < b ∃ (q : ), 0 q a < (↑q).toNNReal (↑q).toNNReal < b
              theorem NNReal.mul_sup (a b c : NNReal) :
              a * (b c) = a * b a * c
              theorem NNReal.sup_mul (a b c : NNReal) :
              (a b) * c = a * c b * c
              @[simp]
              theorem NNReal.coe_max (x y : NNReal) :
              ↑(x y) = x y
              @[simp]
              theorem NNReal.coe_min (x y : NNReal) :
              ↑(x y) = x y
              @[simp]
              theorem NNReal.zero_le_coe {q : NNReal} :
              0 q
              @[simp]
              theorem Real.coe_toNNReal' (r : ) :
              r.toNNReal = r 0
              @[simp]
              @[simp]
              @[simp]
              theorem Real.toNNReal_pos {r : } :
              0 < r.toNNReal 0 < r
              @[simp]
              theorem Real.toNNReal_eq_zero {r : } :
              r.toNNReal = 0 r 0
              theorem Real.toNNReal_of_nonpos {r : } :
              r 0r.toNNReal = 0
              theorem Real.toNNReal_eq_iff_eq_coe {r : } {p : NNReal} (hp : p 0) :
              r.toNNReal = p r = p
              @[simp]
              theorem Real.toNNReal_eq_one {r : } :
              r.toNNReal = 1 r = 1
              @[simp]
              theorem Real.toNNReal_eq_natCast {r : } {n : } (hn : n 0) :
              r.toNNReal = n r = n
              @[simp]
              theorem Real.toNNReal_le_toNNReal_iff {r p : } (hp : 0 p) :
              @[simp]
              theorem Real.toNNReal_le_one {r : } :
              @[simp]
              theorem Real.one_lt_toNNReal {r : } :
              1 < r.toNNReal 1 < r
              @[simp]
              theorem Real.toNNReal_le_natCast {r : } {n : } :
              r.toNNReal n r n
              @[simp]
              theorem Real.natCast_lt_toNNReal {r : } {n : } :
              n < r.toNNReal n < r
              @[simp]
              theorem Real.toNNReal_le_ofNat {r : } {n : } [n.AtLeastTwo] :
              @[simp]
              theorem Real.ofNat_lt_toNNReal {r : } {n : } [n.AtLeastTwo] :
              @[simp]
              theorem Real.toNNReal_eq_toNNReal_iff {r p : } (hr : 0 r) (hp : 0 p) :
              @[simp]
              theorem Real.toNNReal_lt_toNNReal_iff {r p : } (h : 0 < p) :
              theorem Real.lt_of_toNNReal_lt {r p : } (h : r.toNNReal < p.toNNReal) :
              r < p
              @[simp]
              theorem Real.one_le_toNNReal {r : } :
              @[simp]
              theorem Real.toNNReal_lt_one {r : } :
              r.toNNReal < 1 r < 1
              @[simp]
              theorem Real.natCastle_toNNReal' {n : } {r : } :
              n r.toNNReal n r n = 0
              @[simp]
              theorem Real.toNNReal_lt_natCast' {n : } {r : } :
              r.toNNReal < n r < n n 0
              theorem Real.natCast_le_toNNReal {n : } {r : } (hn : n 0) :
              n r.toNNReal n r
              theorem Real.toNNReal_lt_natCast {r : } {n : } (hn : n 0) :
              r.toNNReal < n r < n
              @[simp]
              theorem Real.toNNReal_add {r p : } (hr : 0 r) (hp : 0 p) :
              theorem Real.toNNReal_add_toNNReal {r p : } (hr : 0 r) (hp : 0 p) :
              theorem Real.le_toNNReal_iff_coe_le {r : NNReal} {p : } (hp : 0 p) :
              r p.toNNReal r p
              theorem Real.le_toNNReal_iff_coe_le' {r : NNReal} {p : } (hr : 0 < r) :
              r p.toNNReal r p
              theorem Real.toNNReal_lt_iff_lt_coe {r : } {p : NNReal} (ha : 0 r) :
              r.toNNReal < p r < p
              theorem Real.lt_toNNReal_iff_coe_lt {r : NNReal} {p : } :
              r < p.toNNReal r < p
              theorem Real.toNNReal_pow {x : } (hx : 0 x) (n : ) :
              (x ^ n).toNNReal = x.toNNReal ^ n
              theorem Real.toNNReal_mul {p q : } (hp : 0 p) :
              theorem NNReal.mul_eq_mul_left {a b c : NNReal} (h : a 0) :
              a * b = a * c b = c
              theorem NNReal.pow_antitone_exp {a : NNReal} (m n : ) (mn : m n) (a1 : a 1) :
              a ^ n a ^ m
              theorem NNReal.exists_pow_lt_of_lt_one {a b : NNReal} (ha : 0 < a) (hb : b < 1) :
              ∃ (n : ), b ^ n < a
              theorem NNReal.exists_mem_Ico_zpow {x y : NNReal} (hx : x 0) (hy : 1 < y) :
              ∃ (n : ), x Set.Ico (y ^ n) (y ^ (n + 1))
              theorem NNReal.exists_mem_Ioc_zpow {x y : NNReal} (hx : x 0) (hy : 1 < y) :
              ∃ (n : ), x Set.Ioc (y ^ n) (y ^ (n + 1))

              Lemmas about subtraction #

              In this section we provide a few lemmas about subtraction that do not fit well into any other typeclass. For lemmas about subtraction and addition see lemmas about OrderedSub in the file Mathlib.Algebra.Order.Sub.Basic. See also mul_tsub and tsub_mul.

              theorem NNReal.sub_def {r p : NNReal} :
              r - p = (r - p).toNNReal
              theorem NNReal.coe_sub_def {r p : NNReal} :
              ↑(r - p) = (r - p) 0
              @[simp]
              theorem NNReal.inv_le {r p : NNReal} (h : r 0) :
              r⁻¹ p 1 r * p
              theorem NNReal.inv_le_of_le_mul {r p : NNReal} (h : 1 r * p) :
              @[simp]
              theorem NNReal.le_inv_iff_mul_le {r p : NNReal} (h : p 0) :
              r p⁻¹ r * p 1
              @[simp]
              theorem NNReal.lt_inv_iff_mul_lt {r p : NNReal} (h : p 0) :
              r < p⁻¹ r * p < 1
              @[deprecated le_inv_mul_iff₀ (since := "2024-08-21")]
              theorem NNReal.mul_le_iff_le_inv {a b r : NNReal} (hr : r 0) :
              r * a b a r⁻¹ * b
              @[deprecated le_div_iff₀ (since := "2024-08-21")]
              theorem NNReal.le_div_iff_mul_le {a b r : NNReal} (hr : r 0) :
              a b / r a * r b
              @[deprecated div_le_iff₀ (since := "2024-08-21")]
              theorem NNReal.div_le_iff {a b r : NNReal} (hr : r 0) :
              a / r b a b * r
              @[deprecated div_le_iff₀' (since := "2024-08-21")]
              theorem NNReal.div_le_iff' {a b r : NNReal} (hr : r 0) :
              a / r b a r * b
              theorem NNReal.div_le_of_le_mul {a b c : NNReal} (h : a b * c) :
              a / c b
              theorem NNReal.div_le_of_le_mul' {a b c : NNReal} (h : a b * c) :
              a / b c
              @[deprecated le_div_iff₀ (since := "2024-08-21")]
              theorem NNReal.le_div_iff {a b r : NNReal} (hr : r 0) :
              a b / r a * r b
              @[deprecated le_div_iff₀' (since := "2024-10-02")]
              theorem NNReal.le_div_iff' {a b r : NNReal} (hr : r 0) :
              a b / r r * a b
              @[deprecated div_lt_iff₀ (since := "2024-10-02")]
              theorem NNReal.div_lt_iff {a b r : NNReal} (hr : r 0) :
              a / r < b a < b * r
              @[deprecated div_lt_iff₀' (since := "2024-10-02")]
              theorem NNReal.div_lt_iff' {a b r : NNReal} (hr : r 0) :
              a / r < b a < r * b
              @[deprecated lt_div_iff₀ (since := "2024-10-02")]
              theorem NNReal.lt_div_iff {a b r : NNReal} (hr : r 0) :
              a < b / r a * r < b
              @[deprecated lt_div_iff₀' (since := "2024-10-02")]
              theorem NNReal.lt_div_iff' {a b r : NNReal} (hr : r 0) :
              a < b / r r * a < b
              theorem NNReal.mul_lt_of_lt_div {a b r : NNReal} (h : a < b / r) :
              a * r < b
              @[deprecated div_le_div_of_nonneg_left (since := "2024-11-12")]
              theorem NNReal.div_le_div_left_of_le {a b c : NNReal} (c0 : c 0) (cb : c b) :
              a / b a / c
              @[deprecated div_le_div_iff_of_pos_left (since := "2024-11-12")]
              theorem NNReal.div_le_div_left {a b c : NNReal} (a0 : 0 < a) (b0 : 0 < b) (c0 : 0 < c) :
              a / b a / c c b
              theorem NNReal.le_of_forall_lt_one_mul_le {x y : NNReal} (h : a < 1, a * x y) :
              x y
              theorem NNReal.half_le_self (a : NNReal) :
              a / 2 a
              theorem NNReal.half_lt_self {a : NNReal} (h : a 0) :
              a / 2 < a
              theorem NNReal.div_lt_one_of_lt {a b : NNReal} (h : a < b) :
              a / b < 1
              theorem Real.toNNReal_div {x y : } (hx : 0 x) :
              theorem Real.toNNReal_div' {x y : } (hy : 0 y) :
              theorem NNReal.inv_lt_one_iff {x : NNReal} (hx : x 0) :
              x⁻¹ < 1 1 < x
              @[deprecated zpow_pos (since := "2024-10-08")]
              theorem NNReal.zpow_pos {x : NNReal} (hx : x 0) (n : ) :
              0 < x ^ n
              theorem NNReal.inv_lt_inv {x y : NNReal} (hx : x 0) (h : x < y) :
              @[simp]
              theorem NNReal.abs_eq (x : NNReal) :
              |x| = x
              theorem NNReal.le_toNNReal_of_coe_le {x : NNReal} {y : } (h : x y) :
              theorem NNReal.iSup_of_not_bddAbove {ι : Sort u_1} {f : ιNNReal} (hf : ¬BddAbove (Set.range f)) :
              ⨆ (i : ι), f i = 0
              theorem NNReal.iSup_empty {ι : Sort u_1} [IsEmpty ι] (f : ιNNReal) :
              ⨆ (i : ι), f i = 0
              theorem NNReal.iInf_empty {ι : Sort u_1} [IsEmpty ι] (f : ιNNReal) :
              ⨅ (i : ι), f i = 0
              @[simp]
              theorem NNReal.iSup_eq_zero {ι : Sort u_1} {f : ιNNReal} (hf : BddAbove (Set.range f)) :
              ⨆ (i : ι), f i = 0 ∀ (i : ι), f i = 0
              @[simp]
              theorem NNReal.iInf_const_zero {α : Sort u_2} :
              ⨅ (x : α), 0 = 0

              The absolute value on as a map to ℝ≥0.

              Equations
              Instances For
                @[simp]
                theorem Real.coe_nnabs (x : ) :
                (nnabs x) = |x|
                @[simp]
                theorem Real.nnabs_of_nonneg {x : } (h : 0 x) :
                theorem Real.nnabs_coe (x : NNReal) :
                nnabs x = x
                @[simp]
                theorem NNReal.exists_lt_of_strictMono {Γ₀ : Type u_1} [LinearOrderedCommGroupWithZero Γ₀] [h : Nontrivial Γ₀ˣ] {f : Γ₀ →*₀ NNReal} (hf : StrictMono f) {r : NNReal} (hr : 0 < r) :
                ∃ (d : Γ₀ˣ), f d < r

                If Γ₀ˣ is nontrivial and f : Γ₀ →*₀ ℝ≥0 is strictly monotone, then for any positive r : ℝ≥0, there exists d : Γ₀ˣ with f d < r.

                theorem Real.exists_lt_of_strictMono {Γ₀ : Type u_1} [LinearOrderedCommGroupWithZero Γ₀] [h : Nontrivial Γ₀ˣ] {f : Γ₀ →*₀ NNReal} (hf : StrictMono f) {r : } (hr : 0 < r) :
                ∃ (d : Γ₀ˣ), (f d) < r

                If Γ₀ˣ is nontrivial and f : Γ₀ →*₀ ℝ≥0 is strictly monotone, then for any positive real r, there exists d : Γ₀ˣ with f d < r.

                unsafe instance instReprNNReal :

                While not very useful, this instance uses the same representation as Real.instRepr.

                Equations

                Extension for the positivity tactic: cast from ℝ≥0 to .

                Instances For