Documentation

Mathlib.Data.ENNReal.Basic

Extended non-negative reals #

We define ENNReal = ℝ≥0∞ := WithTop ℝ≥0 to be the type of extended nonnegative real numbers, i.e., the interval [0, +∞]. This type is used as the codomain of a MeasureTheory.Measure, and of the extended distance edist in an EMetricSpace.

In this file we set up many of the instances on ℝ≥0∞, and provide relationships between ℝ≥0∞ and ℝ≥0, and between ℝ≥0∞ and . In particular, we provide a coercion from ℝ≥0 to ℝ≥0∞ as well as functions ENNReal.toNNReal, ENNReal.ofReal and ENNReal.toReal, all of which take the value zero wherever they cannot be the identity. Also included is the relationship between ℝ≥0∞ and . The interaction of these functions, especially ENNReal.ofReal and ENNReal.toReal, with the algebraic and lattice structure can be found in Data.ENNReal.Real.

This file proves many of the order properties of ℝ≥0∞, with the exception of the ways those relate to the algebraic structure, which are included in Data.ENNReal.Operations. This file also defines inversion and division: this includes Inv and Div instances on ℝ≥0∞ making it into a DivInvOneMonoid. As a consequence of being a DivInvOneMonoid, ℝ≥0∞ inherits a power operation with integer exponent: this and other properties is shown in Data.ENNReal.Inv.

Main definitions #

Implementation notes #

We define a CanLift ℝ≥0∞ ℝ≥0 instance, so one of the ways to prove theorems about an ℝ≥0∞ number a is to consider the cases a = ∞ and a ≠ ∞, and use the tactic lift a to ℝ≥0 using ha in the second case. This instance is even more useful if one already has ha : a ≠ ∞ in the context, or if we have (f : α → ℝ≥0∞) (hf : ∀ x, f x ≠ ∞).

Notations #

The extended nonnegative real numbers. This is usually denoted [0, ∞], and is relevant as the codomain of a measure.

Equations
Instances For

    The extended nonnegative real numbers. This is usually denoted [0, ∞], and is relevant as the codomain of a measure.

    Equations
    Instances For

      Notation for infinity as an ENNReal number.

      Equations
      Instances For
        noncomputable instance ENNReal.instInv :
        Equations
        instance ENNReal.covariantClass_mul_le :
        CovariantClass ENNReal ENNReal (fun (x x_1 : ENNReal) => x * x_1) fun (x x_1 : ENNReal) => x x_1
        Equations
        instance ENNReal.covariantClass_add_le :
        CovariantClass ENNReal ENNReal (fun (x x_1 : ENNReal) => x + x_1) fun (x x_1 : ENNReal) => x x_1
        Equations
        Equations
        • One or more equations did not get rendered due to their size.
        @[match_pattern]

        Coercion from ℝ≥0 to ℝ≥0∞.

        Equations
        Instances For
          def ENNReal.recTopCoe {C : ENNRealSort u_2} (top : C ) (coe : (x : NNReal) → C x) (x : ENNReal) :
          C x

          A version of WithTop.recTopCoe that uses ENNReal.ofNNReal.

          Equations
          Instances For
            @[simp]
            theorem ENNReal.none_eq_top :
            none =
            @[simp]
            theorem ENNReal.some_eq_coe (a : NNReal) :
            some a = a
            @[simp]
            theorem ENNReal.some_eq_coe' (a : NNReal) :
            a = a
            @[simp]
            theorem ENNReal.coe_inj {p : NNReal} {q : NNReal} :
            p = q p = q
            theorem ENNReal.coe_ne_coe {p : NNReal} {q : NNReal} :
            p q p q

            toNNReal x returns x if it is real, otherwise 0.

            Equations
            Instances For

              toReal x returns x if it is real, 0 otherwise.

              Equations
              • a.toReal = a.toNNReal
              Instances For
                noncomputable def ENNReal.ofReal (r : ) :

                ofReal x returns x if it is nonnegative, 0 otherwise.

                Equations
                Instances For
                  @[simp]
                  theorem ENNReal.toNNReal_coe {r : NNReal} :
                  (r).toNNReal = r
                  @[simp]
                  theorem ENNReal.coe_toNNReal {a : ENNReal} :
                  a a.toNNReal = a
                  @[simp]
                  theorem ENNReal.ofReal_toReal {a : ENNReal} (h : a ) :
                  ENNReal.ofReal a.toReal = a
                  @[simp]
                  theorem ENNReal.toReal_ofReal {r : } (h : 0 r) :
                  (ENNReal.ofReal r).toReal = r
                  theorem ENNReal.toReal_ofReal' {r : } :
                  (ENNReal.ofReal r).toReal = max r 0
                  theorem ENNReal.coe_toNNReal_le_self {a : ENNReal} :
                  a.toNNReal a
                  theorem ENNReal.ofReal_eq_coe_nnreal {x : } (h : 0 x) :
                  ENNReal.ofReal x = x, h
                  @[simp]
                  @[simp]
                  theorem ENNReal.coe_zero :
                  0 = 0
                  @[simp]
                  theorem ENNReal.coe_one :
                  1 = 1
                  @[simp]
                  theorem ENNReal.toReal_nonneg {a : ENNReal} :
                  0 a.toReal
                  @[simp]
                  theorem ENNReal.top_toNNReal :
                  .toNNReal = 0
                  @[simp]
                  theorem ENNReal.top_toReal :
                  .toReal = 0
                  @[simp]
                  theorem ENNReal.coe_toReal (r : NNReal) :
                  (r).toReal = r
                  theorem ENNReal.forall_ennreal {p : ENNRealProp} :
                  (∀ (a : ENNReal), p a) (∀ (r : NNReal), p r) p
                  theorem ENNReal.forall_ne_top {p : ENNRealProp} :
                  (∀ (a : ENNReal), a p a) ∀ (r : NNReal), p r
                  theorem ENNReal.exists_ne_top {p : ENNRealProp} :
                  (∃ (a : ENNReal), a p a) ∃ (r : NNReal), p r
                  theorem ENNReal.toNNReal_eq_zero_iff (x : ENNReal) :
                  x.toNNReal = 0 x = 0 x =
                  theorem ENNReal.toReal_eq_zero_iff (x : ENNReal) :
                  x.toReal = 0 x = 0 x =
                  theorem ENNReal.toNNReal_ne_zero {a : ENNReal} :
                  a.toNNReal 0 a 0 a
                  theorem ENNReal.toReal_ne_zero {a : ENNReal} :
                  a.toReal 0 a 0 a
                  theorem ENNReal.toNNReal_eq_one_iff (x : ENNReal) :
                  x.toNNReal = 1 x = 1
                  theorem ENNReal.toReal_eq_one_iff (x : ENNReal) :
                  x.toReal = 1 x = 1
                  theorem ENNReal.toNNReal_ne_one {a : ENNReal} :
                  a.toNNReal 1 a 1
                  theorem ENNReal.toReal_ne_one {a : ENNReal} :
                  a.toReal 1 a 1
                  @[simp]
                  theorem ENNReal.coe_ne_top {r : NNReal} :
                  r
                  @[simp]
                  theorem ENNReal.top_ne_coe {r : NNReal} :
                  r
                  @[simp]
                  theorem ENNReal.coe_lt_top {r : NNReal} :
                  r <
                  @[simp]
                  theorem ENNReal.toReal_ofReal_eq_iff {a : } :
                  (ENNReal.ofReal a).toReal = a 0 a
                  @[simp]
                  @[simp]
                  @[simp]
                  @[simp]
                  @[simp]
                  @[simp]
                  theorem ENNReal.coe_le_coe {r : NNReal} {q : NNReal} :
                  r q r q
                  @[simp]
                  theorem ENNReal.coe_lt_coe {r : NNReal} {q : NNReal} :
                  r < q r < q
                  theorem ENNReal.coe_le_coe_of_le {r : NNReal} {q : NNReal} :
                  r qr q

                  Alias of the reverse direction of ENNReal.coe_le_coe.

                  theorem ENNReal.coe_lt_coe_of_lt {r : NNReal} {q : NNReal} :
                  r < qr < q

                  Alias of the reverse direction of ENNReal.coe_lt_coe.

                  @[simp]
                  theorem ENNReal.coe_eq_zero {r : NNReal} :
                  r = 0 r = 0
                  @[simp]
                  theorem ENNReal.zero_eq_coe {r : NNReal} :
                  0 = r 0 = r
                  @[simp]
                  theorem ENNReal.coe_eq_one {r : NNReal} :
                  r = 1 r = 1
                  @[simp]
                  theorem ENNReal.one_eq_coe {r : NNReal} :
                  1 = r 1 = r
                  @[simp]
                  theorem ENNReal.coe_pos {r : NNReal} :
                  0 < r 0 < r
                  theorem ENNReal.coe_ne_zero {r : NNReal} :
                  r 0 r 0
                  theorem ENNReal.coe_ne_one {r : NNReal} :
                  r 1 r 1
                  @[simp]
                  theorem ENNReal.coe_add (x : NNReal) (y : NNReal) :
                  (x + y) = x + y
                  @[simp]
                  theorem ENNReal.coe_mul (x : NNReal) (y : NNReal) :
                  (x * y) = x * y
                  theorem ENNReal.coe_nsmul (n : ) (x : NNReal) :
                  (n x) = n x
                  @[simp]
                  theorem ENNReal.coe_pow (x : NNReal) (n : ) :
                  (x ^ n) = x ^ n
                  @[simp]
                  theorem ENNReal.coe_ofNat (n : ) [n.AtLeastTwo] :
                  theorem ENNReal.coe_two :
                  2 = 2
                  theorem ENNReal.toNNReal_eq_toNNReal_iff (x : ENNReal) (y : ENNReal) :
                  x.toNNReal = y.toNNReal x = y x = 0 y = x = y = 0
                  theorem ENNReal.toReal_eq_toReal_iff (x : ENNReal) (y : ENNReal) :
                  x.toReal = y.toReal x = y x = 0 y = x = y = 0
                  theorem ENNReal.toNNReal_eq_toNNReal_iff' {x : ENNReal} {y : ENNReal} (hx : x ) (hy : y ) :
                  x.toNNReal = y.toNNReal x = y
                  theorem ENNReal.toReal_eq_toReal_iff' {x : ENNReal} {y : ENNReal} (hx : x ) (hy : y ) :
                  x.toReal = y.toReal x = y
                  @[simp]
                  @[simp]

                  (1 : ℝ≥0∞) ≤ 1, recorded as a Fact for use with Lp spaces.

                  Equations

                  (1 : ℝ≥0∞) ≤ 2, recorded as a Fact for use with Lp spaces.

                  Equations

                  (1 : ℝ≥0∞) ≤ ∞, recorded as a Fact for use with Lp spaces.

                  Equations

                  The set of numbers in ℝ≥0∞ that are not equal to is equivalent to ℝ≥0.

                  Equations
                  Instances For
                    theorem ENNReal.cinfi_ne_top {α : Type u_1} [InfSet α] (f : ENNRealα) :
                    ⨅ (x : { x : ENNReal // x }), f x = ⨅ (x : NNReal), f x
                    theorem ENNReal.iInf_ne_top {α : Type u_1} [CompleteLattice α] (f : ENNRealα) :
                    ⨅ (x : ENNReal), ⨅ (_ : x ), f x = ⨅ (x : NNReal), f x
                    theorem ENNReal.csupr_ne_top {α : Type u_1} [SupSet α] (f : ENNRealα) :
                    ⨆ (x : { x : ENNReal // x }), f x = ⨆ (x : NNReal), f x
                    theorem ENNReal.iSup_ne_top {α : Type u_1} [CompleteLattice α] (f : ENNRealα) :
                    ⨆ (x : ENNReal), ⨆ (_ : x ), f x = ⨆ (x : NNReal), f x
                    theorem ENNReal.iInf_ennreal {α : Type u_2} [CompleteLattice α] {f : ENNRealα} :
                    ⨅ (n : ENNReal), f n = (⨅ (n : NNReal), f n) f
                    theorem ENNReal.iSup_ennreal {α : Type u_2} [CompleteLattice α] {f : ENNRealα} :
                    ⨆ (n : ENNReal), f n = (⨆ (n : NNReal), f n) f

                    Coercion ℝ≥0 → ℝ≥0∞ as a RingHom.

                    Equations
                    Instances For
                      @[simp]
                      theorem ENNReal.coe_indicator {α : Type u_2} (s : Set α) (f : αNNReal) (a : α) :
                      (s.indicator f a) = s.indicator (fun (x : α) => (f x)) a
                      @[simp]
                      theorem ENNReal.one_le_coe_iff {r : NNReal} :
                      1 r 1 r
                      @[simp]
                      theorem ENNReal.coe_le_one_iff {r : NNReal} :
                      r 1 r 1
                      @[simp]
                      theorem ENNReal.coe_lt_one_iff {p : NNReal} :
                      p < 1 p < 1
                      @[simp]
                      theorem ENNReal.one_lt_coe_iff {p : NNReal} :
                      1 < p 1 < p
                      @[simp]
                      theorem ENNReal.coe_natCast (n : ) :
                      n = n
                      @[simp]
                      theorem ENNReal.ofReal_natCast (n : ) :
                      ENNReal.ofReal n = n
                      @[simp]
                      theorem ENNReal.ofReal_ofNat (n : ) [n.AtLeastTwo] :
                      @[simp]
                      theorem ENNReal.natCast_ne_top (n : ) :
                      n
                      @[simp]
                      theorem ENNReal.top_ne_natCast (n : ) :
                      n
                      @[simp]
                      @[simp]
                      theorem ENNReal.toNNReal_nat (n : ) :
                      (n).toNNReal = n
                      @[simp]
                      theorem ENNReal.toReal_nat (n : ) :
                      (n).toReal = n
                      @[simp]
                      theorem ENNReal.toReal_ofNat (n : ) [n.AtLeastTwo] :
                      theorem ENNReal.le_coe_iff {a : ENNReal} {r : NNReal} :
                      a r ∃ (p : NNReal), a = p p r
                      theorem ENNReal.coe_le_iff {a : ENNReal} {r : NNReal} :
                      r a ∀ (p : NNReal), a = pr p
                      theorem ENNReal.lt_iff_exists_coe {a : ENNReal} {b : ENNReal} :
                      a < b ∃ (p : NNReal), a = p p < b
                      theorem ENNReal.toReal_le_coe_of_le_coe {a : ENNReal} {b : NNReal} (h : a b) :
                      a.toReal b
                      @[simp]
                      theorem ENNReal.coe_finset_sup {α : Type u_1} {s : Finset α} {f : αNNReal} :
                      (s.sup f) = s.sup fun (x : α) => (f x)
                      @[simp]
                      theorem ENNReal.max_eq_zero_iff {a : ENNReal} {b : ENNReal} :
                      max a b = 0 a = 0 b = 0
                      @[simp]
                      theorem ENNReal.sup_eq_max {a : ENNReal} {b : ENNReal} :
                      a b = max a b
                      theorem ENNReal.lt_iff_exists_rat_btwn {a : ENNReal} {b : ENNReal} :
                      a < b ∃ (q : ), 0 q a < (q).toNNReal (q).toNNReal < b
                      theorem ENNReal.lt_iff_exists_nnreal_btwn {a : ENNReal} {b : ENNReal} :
                      a < b ∃ (r : NNReal), a < r r < b
                      theorem ENNReal.lt_iff_exists_add_pos_lt {a : ENNReal} {b : ENNReal} :
                      a < b ∃ (r : NNReal), 0 < r a + r < b
                      theorem ENNReal.le_of_forall_pos_le_add {a : ENNReal} {b : ENNReal} (h : ∀ (ε : NNReal), 0 < εb < a b + ε) :
                      a b
                      theorem ENNReal.natCast_lt_coe {r : NNReal} {n : } :
                      n < r n < r
                      theorem ENNReal.coe_lt_natCast {r : NNReal} {n : } :
                      r < n r < n
                      @[deprecated ENNReal.coe_natCast]
                      theorem ENNReal.coe_nat (n : ) :
                      n = n

                      Alias of ENNReal.coe_natCast.

                      @[deprecated ENNReal.ofReal_natCast]
                      theorem ENNReal.ofReal_coe_nat (n : ) :
                      ENNReal.ofReal n = n

                      Alias of ENNReal.ofReal_natCast.

                      @[deprecated ENNReal.natCast_ne_top]
                      theorem ENNReal.nat_ne_top (n : ) :
                      n

                      Alias of ENNReal.natCast_ne_top.

                      @[deprecated ENNReal.top_ne_natCast]
                      theorem ENNReal.top_ne_nat (n : ) :
                      n

                      Alias of ENNReal.top_ne_natCast.

                      @[deprecated ENNReal.natCast_lt_coe]
                      theorem ENNReal.coe_nat_lt_coe {r : NNReal} {n : } :
                      n < r n < r

                      Alias of ENNReal.natCast_lt_coe.

                      @[deprecated ENNReal.coe_lt_natCast]
                      theorem ENNReal.coe_lt_coe_nat {r : NNReal} {n : } :
                      r < n r < n

                      Alias of ENNReal.coe_lt_natCast.

                      theorem ENNReal.exists_nat_gt {r : ENNReal} (h : r ) :
                      ∃ (n : ), r < n
                      @[simp]
                      theorem ENNReal.iUnion_Iio_coe_nat :
                      ⋃ (n : ), Set.Iio n = {}
                      @[simp]
                      theorem ENNReal.iUnion_Iic_coe_nat :
                      ⋃ (n : ), Set.Iic n = {}
                      @[simp]
                      theorem ENNReal.iUnion_Ioc_coe_nat {a : ENNReal} :
                      ⋃ (n : ), Set.Ioc a n = Set.Ioi a \ {}
                      @[simp]
                      theorem ENNReal.iUnion_Ioo_coe_nat {a : ENNReal} :
                      ⋃ (n : ), Set.Ioo a n = Set.Ioi a \ {}
                      @[simp]
                      theorem ENNReal.iUnion_Icc_coe_nat {a : ENNReal} :
                      ⋃ (n : ), Set.Icc a n = Set.Ici a \ {}
                      @[simp]
                      theorem ENNReal.iUnion_Ico_coe_nat {a : ENNReal} :
                      ⋃ (n : ), Set.Ico a n = Set.Ici a \ {}
                      @[simp]
                      theorem ENNReal.iInter_Ici_coe_nat :
                      ⋂ (n : ), Set.Ici n = {}
                      @[simp]
                      theorem ENNReal.iInter_Ioi_coe_nat :
                      ⋂ (n : ), Set.Ioi n = {}
                      @[simp]
                      theorem ENNReal.coe_min (r : NNReal) (p : NNReal) :
                      (min r p) = min r p
                      @[simp]
                      theorem ENNReal.coe_max (r : NNReal) (p : NNReal) :
                      (max r p) = max r p
                      theorem ENNReal.le_of_top_imp_top_of_toNNReal_le {a : ENNReal} {b : ENNReal} (h : a = b = ) (h_nnreal : a b a.toNNReal b.toNNReal) :
                      a b
                      @[simp]
                      theorem ENNReal.abs_toReal {x : ENNReal} :
                      |x.toReal| = x.toReal
                      theorem ENNReal.coe_sSup {s : Set NNReal} :
                      BddAbove s(sSup s) = as, a
                      theorem ENNReal.coe_sInf {s : Set NNReal} (hs : s.Nonempty) :
                      (sInf s) = as, a
                      theorem ENNReal.coe_iSup {ι : Sort u_3} {f : ιNNReal} (hf : BddAbove (Set.range f)) :
                      (iSup f) = ⨆ (a : ι), (f a)
                      theorem ENNReal.coe_iInf {ι : Sort u_3} [Nonempty ι] (f : ιNNReal) :
                      (iInf f) = ⨅ (a : ι), (f a)
                      theorem ENNReal.iSup_coe_eq_top {ι : Sort u_2} {f : ιNNReal} :
                      ⨆ (i : ι), (f i) = ¬BddAbove (Set.range f)
                      theorem ENNReal.iSup_coe_lt_top {ι : Sort u_2} {f : ιNNReal} :
                      ⨆ (i : ι), (f i) < BddAbove (Set.range f)
                      theorem ENNReal.iInf_coe_eq_top {ι : Sort u_2} {f : ιNNReal} :
                      ⨅ (i : ι), (f i) = IsEmpty ι
                      theorem ENNReal.iInf_coe_lt_top {ι : Sort u_2} {f : ιNNReal} :
                      ⨅ (i : ι), (f i) < Nonempty ι
                      theorem Set.OrdConnected.preimage_coe_nnreal_ennreal {u : Set ENNReal} (h : u.OrdConnected) :
                      (ENNReal.ofNNReal ⁻¹' u).OrdConnected
                      theorem Set.OrdConnected.image_coe_nnreal_ennreal {t : Set NNReal} (h : t.OrdConnected) :
                      (ENNReal.ofNNReal '' t).OrdConnected
                      theorem Set.OrdConnected.preimage_ennreal_ofReal {u : Set ENNReal} (h : u.OrdConnected) :
                      (ENNReal.ofReal ⁻¹' u).OrdConnected
                      theorem Set.OrdConnected.image_ennreal_ofReal {s : Set } (h : s.OrdConnected) :
                      (ENNReal.ofReal '' s).OrdConnected
                      @[deprecated le_inv_smul_iff_of_pos]
                      theorem ENNReal.le_inv_smul_iff_of_pos {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [GroupWithZero α] [Preorder α] [Preorder β] [MulAction α β] [PosSMulMono α β] [PosSMulReflectLE α β] (ha : 0 < a) :
                      b₁ a⁻¹ b₂ a b₁ b₂

                      Alias of le_inv_smul_iff_of_pos.

                      @[deprecated inv_smul_le_iff_of_pos]
                      theorem ENNReal.inv_smul_le_iff_of_pos {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [GroupWithZero α] [Preorder α] [Preorder β] [MulAction α β] [PosSMulMono α β] [PosSMulReflectLE α β] (ha : 0 < a) :
                      a⁻¹ b₁ b₂ b₁ a b₂

                      Alias of inv_smul_le_iff_of_pos.