Documentation

Mathlib.Data.Real.NNReal

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.

Equations
Instances For
    noncomputable instance NNReal.instSubNNReal :
    Equations

    Coercion ℝ≥0 → ℝ.

    Equations
    Instances For
      @[simp]
      theorem NNReal.val_eq_coe (n : NNReal) :
      n = n
      instance NNReal.canLift :
      Equations
      theorem NNReal.eq {n : NNReal} {m : NNReal} :
      n = mn = m
      theorem NNReal.eq_iff {n : NNReal} {m : NNReal} :
      n = m n = m
      theorem NNReal.ne_iff {x : NNReal} {y : NNReal} :
      x y x y
      theorem NNReal.forall {p : NNRealProp} :
      (∀ (x : NNReal), p x) ∀ (x : ) (hx : 0 x), p { val := x, property := hx }
      theorem NNReal.exists {p : NNRealProp} :
      (∃ (x : NNReal), p x) ∃ (x : ) (hx : 0 x), p { val := x, property := hx }
      noncomputable def Real.toNNReal (r : ) :

      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) :
        (Real.toNNReal r) = r
        theorem Real.toNNReal_of_nonneg {r : } (hr : 0 r) :
        Real.toNNReal r = { val := r, property := hr }
        theorem NNReal.coe_nonneg (r : NNReal) :
        0 r
        @[simp]
        theorem NNReal.coe_mk (a : ) (ha : 0 a) :
        { val := a, property := ha } = a
        @[simp]
        theorem NNReal.coe_eq {r₁ : NNReal} {r₂ : NNReal} :
        r₁ = r₂ r₁ = r₂
        @[simp]
        theorem NNReal.coe_zero :
        0 = 0
        @[simp]
        theorem NNReal.coe_one :
        1 = 1
        @[simp]
        theorem NNReal.coe_add (r₁ : NNReal) (r₂ : NNReal) :
        (r₁ + r₂) = r₁ + r₂
        @[simp]
        theorem NNReal.coe_mul (r₁ : NNReal) (r₂ : NNReal) :
        (r₁ * r₂) = r₁ * r₂
        @[simp]
        theorem NNReal.coe_inv (r : NNReal) :
        r⁻¹ = (r)⁻¹
        @[simp]
        theorem NNReal.coe_div (r₁ : NNReal) (r₂ : NNReal) :
        (r₁ / r₂) = r₁ / r₂
        theorem NNReal.coe_two :
        2 = 2
        @[simp]
        theorem NNReal.coe_sub {r₁ : NNReal} {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

        Coercion ℝ≥0 → ℝ as a RingHom.

        Porting note: todo: what if we define Coe ℝ≥0 ℝ using this function?

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

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

          Equations
          theorem NNReal.smul_def {M : Type u_1} [MulAction M] (c : NNReal) (x : M) :
          c x = c x
          instance NNReal.smulCommClass_left {M : Type u_1} {N : Type u_2} [MulAction N] [SMul M N] [SMulCommClass M N] :
          Equations
          instance NNReal.smulCommClass_right {M : Type u_1} {N : Type u_2} [MulAction N] [SMul M N] [SMulCommClass M N] :
          Equations

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

          Equations

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

          Equations

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

          Equations
          • One or more equations did not get rendered due to their size.
          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem NNReal.coe_indicator {α : Type u_1} (s : Set α) (f : αNNReal) (a : α) :
          (Set.indicator s f a) = Set.indicator s (fun (x : α) => (f x)) a
          @[simp]
          theorem NNReal.coe_pow (r : NNReal) (n : ) :
          (r ^ n) = r ^ n
          @[simp]
          theorem NNReal.coe_zpow (r : NNReal) (n : ) :
          (r ^ n) = r ^ n
          theorem NNReal.coe_sum {α : Type u_1} {s : Finset α} {f : αNNReal} :
          (Finset.sum s fun (a : α) => f a) = Finset.sum s fun (a : α) => (f a)
          theorem Real.toNNReal_sum_of_nonneg {α : Type u_1} {s : Finset α} {f : α} (hf : as, 0 f a) :
          Real.toNNReal (Finset.sum s fun (a : α) => f a) = Finset.sum s fun (a : α) => Real.toNNReal (f a)
          theorem NNReal.coe_prod {α : Type u_1} {s : Finset α} {f : αNNReal} :
          (Finset.prod s fun (a : α) => f a) = Finset.prod s fun (a : α) => (f a)
          theorem Real.toNNReal_prod_of_nonneg {α : Type u_1} {s : Finset α} {f : α} (hf : as, 0 f a) :
          Real.toNNReal (Finset.prod s fun (a : α) => f a) = Finset.prod s fun (a : α) => Real.toNNReal (f a)
          theorem NNReal.coe_nsmul (r : NNReal) (n : ) :
          (n r) = n r
          @[simp]
          theorem NNReal.coe_nat_cast (n : ) :
          n = n
          @[simp]
          theorem NNReal.coe_le_coe {r₁ : NNReal} {r₂ : NNReal} :
          r₁ r₂ r₁ r₂
          @[simp]
          theorem NNReal.coe_lt_coe {r₁ : NNReal} {r₂ : NNReal} :
          r₁ < r₂ r₁ < r₂
          @[simp]
          theorem NNReal.coe_pos {r : NNReal} :
          0 < r 0 < r
          theorem NNReal.toReal_le_toReal {x : NNReal} {y : NNReal} (h : x y) :
          x y
          @[simp]
          theorem Real.toNNReal_coe {r : NNReal} :
          @[simp]
          theorem NNReal.mk_coe_nat (n : ) :
          { val := n, property := (_ : 0 n) } = n
          @[simp]
          theorem NNReal.toNNReal_coe_nat (n : ) :
          Real.toNNReal n = 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
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem NNReal.orderIsoIccZeroCoe_apply_coe_coe (a : NNReal) (b : (Set.Icc 0 a)) :
            ((NNReal.orderIsoIccZeroCoe a) b) = b
            theorem NNReal.coe_image {s : Set NNReal} :
            NNReal.toReal '' s = {x : | ∃ (h : 0 x), { val := x, property := h } s}
            @[simp]
            theorem NNReal.coe_iSup {ι : Sort u_1} (s : ιNNReal) :
            (⨆ (i : ι), s i) = ⨆ (i : ι), (s i)
            @[simp]
            theorem NNReal.coe_iInf {ι : Sort u_1} (s : ιNNReal) :
            (⨅ (i : ι), s i) = ⨅ (i : ι), (s i)
            theorem NNReal.le_iInf_add_iInf {ι : Sort u_1} {ι' : Sort u_2} [Nonempty ι] [Nonempty ι'] {f : ιNNReal} {g : ι'NNReal} {a : NNReal} (h : ∀ (i : ι) (j : ι'), a f i + g j) :
            a (⨅ (i : ι), f i) + ⨅ (j : ι'), g j
            instance NNReal.covariant_add :
            CovariantClass NNReal NNReal (fun (x x_1 : NNReal) => x + x_1) fun (x x_1 : NNReal) => x x_1
            Equations
            instance NNReal.contravariant_add :
            ContravariantClass NNReal NNReal (fun (x x_1 : NNReal) => x + x_1) fun (x x_1 : NNReal) => x < x_1
            Equations
            instance NNReal.covariant_mul :
            CovariantClass NNReal NNReal (fun (x x_1 : NNReal) => x * x_1) fun (x x_1 : NNReal) => x x_1
            Equations
            theorem NNReal.le_of_forall_pos_le_add {a : NNReal} {b : NNReal} (h : ∀ (ε : NNReal), 0 < εa b + ε) :
            a b
            theorem NNReal.lt_iff_exists_rat_btwn (a : NNReal) (b : NNReal) :
            a < b ∃ (q : ), 0 q a < Real.toNNReal q Real.toNNReal q < b
            theorem NNReal.mul_sup (a : NNReal) (b : NNReal) (c : NNReal) :
            a * (b c) = a * b a * c
            theorem NNReal.sup_mul (a : NNReal) (b : NNReal) (c : NNReal) :
            (a b) * c = a * c b * c
            theorem NNReal.mul_finset_sup {α : Type u_1} (r : NNReal) (s : Finset α) (f : αNNReal) :
            r * Finset.sup s f = Finset.sup s fun (a : α) => r * f a
            theorem NNReal.finset_sup_mul {α : Type u_1} (s : Finset α) (f : αNNReal) (r : NNReal) :
            Finset.sup s f * r = Finset.sup s fun (a : α) => f a * r
            theorem NNReal.finset_sup_div {α : Type u_1} {f : αNNReal} {s : Finset α} (r : NNReal) :
            Finset.sup s f / r = Finset.sup s fun (a : α) => f a / r
            @[simp]
            theorem NNReal.coe_max (x : NNReal) (y : NNReal) :
            (max x y) = max x y
            @[simp]
            theorem NNReal.coe_min (x : NNReal) (y : NNReal) :
            (min x y) = min x y
            @[simp]
            theorem NNReal.zero_le_coe {q : NNReal} :
            0 q
            @[simp]
            theorem Real.coe_toNNReal' (r : ) :
            (Real.toNNReal r) = max r 0
            @[simp]
            theorem Real.toNNReal_pos {r : } :
            @[simp]
            theorem Real.toNNReal_eq_iff_eq_coe {r : } {p : NNReal} (hp : p 0) :
            Real.toNNReal r = p r = p
            @[simp]
            theorem Real.toNNReal_eq_one {r : } :
            @[simp]
            theorem Real.toNNReal_eq_nat_cast {r : } {n : } (hn : n 0) :
            Real.toNNReal r = n r = n
            @[simp]
            @[simp]
            @[simp]
            theorem Real.one_lt_toNNReal {r : } :
            @[simp]
            theorem Real.toNNReal_le_nat_cast {r : } {n : } :
            Real.toNNReal r n r n
            @[simp]
            theorem Real.nat_cast_lt_toNNReal {r : } {n : } :
            n < Real.toNNReal r n < r
            @[simp]
            @[simp]
            theorem Real.toNNReal_eq_toNNReal_iff {r : } {p : } (hr : 0 r) (hp : 0 p) :
            @[simp]
            @[simp]
            theorem Real.toNNReal_lt_one {r : } :
            @[simp]
            theorem Real.nat_cast_le_toNNReal' {n : } {r : } :
            n Real.toNNReal r n r n = 0
            @[simp]
            theorem Real.toNNReal_lt_nat_cast' {n : } {r : } :
            Real.toNNReal r < n r < n n 0
            theorem Real.nat_cast_le_toNNReal {n : } {r : } (hn : n 0) :
            n Real.toNNReal r n r
            theorem Real.toNNReal_lt_nat_cast {r : } {n : } (hn : n 0) :
            Real.toNNReal r < 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) :
            theorem Real.le_toNNReal_iff_coe_le' {r : NNReal} {p : } (hr : 0 < r) :
            theorem Real.toNNReal_lt_iff_lt_coe {r : } {p : NNReal} (ha : 0 r) :
            Real.toNNReal r < p r < p
            theorem Real.toNNReal_pow {x : } (hx : 0 x) (n : ) :
            theorem Real.toNNReal_mul {p : } {q : } (hp : 0 p) :
            theorem NNReal.mul_eq_mul_left {a : NNReal} {b : NNReal} {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 : NNReal} {b : NNReal} (ha : 0 < a) (hb : b < 1) :
            ∃ (n : ), b ^ n < a
            theorem NNReal.exists_mem_Ico_zpow {x : NNReal} {y : NNReal} (hx : x 0) (hy : 1 < y) :
            ∃ (n : ), x Set.Ico (y ^ n) (y ^ (n + 1))
            theorem NNReal.exists_mem_Ioc_zpow {x : NNReal} {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 : NNReal} {p : NNReal} :
            r - p = Real.toNNReal (r - p)
            theorem NNReal.coe_sub_def {r : NNReal} {p : NNReal} :
            (r - p) = max (r - p) 0
            theorem NNReal.sub_div (a : NNReal) (b : NNReal) (c : NNReal) :
            (a - b) / c = a / c - b / c
            @[simp]
            theorem NNReal.inv_le {r : NNReal} {p : NNReal} (h : r 0) :
            r⁻¹ p 1 r * p
            theorem NNReal.inv_le_of_le_mul {r : NNReal} {p : NNReal} (h : 1 r * p) :
            @[simp]
            theorem NNReal.le_inv_iff_mul_le {r : NNReal} {p : NNReal} (h : p 0) :
            r p⁻¹ r * p 1
            @[simp]
            theorem NNReal.lt_inv_iff_mul_lt {r : NNReal} {p : NNReal} (h : p 0) :
            r < p⁻¹ r * p < 1
            theorem NNReal.mul_le_iff_le_inv {a : NNReal} {b : NNReal} {r : NNReal} (hr : r 0) :
            r * a b a r⁻¹ * b
            theorem NNReal.le_div_iff_mul_le {a : NNReal} {b : NNReal} {r : NNReal} (hr : r 0) :
            a b / r a * r b
            theorem NNReal.div_le_iff {a : NNReal} {b : NNReal} {r : NNReal} (hr : r 0) :
            a / r b a b * r
            theorem NNReal.div_le_iff' {a : NNReal} {b : NNReal} {r : NNReal} (hr : r 0) :
            a / r b a r * b
            theorem NNReal.div_le_of_le_mul {a : NNReal} {b : NNReal} {c : NNReal} (h : a b * c) :
            a / c b
            theorem NNReal.div_le_of_le_mul' {a : NNReal} {b : NNReal} {c : NNReal} (h : a b * c) :
            a / b c
            theorem NNReal.le_div_iff {a : NNReal} {b : NNReal} {r : NNReal} (hr : r 0) :
            a b / r a * r b
            theorem NNReal.le_div_iff' {a : NNReal} {b : NNReal} {r : NNReal} (hr : r 0) :
            a b / r r * a b
            theorem NNReal.div_lt_iff {a : NNReal} {b : NNReal} {r : NNReal} (hr : r 0) :
            a / r < b a < b * r
            theorem NNReal.div_lt_iff' {a : NNReal} {b : NNReal} {r : NNReal} (hr : r 0) :
            a / r < b a < r * b
            theorem NNReal.lt_div_iff {a : NNReal} {b : NNReal} {r : NNReal} (hr : r 0) :
            a < b / r a * r < b
            theorem NNReal.lt_div_iff' {a : NNReal} {b : NNReal} {r : NNReal} (hr : r 0) :
            a < b / r r * a < b
            theorem NNReal.mul_lt_of_lt_div {a : NNReal} {b : NNReal} {r : NNReal} (h : a < b / r) :
            a * r < b
            theorem NNReal.div_le_div_left_of_le {a : NNReal} {b : NNReal} {c : NNReal} (c0 : c 0) (cb : c b) :
            a / b a / c
            theorem NNReal.div_le_div_left {a : NNReal} {b : NNReal} {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 : NNReal} {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 : NNReal} {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
            theorem NNReal.zpow_pos {x : NNReal} (hx : x 0) (n : ) :
            0 < x ^ n
            theorem NNReal.inv_lt_inv {x : NNReal} {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.iInf_const_zero {α : Sort u_2} :
            ⨅ (x : α), 0 = 0
            theorem NNReal.iInf_mul {ι : Sort u_1} (f : ιNNReal) (a : NNReal) :
            iInf f * a = ⨅ (i : ι), f i * a
            theorem NNReal.mul_iInf {ι : Sort u_1} (f : ιNNReal) (a : NNReal) :
            a * iInf f = ⨅ (i : ι), a * f i
            theorem NNReal.mul_iSup {ι : Sort u_1} (f : ιNNReal) (a : NNReal) :
            a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i
            theorem NNReal.iSup_mul {ι : Sort u_1} (f : ιNNReal) (a : NNReal) :
            (⨆ (i : ι), f i) * a = ⨆ (i : ι), f i * a
            theorem NNReal.iSup_div {ι : Sort u_1} (f : ιNNReal) (a : NNReal) :
            (⨆ (i : ι), f i) / a = ⨆ (i : ι), f i / a
            theorem NNReal.mul_iSup_le {ι : Sort u_1} {a : NNReal} {g : NNReal} {h : ιNNReal} (H : ∀ (j : ι), g * h j a) :
            g * iSup h a
            theorem NNReal.iSup_mul_le {ι : Sort u_1} {a : NNReal} {g : ιNNReal} {h : NNReal} (H : ∀ (i : ι), g i * h a) :
            iSup g * h a
            theorem NNReal.iSup_mul_iSup_le {ι : Sort u_1} {a : NNReal} {g : ιNNReal} {h : ιNNReal} (H : ∀ (i j : ι), g i * h j a) :
            iSup g * iSup h a
            theorem NNReal.le_mul_iInf {ι : Sort u_1} [Nonempty ι] {a : NNReal} {g : NNReal} {h : ιNNReal} (H : ∀ (j : ι), a g * h j) :
            a g * iInf h
            theorem NNReal.le_iInf_mul {ι : Sort u_1} [Nonempty ι] {a : NNReal} {g : ιNNReal} {h : NNReal} (H : ∀ (i : ι), a g i * h) :
            a iInf g * h
            theorem NNReal.le_iInf_mul_iInf {ι : Sort u_1} [Nonempty ι] {a : NNReal} {g : ιNNReal} {h : ιNNReal} (H : ∀ (i j : ι), a g i * h j) :
            a iInf g * iInf h

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

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem Real.coe_nnabs (x : ) :
              (Real.nnabs x) = |x|
              @[simp]
              theorem Real.nnabs_of_nonneg {x : } (h : 0 x) :
              theorem Real.nnabs_coe (x : NNReal) :
              Real.nnabs x = x

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

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