Documentation

Mathlib.Data.Real.EReal

The extended reals [-∞, ∞]. #

This file defines EReal, the real numbers together with a top and bottom element, referred to as ⊤ and ⊥. It is implemented as WithBot (WithTop ℝ)

Addition and multiplication are problematic in the presence of ±∞, but negation has a natural definition and satisfies the usual properties.

An ad hoc addition is defined, for which EReal is an AddCommMonoid, and even an ordered one (if a ≤ a' and b ≤ b' then a + b ≤ a' + b'). Note however that addition is badly behaved at (⊥, ⊤) and (⊤, ⊥) so this can not be upgraded to a group structure. Our choice is that ⊥ + ⊤ = ⊤ + ⊥ = ⊥, to make sure that the exponential and the logarithm between EReal and ℝ≥0∞ respect the operations (notice that the convention 0 * ∞ = 0 on ℝ≥0∞ is enforced by measure theory).

An ad hoc subtraction is then defined by x - y = x + (-y). It does not have nice properties, but it is sometimes convenient to have.

An ad hoc multiplication is defined, for which EReal is a CommMonoidWithZero. We make the choice that 0 * x = x * 0 = 0 for any x (while the other cases are defined non-ambiguously). This does not distribute with addition, as ⊥ = ⊥ + ⊤ = 1*⊥ + (-1)*⊥ ≠ (1 - 1) * ⊥ = 0 * ⊥ = 0.

EReal is a CompleteLinearOrder; this is deduced by type class inference from the fact that WithBot (WithTop L) is a complete linear order if L is a conditionally complete linear order.

Coercions from and from ℝ≥0∞ are registered, and their basic properties are proved. The main one is the real coercion, and is usually referred to just as coe (lemmas such as EReal.coe_add deal with this coercion). The one from ENNReal is usually called coe_ennreal in the EReal namespace.

We define an absolute value EReal.abs from EReal to ℝ≥0∞. Two elements of EReal coincide if and only if they have the same absolute value and the same sign.

Tags #

real, ereal, complete lattice

def EReal :

ereal : The type [-∞, ∞]

Equations
Instances For

    The canonical inclusion from reals to ereals. Registered as a coercion.

    Equations
    Instances For
      instance EReal.decidableLT :
      DecidableRel fun (x x_1 : EReal) => x < x_1
      Equations
      @[simp]
      theorem EReal.coe_le_coe_iff {x : } {y : } :
      x y x y
      @[simp]
      theorem EReal.coe_lt_coe_iff {x : } {y : } :
      x < y x < y
      @[simp]
      theorem EReal.coe_eq_coe_iff {x : } {y : } :
      x = y x = y
      theorem EReal.coe_ne_coe_iff {x : } {y : } :
      x y x y

      The canonical map from nonnegative extended reals to extended reals

      Equations
      • x = match x with | none => | some x => x
      Instances For
        @[simp]
        theorem EReal.coe_zero :
        0 = 0
        @[simp]
        theorem EReal.coe_one :
        1 = 1
        def EReal.rec {C : ERealSort u_1} (h_bot : C ) (h_real : (a : ) → C a) (h_top : C ) (a : EReal) :
        C a

        A recursor for EReal in terms of the coercion.

        A typical invocation looks like induction x using EReal.rec. Note that using induction directly will unfold EReal to Option which is undesirable.

        When working in term mode, note that pattern matching can be used directly.

        Equations
        • EReal.rec h_bot h_real h_top x = match x with | none => h_bot | some (some a) => h_real a | some none => h_top
        Instances For
          def EReal.mul :
          ERealERealEReal

          The multiplication on EReal. Our definition satisfies 0 * x = x * 0 = 0 for any x, and picks the only sensible value elsewhere.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem EReal.coe_mul (x : ) (y : ) :
            (x * y) = x * y
            theorem EReal.induction₂ {P : ERealERealProp} (top_top : P ) (top_pos : ∀ (x : ), 0 < xP x) (top_zero : P 0) (top_neg : x < 0, P x) (top_bot : P ) (pos_top : ∀ (x : ), 0 < xP x ) (pos_bot : ∀ (x : ), 0 < xP x ) (zero_top : P 0 ) (coe_coe : ∀ (x y : ), P x y) (zero_bot : P 0 ) (neg_top : x < 0, P x ) (neg_bot : x < 0, P x ) (bot_top : P ) (bot_pos : ∀ (x : ), 0 < xP x) (bot_zero : P 0) (bot_neg : x < 0, P x) (bot_bot : P ) (x : EReal) (y : EReal) :
            P x y

            Induct on two EReals by performing case splits on the sign of one whenever the other is infinite.

            theorem EReal.induction₂_symm {P : ERealERealProp} (symm : ∀ {x y : EReal}, P x yP y x) (top_top : P ) (top_pos : ∀ (x : ), 0 < xP x) (top_zero : P 0) (top_neg : x < 0, P x) (top_bot : P ) (pos_bot : ∀ (x : ), 0 < xP x ) (coe_coe : ∀ (x y : ), P x y) (zero_bot : P 0 ) (neg_bot : x < 0, P x ) (bot_bot : P ) (x : EReal) (y : EReal) :
            P x y

            Induct on two EReals by performing case splits on the sign of one whenever the other is infinite. This version eliminates some cases by assuming that the relation is symmetric.

            EReal with its multiplication is a CommMonoidWithZero. However, the proof of associativity by hand is extremely painful (with 125 cases...). Instead, we will deduce it later on from the facts that the absolute value and the sign are multiplicative functions taking value in associative objects, and that they characterize an extended real number. For now, we only record more basic properties of multiplication.

            theorem EReal.mul_comm (x : EReal) (y : EReal) :
            x * y = y * x
            theorem EReal.one_mul (x : EReal) :
            1 * x = x
            theorem EReal.zero_mul (x : EReal) :
            0 * x = 0

            Real coercion #

            The map from extended reals to reals sending infinities to zero.

            Equations
            Instances For
              @[simp]
              theorem EReal.toReal_coe (x : ) :
              @[simp]
              theorem EReal.bot_lt_coe (x : ) :
              < x
              @[simp]
              theorem EReal.coe_ne_bot (x : ) :
              x
              @[simp]
              theorem EReal.bot_ne_coe (x : ) :
              x
              @[simp]
              theorem EReal.coe_lt_top (x : ) :
              x <
              @[simp]
              theorem EReal.coe_ne_top (x : ) :
              x
              @[simp]
              theorem EReal.top_ne_coe (x : ) :
              x
              @[simp]
              @[simp]
              @[simp]
              @[simp]
              @[simp]
              @[simp]
              @[simp]
              theorem EReal.coe_add (x : ) (y : ) :
              (x + y) = x + y
              theorem EReal.coe_nsmul (n : ) (x : ) :
              (n x) = n x
              @[simp]
              theorem EReal.coe_eq_zero {x : } :
              x = 0 x = 0
              @[simp]
              theorem EReal.coe_eq_one {x : } :
              x = 1 x = 1
              theorem EReal.coe_ne_zero {x : } :
              x 0 x 0
              theorem EReal.coe_ne_one {x : } :
              x 1 x 1
              @[simp]
              theorem EReal.coe_nonneg {x : } :
              0 x 0 x
              @[simp]
              theorem EReal.coe_nonpos {x : } :
              x 0 x 0
              @[simp]
              theorem EReal.coe_pos {x : } :
              0 < x 0 < x
              @[simp]
              theorem EReal.coe_neg' {x : } :
              x < 0 x < 0
              theorem EReal.toReal_le_toReal {x : EReal} {y : EReal} (h : x y) (hx : x ) (hy : y ) :
              theorem EReal.coe_toReal {x : EReal} (hx : x ) (h'x : x ) :
              (EReal.toReal x) = x
              theorem EReal.le_coe_toReal {x : EReal} (h : x ) :
              x (EReal.toReal x)
              theorem EReal.coe_toReal_le {x : EReal} (h : x ) :
              (EReal.toReal x) x
              theorem EReal.eq_top_iff_forall_lt (x : EReal) :
              x = ∀ (y : ), y < x
              theorem EReal.eq_bot_iff_forall_lt (x : EReal) :
              x = ∀ (y : ), x < y

              Intervals and coercion from reals #

              theorem EReal.exists_between_coe_real {x : EReal} {z : EReal} (h : x < z) :
              ∃ (y : ), x < y y < z
              @[simp]
              theorem EReal.image_coe_Icc (x : ) (y : ) :
              @[simp]
              theorem EReal.image_coe_Ico (x : ) (y : ) :
              @[simp]
              theorem EReal.image_coe_Ioc (x : ) (y : ) :
              @[simp]
              theorem EReal.image_coe_Ioo (x : ) (y : ) :
              @[simp]
              theorem EReal.preimage_coe_Icc (x : ) (y : ) :
              @[simp]
              theorem EReal.preimage_coe_Ico (x : ) (y : ) :
              @[simp]
              theorem EReal.preimage_coe_Ioc (x : ) (y : ) :
              @[simp]
              theorem EReal.preimage_coe_Ioo (x : ) (y : ) :

              ennreal coercion #

              @[simp]
              theorem EReal.toReal_coe_ennreal {x : ENNReal} :
              EReal.toReal x = x.toReal
              @[simp]
              theorem EReal.coe_ennreal_ofReal {x : } :
              (ENNReal.ofReal x) = (max x 0)
              theorem EReal.coe_nnreal_eq_coe_real (x : NNReal) :
              x = x
              @[simp]
              theorem EReal.coe_ennreal_zero :
              0 = 0
              @[simp]
              theorem EReal.coe_ennreal_one :
              1 = 1
              @[simp]
              @[simp]
              @[simp]
              theorem EReal.coe_nnreal_lt_top (x : NNReal) :
              x <
              @[simp]
              theorem EReal.coe_ennreal_le_coe_ennreal_iff {x : ENNReal} {y : ENNReal} :
              x y x y
              @[simp]
              theorem EReal.coe_ennreal_lt_coe_ennreal_iff {x : ENNReal} {y : ENNReal} :
              x < y x < y
              @[simp]
              theorem EReal.coe_ennreal_eq_coe_ennreal_iff {x : ENNReal} {y : ENNReal} :
              x = y x = y
              @[simp]
              theorem EReal.coe_ennreal_eq_zero {x : ENNReal} :
              x = 0 x = 0
              @[simp]
              theorem EReal.coe_ennreal_eq_one {x : ENNReal} :
              x = 1 x = 1
              @[simp]
              theorem EReal.coe_ennreal_pos {x : ENNReal} :
              0 < x 0 < x
              @[simp]
              @[simp]
              @[simp]
              theorem EReal.coe_ennreal_add (x : ENNReal) (y : ENNReal) :
              (x + y) = x + y
              @[simp]
              theorem EReal.coe_ennreal_mul (x : ENNReal) (y : ENNReal) :
              (x * y) = x * y
              theorem EReal.coe_ennreal_nsmul (n : ) (x : ENNReal) :
              (n x) = n x

              Order #

              theorem EReal.exists_rat_btwn_of_lt {a : EReal} {b : EReal} :
              a < b∃ (x : ), a < x x < b
              theorem EReal.lt_iff_exists_rat_btwn {a : EReal} {b : EReal} :
              a < b ∃ (x : ), a < x x < b
              theorem EReal.lt_iff_exists_real_btwn {a : EReal} {b : EReal} :
              a < b ∃ (x : ), a < x x < b

              The set of numbers in EReal that are not equal to ±∞ is equivalent to .

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

                Addition #

                @[simp]
                theorem EReal.add_bot (x : EReal) :
                @[simp]
                theorem EReal.bot_add (x : EReal) :
                @[simp]
                theorem EReal.add_eq_bot_iff {x : EReal} {y : EReal} :
                x + y = x = y =
                @[simp]
                theorem EReal.bot_lt_add_iff {x : EReal} {y : EReal} :
                < x + y < x < y
                @[simp]
                theorem EReal.top_add_coe (x : ) :
                + x =
                @[simp]
                theorem EReal.coe_add_top (x : ) :
                x + =
                theorem EReal.toReal_add {x : EReal} {y : EReal} (hx : x ) (h'x : x ) (hy : y ) (h'y : y ) :
                theorem EReal.add_lt_add_right_coe {x : EReal} {y : EReal} (h : x < y) (z : ) :
                x + z < y + z
                theorem EReal.add_lt_add_left_coe {x : EReal} {y : EReal} (h : x < y) (z : ) :
                z + x < z + y
                theorem EReal.add_lt_add {x : EReal} {y : EReal} {z : EReal} {t : EReal} (h1 : x < y) (h2 : z < t) :
                x + z < y + t
                theorem EReal.add_lt_add_of_lt_of_le' {x : EReal} {y : EReal} {z : EReal} {t : EReal} (h : x < y) (h' : z t) (hbot : t ) (htop : t = z = x = ) :
                x + z < y + t
                theorem EReal.add_lt_add_of_lt_of_le {x : EReal} {y : EReal} {z : EReal} {t : EReal} (h : x < y) (h' : z t) (hz : z ) (ht : t ) :
                x + z < y + t

                See also EReal.add_lt_add_of_lt_of_le' for a version with weaker but less convenient assumptions.

                theorem EReal.add_lt_top {x : EReal} {y : EReal} (hx : x ) (hy : y ) :
                x + y <

                Negation #

                negation on EReal

                Equations
                Instances For
                  @[simp]
                  @[simp]
                  @[simp]
                  theorem EReal.coe_neg (x : ) :
                  (-x) = -x
                  @[simp]
                  theorem EReal.coe_sub (x : ) (y : ) :
                  (x - y) = x - y
                  theorem EReal.coe_zsmul (n : ) (x : ) :
                  (n x) = n x
                  @[simp]
                  theorem EReal.neg_eq_top_iff {x : EReal} :
                  -x = x =
                  @[simp]
                  theorem EReal.neg_eq_bot_iff {x : EReal} :
                  -x = x =
                  @[simp]
                  theorem EReal.neg_eq_zero_iff {x : EReal} :
                  -x = 0 x = 0
                  @[simp]
                  theorem EReal.neg_le_neg_iff {a : EReal} {b : EReal} :
                  -a -b b a
                  @[simp]
                  theorem EReal.neg_lt_neg_iff {a : EReal} {b : EReal} :
                  -a < -b b < a
                  theorem EReal.neg_le {a : EReal} {b : EReal} :
                  -a b -b a

                  -a ≤ b ↔ -b ≤ a on EReal.

                  theorem EReal.neg_le_of_neg_le {a : EReal} {b : EReal} (h : -a b) :
                  -b a

                  if -a ≤ b then -b ≤ a on EReal.

                  theorem EReal.le_neg_of_le_neg {a : EReal} {b : EReal} (h : a -b) :
                  b -a

                  a ≤ -b → b ≤ -a on ereal

                  Negation as an order reversing isomorphism on EReal.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    theorem EReal.neg_lt_iff_neg_lt {a : EReal} {b : EReal} :
                    -a < b -b < a
                    theorem EReal.neg_lt_of_neg_lt {a : EReal} {b : EReal} (h : -a < b) :
                    -b < a

                    Subtraction #

                    Subtraction on EReal is defined by x - y = x + (-y). Since addition is badly behaved at some points, so is subtraction. There is no standard algebraic typeclass involving subtraction that is registered on EReal, beyond SubNegZeroMonoid, because of this bad behavior.

                    @[simp]
                    theorem EReal.bot_sub (x : EReal) :
                    @[simp]
                    theorem EReal.sub_top (x : EReal) :
                    @[simp]
                    theorem EReal.top_sub_coe (x : ) :
                    - x =
                    @[simp]
                    theorem EReal.coe_sub_bot (x : ) :
                    x - =
                    theorem EReal.sub_le_sub {x : EReal} {y : EReal} {z : EReal} {t : EReal} (h : x y) (h' : t z) :
                    x - z y - t
                    theorem EReal.sub_lt_sub_of_lt_of_le {x : EReal} {y : EReal} {z : EReal} {t : EReal} (h : x < y) (h' : z t) (hz : z ) (ht : t ) :
                    x - t < y - z
                    theorem EReal.toReal_sub {x : EReal} {y : EReal} (hx : x ) (h'x : x ) (hy : y ) (h'y : y ) :

                    Multiplication #

                    theorem EReal.coe_mul_top_of_pos {x : } (h : 0 < x) :
                    x * =
                    theorem EReal.coe_mul_top_of_neg {x : } (h : x < 0) :
                    x * =
                    theorem EReal.top_mul_coe_of_pos {x : } (h : 0 < x) :
                    * x =
                    theorem EReal.top_mul_coe_of_neg {x : } (h : x < 0) :
                    * x =
                    theorem EReal.mul_top_of_pos {x : EReal} :
                    0 < xx * =
                    theorem EReal.mul_top_of_neg {x : EReal} :
                    x < 0x * =
                    theorem EReal.top_mul_of_pos {x : EReal} (h : 0 < x) :
                    theorem EReal.top_mul_of_neg {x : EReal} (h : x < 0) :
                    theorem EReal.coe_mul_bot_of_pos {x : } (h : 0 < x) :
                    x * =
                    theorem EReal.coe_mul_bot_of_neg {x : } (h : x < 0) :
                    x * =
                    theorem EReal.bot_mul_coe_of_pos {x : } (h : 0 < x) :
                    * x =
                    theorem EReal.bot_mul_coe_of_neg {x : } (h : x < 0) :
                    * x =
                    theorem EReal.mul_bot_of_pos {x : EReal} :
                    0 < xx * =
                    theorem EReal.mul_bot_of_neg {x : EReal} :
                    x < 0x * =
                    theorem EReal.bot_mul_of_pos {x : EReal} (h : 0 < x) :
                    theorem EReal.bot_mul_of_neg {x : EReal} (h : x < 0) :
                    theorem EReal.induction₂_neg_left {P : ERealERealProp} (neg_left : ∀ {x y : EReal}, P x yP (-x) y) (top_top : P ) (top_pos : ∀ (x : ), 0 < xP x) (top_zero : P 0) (top_neg : x < 0, P x) (top_bot : P ) (zero_top : P 0 ) (zero_bot : P 0 ) (pos_top : ∀ (x : ), 0 < xP x ) (pos_bot : ∀ (x : ), 0 < xP x ) (coe_coe : ∀ (x y : ), P x y) (x : EReal) (y : EReal) :
                    P x y

                    Induct on two ereals by performing case splits on the sign of one whenever the other is infinite. This version eliminates some cases by assuming that P x y implies P (-x) y for all x, y.

                    theorem EReal.induction₂_symm_neg {P : ERealERealProp} (symm : ∀ {x y : EReal}, P x yP y x) (neg_left : ∀ {x y : EReal}, P x yP (-x) y) (top_top : P ) (top_pos : ∀ (x : ), 0 < xP x) (top_zero : P 0) (coe_coe : ∀ (x y : ), P x y) (x : EReal) (y : EReal) :
                    P x y

                    Induct on two ereals by performing case splits on the sign of one whenever the other is infinite. This version eliminates some cases by assuming that P is symmetric and P x y implies P (-x) y for all x, y.

                    theorem EReal.neg_mul (x : EReal) (y : EReal) :
                    -x * y = -(x * y)

                    Absolute value #

                    The absolute value from EReal to ℝ≥0∞, mapping and to and a real x to |x|.

                    Equations
                    Instances For
                      @[simp]
                      theorem EReal.abs_eq_zero_iff {x : EReal} :
                      EReal.abs x = 0 x = 0
                      @[simp]
                      @[simp]
                      theorem EReal.coe_abs (x : ) :
                      (EReal.abs x) = |x|
                      @[simp]
                      @[simp]
                      theorem EReal.abs_mul (x : EReal) (y : EReal) :

                      Sign #

                      theorem EReal.sign_top :
                      SignType.sign = 1
                      theorem EReal.sign_bot :
                      SignType.sign = -1
                      @[simp]
                      theorem EReal.sign_coe (x : ) :
                      SignType.sign x = SignType.sign x
                      @[simp]
                      theorem EReal.coe_coe_sign (x : SignType) :
                      x = x
                      @[simp]
                      theorem EReal.sign_neg (x : EReal) :
                      SignType.sign (-x) = -SignType.sign x
                      @[simp]
                      theorem EReal.sign_mul (x : EReal) (y : EReal) :
                      SignType.sign (x * y) = SignType.sign x * SignType.sign y
                      @[simp]
                      theorem EReal.sign_mul_abs (x : EReal) :
                      (SignType.sign x) * (EReal.abs x) = x
                      @[simp]
                      theorem EReal.abs_mul_sign (x : EReal) :
                      (EReal.abs x) * (SignType.sign x) = x
                      theorem EReal.sign_eq_and_abs_eq_iff_eq {x : EReal} {y : EReal} :
                      EReal.abs x = EReal.abs y SignType.sign x = SignType.sign y x = y
                      theorem EReal.le_iff_sign {x : EReal} {y : EReal} :
                      x y SignType.sign x < SignType.sign y SignType.sign x = SignType.neg SignType.sign y = SignType.neg EReal.abs y EReal.abs x SignType.sign x = SignType.zero SignType.sign y = SignType.zero SignType.sign x = SignType.pos SignType.sign y = SignType.pos EReal.abs x EReal.abs y
                      @[simp]
                      theorem EReal.coe_pow (x : ) (n : ) :
                      (x ^ n) = x ^ n
                      @[simp]
                      theorem EReal.coe_ennreal_pow (x : ENNReal) (n : ) :
                      (x ^ n) = x ^ n