ENNReal.toNNReal_le_toNNReal
theorem ENNReal.toNNReal_le_toNNReal : ∀ {a b : ENNReal}, a ≠ ⊤ → b ≠ ⊤ → (a.toNNReal ≤ b.toNNReal ↔ a ≤ b)
This theorem states that for any two extended nonnegative real numbers 'a' and 'b' that are not equal to positive infinity (notated as '⊤'), the nonnegative real number representation of 'a' is less than or equal to the nonnegative real number representation of 'b' if and only if 'a' is less than or equal to 'b'. Essentially, converting between the extended nonnegative real numbers and the nonnegative real numbers preserves the order of the numbers, as long as neither of them is positive infinity.
More concisely: For any extended nonnegative real numbers 'a' and 'b' not equal to positive infinity, a ≤ b if and only if ℛ(a) ≤ ℛ(b), where ℛ(x) denotes the nonnegative real number representation of x.
|
ENNReal.toReal_prod
theorem ENNReal.toReal_prod :
∀ {ι : Type u_1} {s : Finset ι} {f : ι → ENNReal}, (s.prod fun i => f i).toReal = s.prod fun i => (f i).toReal := by
sorry
The theorem `ENNReal.toReal_prod` states that for any finite set `s` of an arbitrary type `ι` and any function `f` that maps elements of type `ι` to extended nonnegative real numbers (ENNReal), the real part of the product of the `f` values for all elements in `s` is equal to the product of the real parts of the `f` values for all elements in `s`. This essentially indicates that taking the product of the `f` values and then the real part is the same as taking the real part of each `f` value and then their product. In mathematical terms, for any set $s$ and function $f : \iota \rightarrow [0, \infty]$ we have $\text{toReal}(\prod_{i \in s} f(i)) = \prod_{i \in s} \text{toReal}(f(i))$.
More concisely: For any set $s$ and function $f : \iota \rightarrow [0, \infty]$, we have $\text{toReal}(\prod\_{i \in s} f(i)) = \prod\_{i \in s} \text{toReal}(f(i))$.
|
ENNReal.toReal_le_toReal
theorem ENNReal.toReal_le_toReal : ∀ {a b : ENNReal}, a ≠ ⊤ → b ≠ ⊤ → (a.toReal ≤ b.toReal ↔ a ≤ b)
This theorem states that for any two extended nonnegative real numbers `a` and `b` that are not infinity (`⊤`), the inequality `a.toReal ≤ b.toReal` holds if and only if `a ≤ b`. In other words, when `a` and `b` are finite, comparing them as extended nonnegative real numbers or as standard real numbers gives the same result. This is a property that connects the orderings of the extended nonnegative reals and the standard reals.
More concisely: For any finite extended nonnegative real numbers `a` and `b`, the equality `a.toReal = b.toReal` if and only if `a = b`. (The implication also holds with `≤` instead of `=` for the order relation.)
|
ENNReal.toReal_le_of_le_ofReal
theorem ENNReal.toReal_le_of_le_ofReal : ∀ {a : ENNReal} {b : ℝ}, 0 ≤ b → a ≤ ENNReal.ofReal b → a.toReal ≤ b := by
sorry
This theorem asserts that for any extended nonnegative real number 'a' and any real number 'b', if 'b' is nonnegative and 'a' is less than or equal to the extended nonnegative real number that represents 'b' (as produced by the 'ENNReal.ofReal' function), then the real number representation of 'a' (which we get by using the 'toReal' function) is less than or equal to 'b'. In other words, if 'b' is nonnegative and 'a' is not bigger than the nonnegative real version of 'b', then 'a' interpreted as a real number is not bigger than 'b'.
More concisely: For all extended non-negative real numbers 'a' and real numbers 'b' with 'b' non-negative, if 'a' ≤ ENNReal.ofReal 'b' then a.toReal ≤ b.
|
ENNReal.iSup_zero_eq_zero
theorem ENNReal.iSup_zero_eq_zero : ∀ {ι : Sort u_1}, ⨆ x, 0 = 0
This theorem states that for all types `ι`, the supremum (least upper bound) of the set where each element is `0` is `0`. In other words, when you have a set where all elements are `0`, the least upper bound of this set is also `0`.
More concisely: For any type `ι`, the supremum of the set of all `ι`-valued elements equal to 0 is 0.
|
ENNReal.ofReal_eq_ofReal_iff
theorem ENNReal.ofReal_eq_ofReal_iff : ∀ {p q : ℝ}, 0 ≤ p → 0 ≤ q → (ENNReal.ofReal p = ENNReal.ofReal q ↔ p = q) := by
sorry
The theorem `ENNReal.ofReal_eq_ofReal_iff` states that for any two real numbers `p` and `q` that are both nonnegative (i.e., `0 ≤ p` and `0 ≤ q`), the function `ENNReal.ofReal` applied to `p` equals the same function applied to `q` if and only if `p` equals `q`. In other words, `ENNReal.ofReal` is injective for nonnegative real numbers.
More concisely: For non-negative real numbers `p` and `q`, `ENNReal.ofReal p = ENNReal.ofReal q` if and only if `p = q`.
|
ENNReal.toReal_smul
theorem ENNReal.toReal_smul : ∀ (r : NNReal) (s : ENNReal), (r • s).toReal = r • s.toReal
The theorem `ENNReal.toReal_smul` states that for any nonnegative real number `r` and any extended nonnegative real number `s`, multiplying `r` and `s` in the extended nonnegative reals and then converting to a real number is the same as first converting `s` to a real number and then multiplying by `r`. In mathematical terms, this theorem states that for all `r` in the set of nonnegative real numbers and for all `s` in the extended set of nonnegative real numbers (which includes positive infinity), the real part of the product `r * s` is equal to `r` times the real part of `s`.
More concisely: For all non-negative real numbers `r` and extended non-negative real numbers `s`, the real part of `r * s` equals `r` times the real part of `s`.
|
ENNReal.toReal_pos
theorem ENNReal.toReal_pos : ∀ {a : ENNReal}, a ≠ 0 → a ≠ ⊤ → 0 < a.toReal
The theorem `ENNReal.toReal_pos` asserts that for any extended nonnegative real number `a`, if `a` is not equal to zero and `a` is not equal to positive infinity, then the real representation of `a` (denoted as `a.toReal`) is strictly greater than zero. In other words, any non-zero, finite extended nonnegative real number, when converted to a real number, is positive.
More concisely: For any non-zero, finite extended nonnegative real number `a`, its real representation `a.toReal` is strictly positive.
|
ENNReal.ofReal_mul
theorem ENNReal.ofReal_mul : ∀ {p q : ℝ}, 0 ≤ p → ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q := by
sorry
The theorem `ENNReal.ofReal_mul` states that for all real numbers `p` and `q`, if `p` is nonnegative then the function `ENNReal.ofReal` applied to the product `p * q` is equal to the product of `ENNReal.ofReal p` and `ENNReal.ofReal q`. In other words, this theorem is asserting that the function `ENNReal.ofReal` preserves multiplication for nonnegative real numbers.
More concisely: For all non-negative real numbers p and q, `ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q`.
|
ENNReal.toReal_add
theorem ENNReal.toReal_add : ∀ {a b : ENNReal}, a ≠ ⊤ → b ≠ ⊤ → (a + b).toReal = a.toReal + b.toReal
The theorem `ENNReal.toReal_add` states that for any two elements `a` and `b` of the extended nonnegative real numbers (which are typically denoted as [0, ∞] and are relevant as the codomain of a measure), given that neither of them is the top element, the real part of their sum equals the sum of their real parts. This is a property ensuring the consistency of the 'toReal' operation with addition in the extended nonnegative real numbers.
More concisely: For any `a, b` in the extended nonnegative real numbers with `a, b` not top element, `(toReal a + toReal b) = toReal (a + b)`.
|
ENNReal.trichotomy
theorem ENNReal.trichotomy : ∀ (p : ENNReal), p = 0 ∨ p = ⊤ ∨ 0 < p.toReal
The theorem `ENNReal.trichotomy` states that for every extended nonnegative real number `p`, one and only one of the following three conditions holds: `p` is equal to zero, `p` is equal to positive infinity (denoted by '⊤'), or the real number representation of `p` is strictly greater than zero.
More concisely: Every extended nonnegative real number `p` is equal to zero, positive infinity, or lies strictly between them.
|
ENNReal.toReal_mul
theorem ENNReal.toReal_mul : ∀ {a b : ENNReal}, (a * b).toReal = a.toReal * b.toReal
This theorem states that for all extended nonnegative real numbers `a` and `b`, the real part of the product of `a` and `b` is equal to the product of the real parts of `a` and `b`. In other words, when we multiply two extended nonnegative real numbers (which could possibly be infinite) and then take the real part, it's the same as if we had first taken the real part of each number and then multiplied them. This theorem is crucial when working with measures, as it ensures that the multiplication operation is compatible with real numbers and extended nonnegative real numbers.
More concisely: For all extended nonnegative real numbers `a` and `b`, the real part of their product equals the product of their real parts.
|
ENNReal.iInf_mul
theorem ENNReal.iInf_mul :
∀ {ι : Sort u_2} [inst : Nonempty ι] {f : ι → ENNReal} {x : ENNReal}, x ≠ ⊤ → iInf f * x = ⨅ i, f i * x
This theorem states that for any nonempty type `ι`, any function from `ι` to the extended nonnegative real numbers `ENNReal` (denoted as `f`), and any `x` in `ENNReal` that is not infinity (`∞`), the infimum (`iInf`) of the function `f` multiplied by `x` is equal to the infimum over all `i` of the product of `f(i)` and `x`. In other words, if `x` is not infinity, then right multiplication by `x` preserves the infimum operation over the range of a function mapping from a nonempty type to the extended nonnegative real numbers.
More concisely: For any nonempty type `ι`, any function `f` from `ι` to the extended nonnegative real numbers `ENNReal`, and any `x ∈ ENNReal\setminus\{∞\}`: `iInf(xi : ENNReal | i ∈ ι) * x = iInf(f i) * x`, where `iInf` represents the infimum operation.
|
ENNReal.ofReal_pos
theorem ENNReal.ofReal_pos : ∀ {p : ℝ}, 0 < ENNReal.ofReal p ↔ 0 < p
The theorem `ENNReal.ofReal_pos` states that for any real number `p`, the statement that the extended nonnegative real representation of `p` (which maps `p` to itself if it's nonnegative, and to `0` otherwise) is greater than `0` is equivalent to the statement that `p` is greater than `0`. In other words, a real number `p` is positive if and only if its extended nonnegative real representation is also positive.
More concisely: The theorem `ENNReal.ofReal_pos` asserts that for every real number `p`, `ENNReal p > 0` if and only if `p > 0`.
|
ENNReal.ofReal_eq_zero
theorem ENNReal.ofReal_eq_zero : ∀ {p : ℝ}, ENNReal.ofReal p = 0 ↔ p ≤ 0
The theorem `ENNReal.ofReal_eq_zero` states that for any real number `p`, the function `ENNReal.ofReal` applied to `p` equals zero if and only if `p` is less than or equal to zero. In other words, in the extended nonnegative real number system, a real number converts to zero when it is nonpositive.
More concisely: For any real number `p` in the extended nonnegative real numbers system, `ENNReal.ofReal p = 0` if and only if `p` is less than or equal to zero.
|
ENNReal.ofReal_le_ofReal
theorem ENNReal.ofReal_le_ofReal : ∀ {p q : ℝ}, p ≤ q → ENNReal.ofReal p ≤ ENNReal.ofReal q
The theorem `ENNReal.ofReal_le_ofReal` states that for any two real numbers `p` and `q`, if `p` is less than or equal to `q`, then the nonnegative real number corresponding to `p` (obtained using the `ENNReal.ofReal` function) is also less than or equal to the nonnegative real number corresponding to `q`. In other words, the function `ENNReal.ofReal` preserves the order of real numbers when they are mapped to their nonnegative counterparts.
More concisely: For all real numbers `p` and `q`, if `p ≤ q`, then `ENNReal.ofReal p ≤ ENNReal.ofReal q`.
|
ENNReal.mul_iInf_of_ne
theorem ENNReal.mul_iInf_of_ne :
∀ {ι : Sort u_2} {f : ι → ENNReal} {x : ENNReal}, x ≠ 0 → x ≠ ⊤ → x * iInf f = ⨅ i, x * f i
This theorem states that for any given indexed set `f` of extended nonnegative real numbers (represented as `ENNReal`), and any `x` from extended nonnegative real numbers such that `x` is not equal to zero and `x` is not infinity, the multiplication of `x` with the infimum of the set `f` (denoted as `iInf f`) is equal to the infimum over all elements `i` of the set obtained by multiplying `x` with each element of the set `f`. This theorem basically shows how left-multiplication interacts with the operation of taking infimum in the context of extended nonnegative real numbers. Note that there's a related theorem `ENNReal.mul_iInf` which does not require `x` to be nonzero but instead assumes the indexing set `ι` is nonempty.
More concisely: For any indexed set `f` of extended nonnegative real numbers and any `x` in the extended nonnegative real numbers not equal to zero or infinity, `x * iInf (f) = iInf (map x f)`.
|
ENNReal.ofReal_le_ofReal_iff
theorem ENNReal.ofReal_le_ofReal_iff : ∀ {p q : ℝ}, 0 ≤ q → (ENNReal.ofReal p ≤ ENNReal.ofReal q ↔ p ≤ q)
The theorem `ENNReal.ofReal_le_ofReal_iff` states that for every two real numbers `p` and `q`, if `q` is nonnegative, then the nonnegative extended real number representation of `p` is less than or equal to the nonnegative extended real number representation of `q` if and only if `p` is less than or equal to `q`. In other words, the function `ENNReal.ofReal`, which maps real numbers to nonnegative extended real numbers, preserves the order of nonnegative real numbers.
More concisely: For every real numbers `p` and `q` with `q` nonnegative, `ENNReal.ofReal p <= ENNReal.ofReal q` if and only if `p <= q`.
|
ENNReal.toReal_pos_iff
theorem ENNReal.toReal_pos_iff : ∀ {a : ENNReal}, 0 < a.toReal ↔ 0 < a ∧ a < ⊤
This theorem states that for any extended nonnegative real number `a`, `a`'s real number value is greater than zero if and only if `a` is greater than zero and `a` is less than positive infinity. In other words, an extended nonnegative real number `a` has a positive real counterpart if and only if it itself is positive and finite. This theorem bridges the relationship between the positivity in the space of extended nonnegative real numbers and the space of real numbers.
More concisely: An extended nonnegative real number `a` has a positive real value if and only if `a` is positive and finite.
|
ENNReal.toNNReal_inv
theorem ENNReal.toNNReal_inv : ∀ (a : ENNReal), a⁻¹.toNNReal = a.toNNReal⁻¹
This theorem states that for every element `a` of the extended nonnegative real numbers (which is typically denoted as [0, ∞]), the operation of taking the inverse in the extended nonnegative reals followed by the operation of converting to the nonnegative reals is the same as first converting to the nonnegative reals and then taking the inverse. Therefore, the inverse operation in the extended nonnegative real numbers preserves the structure of the nonnegative real numbers when it comes to inversion.
More concisely: For every extended nonnegative real number `a`, the operations of taking the inverse in the extended nonnegative reals and then converting to the nonnegative reals, and converting to the nonnegative reals and then taking the inverse, are equal. In Lean notation: `(0 ≤ a ∧ a ≤ ∞) → (∥−1∥ a = ∥−1∥ (convert a to ℝ0+))`.
|
ENNReal.toReal_inv
theorem ENNReal.toReal_inv : ∀ (a : ENNReal), a⁻¹.toReal = a.toReal⁻¹
This theorem states that for every extended nonnegative real number `a`, the real number obtained by taking the reciprocal of `a` and then converting to a real number (using the `toReal` function) is the same as first converting `a` to a real number and then taking its reciprocal. In mathematical terms, for all `a` in the extended nonnegative real numbers (usually denoted as [0, ∞]), the operation of taking the reciprocal commutes with the operation of converting to a real number.
More concisely: For all extended nonnegative real numbers `a`, the conversion of `a` to a real number and taking its reciprocal is equal to taking the reciprocal of `a` and then converting it to a real number.
|
ENNReal.mul_iInf
theorem ENNReal.mul_iInf :
∀ {ι : Sort u_2} [inst : Nonempty ι] {f : ι → ENNReal} {x : ENNReal}, x ≠ ⊤ → x * iInf f = ⨅ i, x * f i
This theorem states that if `x` is a real number that is not infinity (usually denoted as `∞`) in extended nonnegative real numbers (`ENNReal`), then for any nonempty type `ι` and function `f` mapping `ι` to `ENNReal`, multiplying `x` with the infimum (greatest lower bound) of the `f`'s values (denoted as `iInf f`) is equal to the infimum of the product of `x` and each `f(i)`. Essentially, it says that left multiplication by `x` maps the infimum over a nonempty type to the infimum. There is a similar theorem `ENNReal.mul_iInf_of_ne` that assumes `x` is not zero but does not require `ι` to be nonempty.
More concisely: For any non-zero real number `x` and nonempty type `ι`, the product of `x` and the infimum of a function `f` mapping `ι` to extended nonnegative real numbers is equal to the infimum of the products `x * f(i)` over all `i` in `ι`.
|
ENNReal.ofReal_of_nonpos
theorem ENNReal.ofReal_of_nonpos : ∀ {p : ℝ}, p ≤ 0 → ENNReal.ofReal p = 0
This theorem, named `ENNReal.ofReal_of_nonpos`, states that for any real number `p`, if `p` is less than or equal to zero, then the function `ENNReal.ofReal` applied to `p` will return zero. In mathematical terms, for all real numbers `p`, if `p ≤ 0` then `ENNReal.ofReal(p) = 0`. This theorem is the reverse direction of the theorem `ENNReal.ofReal_eq_zero`.
More concisely: For all real numbers `p`, if `p <= 0`, then `ENNReal.ofReal(p) = 0`.
|
ENNReal.ofReal_add
theorem ENNReal.ofReal_add :
∀ {p q : ℝ}, 0 ≤ p → 0 ≤ q → ENNReal.ofReal (p + q) = ENNReal.ofReal p + ENNReal.ofReal q
This theorem states that for any two real numbers `p` and `q` that are nonnegative (i.e., greater than or equal to 0), the function `ENNReal.ofReal` applied to the sum of `p` and `q` is equal to the sum of the function `ENNReal.ofReal` applied to `p` and `q` separately. In other words, for nonnegative real numbers, the `ENNReal.ofReal` function distributes over addition.
More concisely: For all non-negative real numbers `p` and `q`, `ENNReal.ofReal (p + q) = ENNReal.ofReal p + ENNReal.ofReal q`.
|
ENNReal.lt_ofReal_iff_toReal_lt
theorem ENNReal.lt_ofReal_iff_toReal_lt : ∀ {a : ENNReal} {b : ℝ}, a ≠ ⊤ → (a < ENNReal.ofReal b ↔ a.toReal < b) := by
sorry
This theorem states that for any extended nonnegative real number `a` and any real number `b`, provided that `a` is not infinity, `a` is less than the extended nonnegative real equivalent of `b` if and only if the real equivalent of `a` is less than `b`. In other words, the ordering of these numbers is preserved when transitioning between the domains of real numbers and extended nonnegative real numbers (excluding infinity).
More concisely: For any real numbers `a` and `b`, and extended non-negative real number `a'`, if `a < b` holds in the real numbers and `a != \infty`, then `a' < b` holds in the extended non-negative real numbers.
|
ENNReal.iInf_mul_of_ne
theorem ENNReal.iInf_mul_of_ne :
∀ {ι : Sort u_2} {f : ι → ENNReal} {x : ENNReal}, x ≠ 0 → x ≠ ⊤ → iInf f * x = ⨅ i, f i * x
The theorem `ENNReal.iInf_mul_of_ne` states that for an index set `ι` and a function `f` mapping from this index set to the extended nonnegative real numbers (which includes positive real numbers and infinity), and a given extended nonnegative real number `x` that is neither zero nor infinity, the operation of right multiplication by `x` preserves the infimum operation. In other words, multiplying the infimum (lowest value) of the set of all function values by `x` is the same as taking the infimum of the set of all function values each individually multiplied by `x`. This theorem does not require the index set to be nonempty but does require `x` to be non-zero and non-infinite.
More concisely: For a function `f` from a nonempty index set `ι` to the extended nonnegative real numbers, and an extended nonzero and non-infinite real number `x`, the infimum of `{xf(i) | i ∈ ι}` equals `x * inf {f(i) | i ∈ ι}`.
|
ENNReal.toReal_mono
theorem ENNReal.toReal_mono : ∀ {a b : ENNReal}, b ≠ ⊤ → a ≤ b → a.toReal ≤ b.toReal
This theorem states that for any two extended nonnegative real numbers `a` and `b`, if `b` is not infinity (`⊤`), then if `a` is less than or equal to `b` (`a ≤ b`), it implies that the conversion of `a` and `b` to real numbers retains this ordering (`a.toReal ≤ b.toReal`). In other words, the `toReal` function is monotonic: preserving the order of `a` and `b` in the ENNReal numbers when they are converted to real numbers, as long as `b` is not infinity.
More concisely: For any extended nonnegative real numbers `a` and `b` with `b` finite, if `a ≤ b`, then `a.toReal ≤ b.toReal`.
|
ENNReal.toReal_le_add'
theorem ENNReal.toReal_le_add' :
∀ {a b c : ENNReal}, a ≤ b + c → (b = ⊤ → a = ⊤) → (c = ⊤ → a = ⊤) → a.toReal ≤ b.toReal + c.toReal
This theorem states that for any three extended nonnegative real numbers `a`, `b`, and `c`, if `a` is less than or equal to the sum of `b` and `c`, and if `a` equals infinity whenever `b` or `c` equals infinity, then the real value of `a` is less than or equal to the sum of the real values of `b` and `c`. This is useful for transferring inequalities that resemble the triangle inequality from extended nonnegative real numbers to real numbers.
More concisely: If $a$ is an extended non-negative real number less than or equal to the sum of extended non-negative real numbers $b$ and $c$, and $a = \infty$ if and only if $b$ or $c$ is $\infty$, then $a \leqslant \mathrm{Re}(b) + \mathrm{Re}(c)$, where $\mathrm{Re}(x)$ denotes the real part of a complex number $x$.
|
ENNReal.toReal_div
theorem ENNReal.toReal_div : ∀ (a b : ENNReal), (a / b).toReal = a.toReal / b.toReal
This theorem states that for all elements 'a' and 'b' of the extended nonnegative real numbers (denoted as [0, ∞]), the real number equivalent of the quotient of 'a' and 'b' (a divided by b) is equal to the quotient of the real number equivalents of 'a' and 'b'. In other words, converting the quotient of 'a' and 'b' to a real number yields the same result as first converting 'a' and 'b' to real numbers and then taking their quotient.
More concisely: For all 'a' and 'b' in the extended nonnegative real numbers, [a/b] = (mêmea : ℝ) / (mêmeb : ℝ), where [a] and [b] denote the real number equivalents of 'a' and 'b' respectively.
|
ENNReal.toNNReal_mul
theorem ENNReal.toNNReal_mul : ∀ {a b : ENNReal}, (a * b).toNNReal = a.toNNReal * b.toNNReal
This theorem states that for every two elements `a` and `b` from the extended nonnegative real numbers `ENNReal`, the operation of converting the product of `a` and `b` to the nonnegative real numbers `toNNReal` is the same as first converting `a` and `b` separately to nonnegative real numbers and then multiplying them. In other words, the multiplication operation is compatible with the `toNNReal` function.
More concisely: For all `a` and `b` in the extended nonnegative real numbers `ENNReal`, `toNNReal (a * b) = toNNReal a * toNNReal b`.
|
ENNReal.dichotomy
theorem ENNReal.dichotomy : ∀ (p : ENNReal) [inst : Fact (1 ≤ p)], p = ⊤ ∨ 1 ≤ p.toReal
The theorem `ENNReal.dichotomy` states that for any extended nonnegative real number `p`, given that `p` is greater than or equal to 1 (`1 ≤ p`), there are only two possibilities: `p` is either equal to the infinity symbol `⊤`, which represents an infinite quantity in extended nonnegative real numbers, or `p` is greater than or equal to 1 when converted to a real number (`1 ≤ p.toReal`).
More concisely: For every extended nonnegative real number `p` greater than or equal to 1, either `p = ⊤` or `1 ≤ p.toReal`.
|
Mathlib.Data.ENNReal.Real._auxLemma.14
theorem Mathlib.Data.ENNReal.Real._auxLemma.14 : ∀ {p : ℝ}, (ENNReal.ofReal p = 0) = (p ≤ 0)
The theorem `Mathlib.Data.ENNReal.Real._auxLemma.14` states that for any real number `p`, the function `ENNReal.ofReal p` returns `0` if and only if `p` is less than or equal to `0`. In other words, this function effectively discards the negative part of the real number, setting it to zero.
More concisely: For any real number `p`, `ENNReal.ofReal p = 0` if and only if `p <= 0`.
|
ENNReal.iInf_add
theorem ENNReal.iInf_add : ∀ {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal}, iInf f + a = ⨅ i, f i + a
The theorem `ENNReal.iInf_add` states that for any index type `ι`, any function `f` from `ι` to the extended nonnegative real numbers (`ENNReal`), and any extended nonnegative real number `a`, the indexed infimum of `f` plus `a` is equal to the infimum over all `i` of `f i` plus `a`. This essentially says that adding a constant `a` to the indexed infimum of a function is the same as finding the infimum of the function values plus `a`.
More concisely: For any index type `ι`, function `f` from `ι` to `ENNReal`, and extended nonnegative real number `a`, the indexed infimum of `f` equals the infimum of `(fi + a)` for all `i` in `ι`.
|
ENNReal.toReal_le_add
theorem ENNReal.toReal_le_add : ∀ {a b c : ENNReal}, a ≤ b + c → b ≠ ⊤ → c ≠ ⊤ → a.toReal ≤ b.toReal + c.toReal := by
sorry
This theorem states that, for any three extended nonnegative real numbers 'a', 'b', and 'c', if 'a' is less than or equal to the sum of 'b' and 'c', and neither 'b' nor 'c' is infinity, then the real number representation of 'a' is less than or equal to the sum of the real number representations of 'b' and 'c'. This theorem is helpful to apply inequalities that resemble the triangle inequality from the extended nonnegative real numbers to the real numbers.
More concisely: For any extended nonnegative real numbers a, b, and c, if a <= b + c and neither b nor c is infinity, then a <= real.mkTop (real.mkTop +^ real.mkTop real.mkTop) (some b) (some c), where real.mkTop denotes the top element of the real numbers and some represents the existence quantifier in Lean.
|
ENNReal.toReal_lt_toReal
theorem ENNReal.toReal_lt_toReal : ∀ {a b : ENNReal}, a ≠ ⊤ → b ≠ ⊤ → (a.toReal < b.toReal ↔ a < b)
This theorem states that for any two extended nonnegative real numbers `a` and `b`, provided that neither `a` nor `b` are equal to positive infinity, the real number equivalent of `a` is less than the real number equivalent of `b` if and only if `a` is less than `b`. In other words, the comparison of `a` and `b` remains consistent whether we consider them as extended nonnegative real numbers or as their real number equivalents.
More concisely: For any extended nonnegative real numbers `a` and `b` not equal to positive infinity, `a < b` if and only if their real number equivalents have the same comparison relation.
|
ENNReal.toReal_pos_iff_ne_top
theorem ENNReal.toReal_pos_iff_ne_top : ∀ (p : ENNReal) [inst : Fact (1 ≤ p)], 0 < p.toReal ↔ p ≠ ⊤
This theorem states that for any extended nonnegative real number `p` such that `p` is greater than or equal to 1, `p` is greater than 0 when converted to a standard real number if and only if `p` is not equal to positive infinity. This essentially relates the positivity of the real number representation of `p` to the condition that `p` is not the "top" element (which represents positive infinity) in the set of extended nonnegative real numbers.
More concisely: For an extended nonnegative real number `p` greater than or equal to 1, `p` represents a positive real number if and only if `p` is finite.
|
ENNReal.toReal_eq_toReal
theorem ENNReal.toReal_eq_toReal : ∀ {a b : ENNReal}, a ≠ ⊤ → b ≠ ⊤ → (a.toReal = b.toReal ↔ a = b)
This theorem states that for any two extended nonnegative real numbers `a` and `b` that are not equal to positive infinity (`⊤`), `a` is equal to `b` if and only if the real number representations of `a` and `b` are equal. In other words, excluding the positive infinity case, the process of converting extended nonnegative real numbers to real numbers preserves equality.
More concisely: For extended nonnegative real numbers `a` and `b` not equal to positive infinity, `a = b` if and only if their real number representations are equal.
|
ENNReal.ofReal_lt_ofReal_iff
theorem ENNReal.ofReal_lt_ofReal_iff : ∀ {p q : ℝ}, 0 < q → (ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q)
This theorem states that for any two real numbers `p` and `q`, given that `q` is greater than zero, the function `ENNReal.ofReal` applied to `p` is less than the function applied to `q` if and only if `p` is less than `q`. In other words, the comparison of the two real numbers remains the same after going through the `ENNReal.ofReal` operation as long as `q` is positive.
More concisely: For all real numbers `p` and `q` with `q > 0`, `ENNReal.ofReal p < ENNReal.ofReal q` if and only if `p < q`.
|
ENNReal.ofReal_le_of_le_toReal
theorem ENNReal.ofReal_le_of_le_toReal : ∀ {a : ℝ} {b : ENNReal}, a ≤ b.toReal → ENNReal.ofReal a ≤ b
The theorem `ENNReal.ofReal_le_of_le_toReal` states that for any real number `a` and any extended nonnegative real number `b`, if `a` is less than or equal to the real number representation of `b` (indicated by `b.toReal`), then the extended nonnegative real number representation of `a` (given by `ENNReal.ofReal a`) is less than or equal to `b`. In other words, this theorem preserves the order relation "less than or equal to" under the map from real numbers to extended nonnegative real numbers.
More concisely: For all real numbers `a` and extended nonnegative real numbers `b`, `a ≤ b.toReal` implies `ENNReal.ofReal a ≤ b`.
|