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
      Equations

        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
                Equations
                  Equations
                    Equations
                      Equations
                        Equations
                          noncomputable instance ENNReal.instInv :
                          Equations
                            Equations
                              @[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.some_eq_coe (a : NNReal) :
                                      some a = a
                                      @[simp]
                                      theorem ENNReal.some_eq_coe' (a : NNReal) :
                                      a = a
                                      @[simp]
                                      theorem ENNReal.coe_inj {p q : NNReal} :
                                      p = q p = q
                                      theorem ENNReal.coe_ne_coe {p q : NNReal} :
                                      p q p q
                                      theorem ENNReal.coe_nnratCast (q : ℚ≥0) :
                                      q = 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
                                            Instances For

                                              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.coe_comp_toNNReal_comp {ι : Type u_2} {f : ιENNReal} (hf : ∀ (x : ι), f x ) :
                                                  (fun (x : NNReal) => x) ENNReal.toNNReal f = f
                                                  @[simp]
                                                  @[simp]
                                                  theorem ENNReal.toReal_ofReal {r : } (h : 0 r) :
                                                  @[simp]
                                                  @[simp]
                                                  theorem ENNReal.coe_zero :
                                                  0 = 0
                                                  @[simp]
                                                  theorem ENNReal.coe_one :
                                                  1 = 1
                                                  @[simp]
                                                  @[deprecated ENNReal.toNNReal_top (since := "2025-03-20")]

                                                  Alias of ENNReal.toNNReal_top.

                                                  @[deprecated ENNReal.toReal_top (since := "2025-03-20")]

                                                  Alias of ENNReal.toReal_top.

                                                  @[deprecated ENNReal.toReal_one (since := "2025-03-20")]

                                                  Alias of ENNReal.toReal_one.

                                                  @[deprecated ENNReal.toNNReal_one (since := "2025-03-20")]

                                                  Alias of ENNReal.toNNReal_one.

                                                  @[simp]
                                                  theorem ENNReal.coe_toReal (r : NNReal) :
                                                  (↑r).toReal = r
                                                  @[deprecated ENNReal.toNNReal_zero (since := "2025-03-20")]

                                                  Alias of ENNReal.toNNReal_zero.

                                                  @[deprecated ENNReal.toReal_zero (since := "2025-03-20")]

                                                  Alias of ENNReal.toReal_zero.

                                                  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
                                                  @[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]
                                                  @[simp]
                                                  @[simp]
                                                  @[simp]
                                                  @[simp]
                                                  @[simp]
                                                  theorem ENNReal.coe_le_coe {r q : NNReal} :
                                                  r q r q
                                                  @[simp]
                                                  theorem ENNReal.coe_lt_coe {r q : NNReal} :
                                                  r < q r < q
                                                  theorem ENNReal.coe_le_coe_of_le {r q : NNReal} :
                                                  r qr q

                                                  Alias of the reverse direction of ENNReal.coe_le_coe.

                                                  theorem ENNReal.coe_lt_coe_of_lt {r 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 y : NNReal) :
                                                  ↑(x + y) = x + y
                                                  @[simp]
                                                  theorem ENNReal.coe_mul (x 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_two :
                                                  2 = 2
                                                  theorem ENNReal.toNNReal_eq_toNNReal_iff' {x y : ENNReal} (hx : x ) (hy : y ) :
                                                  theorem ENNReal.toReal_eq_toReal_iff' {x y : ENNReal} (hx : x ) (hy : y ) :
                                                  x.toReal = y.toReal x = y

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

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

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

                                                  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.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.natCast_ne_top (n : ) :
                                                          n
                                                          @[simp]
                                                          theorem ENNReal.natCast_lt_top (n : ) :
                                                          n <
                                                          @[simp]
                                                          theorem ENNReal.top_ne_natCast (n : ) :
                                                          n
                                                          @[simp]
                                                          theorem ENNReal.natCast_le_ofNNReal {r : NNReal} {n : } :
                                                          n r n r
                                                          @[simp]
                                                          theorem ENNReal.ofNNReal_le_natCast {r : NNReal} {n : } :
                                                          r n r n
                                                          @[simp]
                                                          theorem ENNReal.ofNNReal_add_natCast (r : NNReal) (n : ) :
                                                          ↑(r + n) = r + n
                                                          @[simp]
                                                          theorem ENNReal.ofNNReal_natCast_add (n : ) (r : NNReal) :
                                                          ↑(n + r) = n + r
                                                          @[simp]
                                                          theorem ENNReal.ofNNReal_sub_natCast (r : NNReal) (n : ) :
                                                          ↑(r - n) = r - n
                                                          @[simp]
                                                          theorem ENNReal.ofNNReal_natCast_sub (n : ) (r : NNReal) :
                                                          ↑(n - r) = n - r
                                                          @[deprecated ENNReal.ofNat_ne_top (since := "2025-01-21")]
                                                          @[deprecated ENNReal.ofNat_lt_top (since := "2025-01-21")]
                                                          @[simp]
                                                          @[simp]
                                                          theorem ENNReal.toNNReal_natCast (n : ) :
                                                          (↑n).toNNReal = n
                                                          @[deprecated ENNReal.toNNReal_natCast (since := "2025-02-19")]
                                                          theorem ENNReal.toNNReal_nat (n : ) :
                                                          (↑n).toNNReal = n

                                                          Alias of ENNReal.toNNReal_natCast.

                                                          @[simp]
                                                          theorem ENNReal.toReal_natCast (n : ) :
                                                          (↑n).toReal = n
                                                          @[deprecated ENNReal.toReal_natCast (since := "2025-02-19")]
                                                          theorem ENNReal.toReal_nat (n : ) :
                                                          (↑n).toReal = n

                                                          Alias of ENNReal.toReal_natCast.

                                                          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 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.max_eq_zero_iff {a b : ENNReal} :
                                                          max a b = 0 a = 0 b = 0
                                                          theorem ENNReal.lt_iff_exists_rat_btwn {a b : ENNReal} :
                                                          a < b ∃ (q : ), 0 q a < (↑q).toNNReal (↑q).toNNReal < b
                                                          theorem ENNReal.lt_iff_exists_nnreal_btwn {a b : ENNReal} :
                                                          a < b ∃ (r : NNReal), a < r r < b
                                                          theorem ENNReal.lt_iff_exists_add_pos_lt {a b : ENNReal} :
                                                          a < b ∃ (r : NNReal), 0 < r a + r < b
                                                          theorem ENNReal.le_of_forall_pos_le_add {a 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
                                                          theorem ENNReal.exists_nat_gt {r : ENNReal} (h : r ) :
                                                          ∃ (n : ), r < n
                                                          @[simp]
                                                          @[simp]
                                                          @[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 p : NNReal) :
                                                          (min r p) = min r p
                                                          @[simp]
                                                          theorem ENNReal.coe_max (r p : NNReal) :
                                                          (max r p) = max r p
                                                          theorem ENNReal.le_of_top_imp_top_of_toNNReal_le {a b : ENNReal} (h : a = b = ) (h_nnreal : a b a.toNNReal b.toNNReal) :
                                                          a b
                                                          @[simp]
                                                          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 ι
                                                          unsafe instance instReprENNReal :

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

                                                          Equations

                                                            Extension for the positivity tactic: ENNReal.toReal.

                                                            Equations
                                                              Instances For