NNReal.coe_zero
theorem NNReal.coe_zero : ↑0 = 0
This theorem states that the non-negative real number representation of zero (`↑0`) is equal to zero (`0`). In simpler words, when zero is cast as a non-negative real number, it remains zero. The proof for this theorem is not provided here (represented by `sorry`).
More concisely: The theorem asserts that `↑0 = 0` in Lean 4's non-negative real numbers.
|
Real.toNNReal_coe
theorem Real.toNNReal_coe : ∀ {r : NNReal}, (↑r).toNNReal = r
This theorem states that for every non-negative real number `r`, when we apply the function `Real.toNNReal` to `r` (after it has been coerced to a real number), we get back `r` itself. This essentially means that converting a non-negative real number to a real and then reinterpreting it back to a non-negative real number does not change the initial number.
More concisely: For every non-negative real number `r`, `Real.toNNReal (real.coerce r) = r`.
|
NNReal.coe_eq_zero
theorem NNReal.coe_eq_zero : ∀ {r : NNReal}, ↑r = 0 ↔ r = 0
This theorem states that for any nonnegative real number `r` (denoted by `NNReal`), the condition that its coercion (or embedding) into the real numbers equals zero is equivalent to the condition that `r` itself equals zero. In more mathematical terms, it asserts that a nonnegative real number `r` is zero if and only if its image under the natural embedding of nonnegative real numbers into the real numbers is zero.
More concisely: For any nonnegative real number `r`, `r = 0` if and only if the real number representation of `r` is 0.
|
Real.toNNReal_inv
theorem Real.toNNReal_inv : ∀ {x : ℝ}, x⁻¹.toNNReal = x.toNNReal⁻¹
This theorem states that for any real number 'x', the function 'Real.toNNReal' applied to the inverse of 'x' is equal to the inverse of 'Real.toNNReal x'. In other words, the process of converting a real number to a non-negative real number commutes with taking the reciprocal. This means that whether you first take a reciprocal and then convert to a non-negative real, or first convert to a non-negative real and then take a reciprocal, you get the same result.
More concisely: For any real number x, Real.toNNReal (1 / x) = 1 / Real.toNNReal x.
|
Real.toNNReal_of_nonpos
theorem Real.toNNReal_of_nonpos : ∀ {r : ℝ}, r ≤ 0 → r.toNNReal = 0
The theorem `Real.toNNReal_of_nonpos` states that for any real number `r`, if `r` is less than or equal to zero, then the result of applying the function `Real.toNNReal` to `r` will be zero. This is in line with the definition of the function `Real.toNNReal`, which reinterprets a real number as a non-negative real number, returning `0` for all inputs less than `0`.
More concisely: For any real number `r`, if `r ≤ 0`, then `Real.toNNReal r = 0`.
|
NNReal.coe_mono
theorem NNReal.coe_mono : Monotone NNReal.toReal
The theorem `NNReal.coe_mono` states that the function `NNReal.toReal`, which coerces non-negative real numbers (`ℝ≥0`) into real numbers (`ℝ`), is a monotone function. This means that for any two non-negative real numbers `a` and `b`, if `a ≤ b` then `NNReal.toReal a ≤ NNReal.toReal b`. In simpler terms, the function preserves the order of the non-negative real numbers when they are converted into real numbers.
More concisely: The `NNReal.toReal` function that coerces non-negative real numbers into real numbers is monotone, i.e., for all non-negative real numbers `a` and `b` with `a ≤ b`, `NNReal.toReal a ≤ NNReal.toReal b`.
|
NNReal.abs_eq
theorem NNReal.abs_eq : ∀ (x : NNReal), |↑x| = ↑x
This theorem states that for every nonnegative real number `x` (denoted as `NNReal`), the absolute value of `x` (expressed as `|↑x|`) is equal to `x` itself (expressed as `↑x`). In mathematical terms, it would be stated as "For all x in the set of nonnegative real numbers, the absolute value of x equals x". This is expected because, by the definition of nonnegative real numbers, `x` is always greater than or equal to 0, so its absolute value is just `x` itself.
More concisely: For all non-negative real numbers x, |x| = x holds.
|
Mathlib.Data.Real.NNReal._auxLemma.29
theorem Mathlib.Data.Real.NNReal._auxLemma.29 : ∀ {q : NNReal}, (0 ≤ ↑q) = True
This theorem states that for every nonnegative real number `q`, the assertion that `q` is greater than or equal to zero is always true. In other words, it's a formal statement about a property of nonnegative real numbers: they are always, by definition, greater than or equal to zero.
More concisely: For every non-negative real number `q`, we have `q ≥ 0`.
|
Real.toNNReal_one
theorem Real.toNNReal_one : Real.toNNReal 1 = 1
This theorem states that when we convert the real number 1 into a non-negative real number using the function `Real.toNNReal`, we get 1. In other words, the function `Real.toNNReal` when applied to 1 produces 1 as the output. The function `Real.toNNReal` is designed to provide zero if the input is less than zero, but since 1 is not less than zero, the function just returns 1 as expected.
More concisely: The theorem asserts that `Real.toNNReal 1` equals 1.
|
NNReal.eq
theorem NNReal.eq : ∀ {n m : NNReal}, ↑n = ↑m → n = m
This theorem states that for any two nonnegative real numbers `n` and `m`, if the underlying real number representation of `n` (denoted by `↑n`) is equal to the underlying real number representation of `m` (denoted by `↑m`), then `n` is equal to `m`. In other words, it asserts the injectivity of the inclusion map from the nonnegative real numbers to the real numbers.
More concisely: If two non-negative real numbers have the same underlying real number representation, then they are equal.
|
Real.toNNReal_mono
theorem Real.toNNReal_mono : Monotone Real.toNNReal
The theorem `Real.toNNReal_mono` states that the function `Real.toNNReal`, which converts a real number to a non-negative real number (returning `0` if the input is less than `0`), is monotone. This means that for any two real numbers `a` and `b`, if `a` is less than or equal to `b`, then `Real.toNNReal a` is also less than or equal to `Real.toNNReal b`. In other words, the function preserves the order of the real numbers when they are mapped to non-negative real numbers.
More concisely: For all real numbers `a` and `b` with `a ≤ b`, we have `Real.toNNReal a ≤ Real.toNNReal b`.
|
Mathlib.Data.Real.NNReal._auxLemma.18
theorem Mathlib.Data.Real.NNReal._auxLemma.18 : ∀ {r₁ r₂ : NNReal}, (↑r₁ ≤ ↑r₂) = (r₁ ≤ r₂)
The theorem `Mathlib.Data.Real.NNReal._auxLemma.18` states that for any two nonnegative real numbers `r₁` and `r₂`, the inequality `r₁ ≤ r₂` holds if and only if the same inequality holds when `r₁` and `r₂` are coerced to real numbers. In other words, comparing two nonnegative real numbers using the `≤` operator on the original type `NNReal` is equivalent to comparing them using the `≤` operator on the type `Real`.
More concisely: For any nonnegative real numbers `r₁` and `r₂`, `r₁ ≤ r₂` in `NNReal` if and only if `r₁.to Real ≤ r₂.to Real` in `Real`.
|
NNReal.coe_lt_coe
theorem NNReal.coe_lt_coe : ∀ {r₁ r₂ : NNReal}, ↑r₁ < ↑r₂ ↔ r₁ < r₂
This theorem states that for any two nonnegative real numbers (`NNReal`), r₁ and r₂, the condition that the real number representation of r₁ is less than the real number representation of r₂ is equivalent to the condition that r₁ is less than r₂ within the type `NNReal`. This theorem thus guarantees a consistent ordering between nonnegative real numbers when considered either as `NNReal` or as real numbers.
More concisely: For any nonnegative real numbers r₁ and r₂, r₁ < r₂ in the `NNReal` ordering if and only if r₁ < r₂ as real numbers.
|
Real.coe_toNNReal
theorem Real.coe_toNNReal : ∀ (r : ℝ), 0 ≤ r → ↑r.toNNReal = r
The theorem `Real.coe_toNNReal` states that for every real number `r`, if `r` is non-negative (i.e., `r` is greater than or equal to 0), then the coercion of the non-negative real number returned by the function `Real.toNNReal` when applied to `r` is equal to `r` itself. This theorem guarantees that the `Real.toNNReal` function is an identity on non-negative real numbers, when we consider the output as a real number again by applying the coercion function.
More concisely: For all real numbers `r` with `r ≥ 0`, the coercion of `Real.toNNReal r` back to a real number equals `r` itself.
|
NNReal.coe_sSup
theorem NNReal.coe_sSup : ∀ (s : Set NNReal), ↑(sSup s) = sSup (NNReal.toReal '' s)
This theorem states that for any set `s` of nonnegative real numbers (`NNReal`), the supremum (`sSup`) of `s` when cast to real numbers is equal to the supremum (`sSup`) of the set obtained by applying the function `NNReal.toReal` (which casts each nonnegative real number in the set `s` to a real number) to every element of `s`. In other words, taking the supremum before or after converting the entire set of nonnegative real numbers to real numbers doesn't change the value of the supremum.
More concisely: For any set `s` of nonnegative real numbers, the supremum of `s` is equal to the supremum of the set obtained by applying the function `NNReal.toReal` to each element in `s`.
|
NNReal.coe_one
theorem NNReal.coe_one : ↑1 = 1
This theorem states that the coercion of the natural number 1 to the non-negative real numbers is equal to the real number 1. In simpler terms, converting 1 from a natural number to a non-negative real number doesn't change its numeric value, it remains 1.
More concisely: The natural number 1 is equal to its coercion to the non-negative real numbers.
|
NNReal.toNNReal_coe_nat
theorem NNReal.toNNReal_coe_nat : ∀ (n : ℕ), (↑n).toNNReal = ↑n
This theorem states that for any natural number `n`, when it is co-erced (i.e., converted) to a real number and then reinterpreted as a non-negative real number using the `Real.toNNReal` function, it remains the same after being co-erced to a non-negative real number directly. In other words, the two operations of first converting a natural number to a real number and then applying the `Real.toNNReal` function, and the operation of directly co-ercing the natural number to a non-negative real number, are equivalent for all natural numbers.
More concisely: For any natural number `n`, `Real.toNNReal (realOfNat n) = realOfNat (natIntToReal n)`, where `natIntToReal` is the function converting a natural number to a real number.
|
NNReal.coe_sum
theorem NNReal.coe_sum :
∀ {α : Type u_1} {s : Finset α} {f : α → NNReal}, ↑(s.sum fun a => f a) = s.sum fun a => ↑(f a)
This theorem, `NNReal.coe_sum`, states that for any type `α`, any finite set `s` of type `α`, and any function `f` that maps an element of `α` to a nonnegative real number, the real number representation (indicated by `↑`) of the sum of `f(a)` for all `a` in `s` is equal to the sum of the real number representations of `f(a)` for all `a` in `s`. In mathematical terms, for all `s` in finite sets of `α` and all functions `f: α → NNReal`, it holds that `∑_{a ∈ s} f(a) = ∑_{a ∈ s} ↑f(a)`.
More concisely: For any finite set `s` and function `f` mapping elements of type `α` to non-negative reals, the sum of `↑(f(a))` over `a` in `s` equals the sum of `f(a)` over `a` in `s`.
|
NNReal.coe_list_prod
theorem NNReal.coe_list_prod : ∀ (l : List NNReal), ↑l.prod = (List.map NNReal.toReal l).prod
This theorem, `NNReal.coe_list_prod`, states that for any list of nonnegative real numbers (`NNReal`), the real number representation (`toReal`) of the product of the list is equal to the product of the list obtained by mapping each nonnegative real number in the list to its real number representation. In other words, converting a list of nonnegative real numbers to their real number equivalents and then taking the product is the same as taking the product of the nonnegative real numbers first and then converting the result to a real number.
More concisely: For any list of non-negative real numbers, the product of their real number representations is equal to the real number representation of the product of the numbers in the list.
|
Mathlib.Data.Real.NNReal._auxLemma.33
theorem Mathlib.Data.Real.NNReal._auxLemma.33 : ∀ {r : ℝ}, (r.toNNReal = 0) = (r ≤ 0)
This theorem, `Mathlib.Data.Real.NNReal._auxLemma.33`, states that for any real number `r`, the result of applying the `Real.toNNReal` function (which converts a real number to a non-negative real number, returning `0` if the number is less than `0`) to `r` equals `0` if and only if `r` is less than or equal to `0`. In mathematical terms, for all $r \in \mathbb{R}$, $\text{Real.toNNReal}(r) = 0$ if and only if $r \le 0$.
More concisely: For all real numbers $r$, $\text{Real.toNNReal}(r) = 0$ if and only if $r \leq 0$.
|
NNReal.zero_le_coe
theorem NNReal.zero_le_coe : ∀ {q : NNReal}, 0 ≤ ↑q
This theorem states that for any nonnegative real number `q`, the real number it represents is also nonnegative. In other words, if `q` is an element of the set of nonnegative real numbers (`NNReal`), then when `q` is converted to a standard real number (using the coercion function `↑q`), the result will always be greater than or equal to zero. In mathematical terms, for all `q` in `NNReal`, `0 ≤ ↑q`.
More concisely: For any nonnegative real number `q`, its standard real number representation `↑q` is nonnegative.
|
NNReal.coe_inv
theorem NNReal.coe_inv : ∀ (r : NNReal), ↑r⁻¹ = (↑r)⁻¹
This theorem states that for all nonnegative real numbers `r`, the operation of taking the multiplicative inverse (or reciprocal) commutes with the coercion operation from nonnegative real numbers to real numbers. In other words, for any `r` in the set of nonnegative real numbers, the inverse of the coerced value of `r` (that is, treating `r` as a regular real number and finding its multiplicative inverse) is the same as the coerced value of the inverse of `r`. In mathematical notations, it can be written as: for all $r \in \text{NNReal}$, $(r^{-1})^\vee = (r^\vee)^{-1}$ where $^\vee$ denotes the coercion.
More concisely: For all non-negative real numbers $r$, $(r^{-1})^\vee = (r^\vee)^{-1}$, where $\vee$ denotes the coercion.
|
Mathlib.Data.Real.NNReal._auxLemma.1
theorem Mathlib.Data.Real.NNReal._auxLemma.1 : ∀ {r₁ r₂ : NNReal}, (↑r₁ = ↑r₂) = (r₁ = r₂)
This theorem states that for every pair of non-negative real numbers `r₁` and `r₂`, the equality of their coercions (treating them as normal real numbers) is equivalent to their equality as non-negative real numbers. In other words, two non-negative real numbers are considered the same if and only if they are equal when treated as just real numbers.
More concisely: For all non-negative real numbers `r₁` and `r₂`, `r₁ = r₂` if and only if their real coercions are equal: `ℝ.coe r₁ = ℝ.coe r₂`.
|
NNReal.coe_iInf
theorem NNReal.coe_iInf : ∀ {ι : Sort u_1} (s : ι → NNReal), ↑(⨅ i, s i) = ⨅ i, ↑(s i)
This theorem asserts that for any indexed family of nonnegative real numbers (`NNReal`), the infimum (greatest lower bound) of the entire family, when considered as an element of the real numbers (which is what the ↑ notation indicates), is equal to the infimum of the images of the individual elements under the canonical embedding of nonnegative real numbers into the real numbers. In simpler terms, it says that taking the infimum then mapping to the real numbers gives the same result as first mapping each element of the family to the real numbers then taking the infimum.
More concisely: The inf inf (x : ℝ↑^∞) = inf (map ℝ⊙ x) where ℝ↑^∞ is the type of indexed nonnegative real numbers and ℝ⊙ is the canonical embedding of nonnegative real numbers into the real numbers.
|
Real.toNNReal_le_toNNReal
theorem Real.toNNReal_le_toNNReal : ∀ {r p : ℝ}, r ≤ p → r.toNNReal ≤ p.toNNReal
This theorem states that for all real numbers `r` and `p`, if `r` is less than or equal to `p`, then the non-negative real number equivalent of `r` (which is `0` if `r` is less than `0`) is less than or equal to the non-negative real number equivalent of `p`. In mathematical terms, for any $r, p \in \mathbb{R}$, if $r \leq p$ then $\text{toNNReal}(r) \leq \text{toNNReal}(p)$, where $\text{toNNReal}$ is a function that converts a real number to a non-negative real number by taking the maximum of the number and zero.
More concisely: For all real numbers $r$ and $p$, if $r \leq p$, then $0 \lor r \leq 0 \lor p \implies \text{toNNReal}(r) \leq \text{toNNReal}(p)$, where $\text{toNNReal}$ is the function mapping $r$ to $0$ if $r < 0$ and to $r$ otherwise.
|
NNReal.coe_iSup
theorem NNReal.coe_iSup : ∀ {ι : Sort u_1} (s : ι → NNReal), ↑(⨆ i, s i) = ⨆ i, ↑(s i)
This theorem states that for any indexed set of nonnegative real numbers, the supremum of the set (if it exists) when considered as a real number, is equal to the supremum of the set of the corresponding real numbers. In other words, taking supremum doesn't change when we switch between considering the elements of the set as nonnegative real numbers or as real numbers.
More concisely: For any indexed set of nonnegative real numbers, the supremum of the set as a nonnegative real number equals the supremum of the set considered as a subset of the real numbers.
|
NNReal.coe_inj
theorem NNReal.coe_inj : ∀ {r₁ r₂ : NNReal}, ↑r₁ = ↑r₂ ↔ r₁ = r₂
The theorem `NNReal.coe_inj` states that for any two nonnegative real numbers `r₁` and `r₂`, the proposition that their coerced values are equal is equivalent to the proposition that `r₁` and `r₂` themselves are equal. In simpler terms, this theorem is about the injectivity of the coercion function on nonnegative real numbers; it says that if the real-number representations of two nonnegative real numbers are the same, then the two nonnegative real numbers themselves must be the same, and vice versa.
More concisely: The coercion function from nonnegative real numbers to their real representations is an injective function.
|
Mathlib.Data.Real.NNReal._auxLemma.7
theorem Mathlib.Data.Real.NNReal._auxLemma.7 : ∀ {r : NNReal}, (↑r = 0) = (r = 0)
This theorem states that for any nonnegative real number `r`, `r` is equal to `0` if and only if its coercion to a real number is equal to `0`. In other words, a nonnegative real number `r` is zero if and only if it is zero when considered as a real number. This theorem connects the equality of `r` in two different types, `NNReal` and `Real` - asserting that equality in one implies equality in the other.
More concisely: For any nonnegative real number `r`, `r = 0` if and only if its real number representation `real r = 0`.
|
Real.toNNReal_eq_zero
theorem Real.toNNReal_eq_zero : ∀ {r : ℝ}, r.toNNReal = 0 ↔ r ≤ 0
This theorem states that for every real number `r`, the function `Real.toNNReal` applied to `r` equals 0 if and only if `r` is less than or equal to 0. In other words, it asserts that `Real.toNNReal`, which converts a real number to a non-negative real number by returning `0` if the input is less than `0`, yields `0` precisely when the input real number is non-positive.
More concisely: For every real number `r`, `Real.toNNReal r = 0 <--> r <= 0`.
|
NNReal.coe_sub
theorem NNReal.coe_sub : ∀ {r₁ r₂ : NNReal}, r₂ ≤ r₁ → ↑(r₁ - r₂) = ↑r₁ - ↑r₂
This theorem states that for any two non-negative real numbers `r₁` and `r₂`, if `r₂` is less than or equal to `r₁`, then the real number coercion of the difference between `r₁` and `r₂` (that is `r₁ - r₂`) is equal to the difference between the real number coercions of `r₁` and `r₂` (that is `↑r₁ - ↑r₂`). Essentially, it's saying that subtraction behaves the same way in the set of all non-negative real numbers as it does in the set of all real numbers, when the second number is less than or equal to the first.
More concisely: For all non-negative real numbers `r₁` and `r₂` with `r₂ ≤ r₁`, the real number coercion of `r₁ - r₂` equals `↑r₁ - ↑r₂`.
|
Real.le_toNNReal_iff_coe_le
theorem Real.le_toNNReal_iff_coe_le : ∀ {r : NNReal} {p : ℝ}, 0 ≤ p → (r ≤ p.toNNReal ↔ ↑r ≤ p)
This theorem states that for any non-negative real number `r` and any real number `p` that is greater than or equal to zero, the non-negative real number `r` is less than or equal to the non-negative real number representation of `p` if and only if the real number equivalent of `r` is less than or equal to `p`. In mathematical terms, for all $r \in \text{NNReal}$ and $p \in \mathbb{R}$ with $p \geq 0$, we have $r \leq \text{Real.toNNReal}(p)$ if and only if $r \leq p$.
More concisely: For any non-negative real number `r` and real number `p` with `p` greater than or equal to zero, `r` is less than or equal to the non-negative real representation of `p` if and only if `r` is less than or equal to `p`. In mathematical notation, for all $r \in \text{NNReal}$ and $p \in \mathbb{R}$ with $p \geq 0$, $r \leq \text{Real.toNNReal}(p) \Leftrightarrow r \leq p$.
|
Real.le_coe_toNNReal
theorem Real.le_coe_toNNReal : ∀ (r : ℝ), r ≤ ↑r.toNNReal
This theorem states that for any real number `r`, `r` is less than or equal to the non-negative real number equivalent of `r`. Specifically, `Real.toNNReal r` is a function that converts a real number `r` into a non-negative real number, and `↑(Real.toNNReal r)` is the coercion of this non-negative real number back to a real number. This theorem guarantees that this process never decreases the value of `r`. If `r` is negative, its non-negative real number equivalent is `0`, and so `r` is less than or equal to `0`. If `r` is non-negative, its non-negative real number equivalent is `r` itself, and so `r` is less than or equal to `r`.
More concisely: For any real number `r`, `r` is less than or equal to its non-negative real number equivalent `↑(Real.toNNReal r)`.
|
NNReal.coe_mul
theorem NNReal.coe_mul : ∀ (r₁ r₂ : NNReal), ↑(r₁ * r₂) = ↑r₁ * ↑r₂
This theorem states that for any two nonnegative real numbers (`NNReal`), the operation of multiplying them together and then taking the underlying real number (as denoted by `↑`) is the same as first taking their underlying real numbers and then multiplying those. In other words, if `r₁` and `r₂` are nonnegative real numbers, then the real number associated with the product `r₁ * r₂` is the same as the product of the real numbers associated with `r₁` and `r₂` respectively. This is a property of multiplication in the context of nonnegative real numbers in Lean 4.
More concisely: For any nonnegative real numbers `r₁` and `r₂`, `↑(r₁ * r₂) = ↑r₁ * ↑r₂`.
|
Real.coe_nnabs
theorem Real.coe_nnabs : ∀ (x : ℝ), ↑(Real.nnabs x) = |x|
This theorem states that for any real number `x`, the coercion (or conversion) of the non-negative absolute value of `x` (`Real.nnabs x`) back to a real number produces the standard absolute value of `x`. In mathematical terms, given any real number `x`, the absolute value `|x|` is equivalent to transforming `x` to a non-negative real number using `Real.nnabs` and then converting it back to a real number.
More concisely: For any real number `x`, the absolute value `|x|` is equal to the coercion of `Real.nnabs x` back to a real number.
|
NNReal.coe_nonneg
theorem NNReal.coe_nonneg : ∀ (r : NNReal), 0 ≤ ↑r
The theorem `NNReal.coe_nonneg` states that for every nonnegative real number `r`, the real number corresponding to `r` (obtained by applying the coercion (`↑r`)) is nonnegative. In other words, the coercion of any element in the set of nonnegative real numbers, denoted as `NNReal`, is always greater than or equal to zero.
More concisely: For every non-negative real number `r`, `↑r` ≥ 0 holds true.
|
NNReal.coe_sInf
theorem NNReal.coe_sInf : ∀ (s : Set NNReal), ↑(sInf s) = sInf (NNReal.toReal '' s)
This theorem states that for any set `s` of nonnegative real numbers (`NNReal`), the greatest lower bound (infimum) of `s` when coerced into the set of real numbers is equal to the greatest lower bound of the image of `s` under the coercion function `NNReal.toReal`. In other words, taking the infimum of a set of nonnegative real numbers and then mapping it to the real numbers is the same as first mapping the set to the real numbers and then taking the infimum.
More concisely: For any set `s` of nonnegative real numbers, the infimum of `s` equals the infimum of `NNReal.toReal s`.
|
Mathlib.Data.Real.NNReal._auxLemma.16
theorem Mathlib.Data.Real.NNReal._auxLemma.16 :
∀ {α : Type u_1} {s : Finset α} {f : α → NNReal}, (s.sum fun a => ↑(f a)) = ↑(s.sum fun a => f a)
This theorem states that for any type `α`, any finite set `s` of type `α`, and any function `f` from `α` to the nonnegative real numbers (NNReal), the sum of the values of `f` when applied to the elements of `s` is the same whether you first convert `f a` to a real number and then sum, or first sum over `f a` and then convert to a real number. That is, the operation of summing over a finite set commutes with the operation of converting a nonnegative real number to a real number.
More concisely: For any type `α`, any finite set `s` of type `α`, and any function `f` from `α` to the non-negative real numbers, the sum of `(f a)` for all `a` in `s` is equal to the real number obtained by summing the real numbers `(f !a)` for all `a` in `s`.
|
NNReal.coe_eq_one
theorem NNReal.coe_eq_one : ∀ {r : NNReal}, ↑r = 1 ↔ r = 1
This theorem states that for any nonnegative real number `r`, the coercion of `r` to a real number equals 1 if and only if `r` itself equals 1. In other words, the only nonnegative real number that, when considered as a normal real number, equals 1, is the nonnegative real number 1 itself.
More concisely: For any non-negative real number `r`, `r = 1` if and only if the coercion of `r` to a real number is equal to 1.
|
Real.toNNReal_le_toNNReal_iff
theorem Real.toNNReal_le_toNNReal_iff : ∀ {r p : ℝ}, 0 ≤ p → (r.toNNReal ≤ p.toNNReal ↔ r ≤ p)
The theorem `Real.toNNReal_le_toNNReal_iff` states that for any two real numbers `r` and `p`, where `p` is greater than or equal to zero, the non-negative real number interpretation of `r` is less than or equal to the non-negative real number interpretation of `p` if and only if `r` is less than or equal to `p`. In other words, the comparison of `r` and `p` remains the same whether they are interpreted as non-negative real numbers or as their original real numbers, given that `p` is non-negative.
More concisely: For any real numbers `r` and `p` with `p ≥ 0`, `Real.toNNReal r ≤ Real.toNNReal p` if and only if `r ≤ p`.
|
NNReal.mul_finset_sup
theorem NNReal.mul_finset_sup :
∀ {α : Type u_1} (r : NNReal) (s : Finset α) (f : α → NNReal), r * s.sup f = s.sup fun a => r * f a
The theorem `NNReal.mul_finset_sup` asserts that for any type `α`, any nonnegative real number `r`, any finite set `s` of elements of type `α`, and any function `f` from `α` to nonnegative real numbers, the product of `r` and the supremum (greatest element) of the set obtained by applying `f` to every element of `s` is equal to the supremum of the set obtained by multiplying `r` with the application of `f` to each element of `s`. In mathematical terms, it can be denoted as `r * sup(f(s)) = sup(r * f(a))` for all `a` in `s`.
More concisely: For any nonnegative real number `r`, finite set `s` of elements from type `α`, and function `f` from `α` to nonnegative real numbers, `r * sup(f(s)) = sup(r * f(x) | x ∈ s)`.
|
Real.toNNReal_mul
theorem Real.toNNReal_mul : ∀ {p q : ℝ}, 0 ≤ p → (p * q).toNNReal = p.toNNReal * q.toNNReal
The theorem `Real.toNNReal_mul` states that for all real numbers `p` and `q`, if `p` is non-negative (i.e., `p` is greater than or equal to zero), then the function `Real.toNNReal` applied to the product of `p` and `q` is equal to the product of `Real.toNNReal p` and `Real.toNNReal q`. In other words, this theorem verifies the preserving property of multiplication under the `Real.toNNReal` function for non-negative real numbers.
More concisely: For all non-negative real numbers `p` and `q`, `Real.toNNReal (p * q) = Real.toNNReal p * Real.toNNReal q`.
|
NNReal.coe_le_coe
theorem NNReal.coe_le_coe : ∀ {r₁ r₂ : NNReal}, ↑r₁ ≤ ↑r₂ ↔ r₁ ≤ r₂
This theorem states that for any two nonnegative real numbers `r₁` and `r₂`, the inequality `r₁ ≤ r₂` holds if and only if the inequality holds when `r₁` and `r₂` are coerced to real numbers, i.e., `↑r₁ ≤ ↑r₂`. In other words, the order of nonnegative real numbers is preserved under the coercion from `NNReal` to `Real`.
More concisely: For all nonnegative real numbers `r₁` and `r₂`, `r₁ ≤ r₂` if and only if `↑r₁ ≤ ↑r₂`.
|
NNReal.coe_pow
theorem NNReal.coe_pow : ∀ (r : NNReal) (n : ℕ), ↑(r ^ n) = ↑r ^ n
This theorem states that for any nonnegative real number `r` and any natural number `n`, the action of raising `r` to the power of `n` (denoted `r^n`) and then taking the real part (denoted `(r ^ n).to_real`) is equivalent to first taking the real part of `r` (denoted `r.to_real`) and then raising it to the power of `n`. In other words, the operations of exponentiation and taking the real part commute for nonnegative real numbers and natural number exponents.
More concisely: For any non-negative real number `r` and natural number `n`, `(r.to_real ^ n) = (r.to_real ^ n)`. That is, real part commuting with power operation for non-negative real numbers and natural number exponents.
|
Mathlib.Data.Real.NNReal._auxLemma.19
theorem Mathlib.Data.Real.NNReal._auxLemma.19 : ∀ {r₁ r₂ : NNReal}, (↑r₁ < ↑r₂) = (r₁ < r₂)
This theorem, from the Mathlib library in Lean 4, states that for any two nonnegative real numbers `r₁` and `r₂`, the condition "the value of `r₁` is less than the value of `r₂`" is equivalent to "the real number represented by `r₁` is less than the real number represented by `r₂`". Here, `NNReal` refers to the type of nonnegative real numbers, and `↑r₁` and `↑r₂` denote the real numbers corresponding to `r₁` and `r₂`, respectively.
More concisely: For any `r₁, r₂ : NNReal`, `r₁ < r₂` if and only if `↑r₁ < ↑r₂`.
|
Real.toNNReal_add
theorem Real.toNNReal_add : ∀ {r p : ℝ}, 0 ≤ r → 0 ≤ p → (r + p).toNNReal = r.toNNReal + p.toNNReal
The theorem `Real.toNNReal_add` states that for all real numbers `r` and `p`, if `r` and `p` are both non-negative, then the function `Real.toNNReal` applied to the sum of `r` and `p` is equal to the sum of `Real.toNNReal r` and `Real.toNNReal p`. In other words, we can either sum two non-negative real numbers first and then apply `Real.toNNReal`, or apply `Real.toNNReal` first and then sum the results, and both will give us the same output.
More concisely: For all non-negative real numbers `r` and `p`, `Real.toNNReal (r + p) = Real.toNNReal r + Real.toNNReal p`.
|
NNReal.div_le_iff
theorem NNReal.div_le_iff : ∀ {a b r : NNReal}, r ≠ 0 → (a / r ≤ b ↔ a ≤ b * r)
The theorem `NNReal.div_le_iff` is stating that for any nonnegative real numbers `a`, `b`, and `r`, given that `r` is not equal to zero, then the quotient of `a` divided by `r` is less than or equal to `b` if and only if `a` is less than or equal to the product of `b` and `r`. This theorem provides a way to compare fractions and products in the context of nonnegative real numbers.
More concisely: For nonnegative real numbers `a`, `b`, and `r` with `r != 0`, `a / r <= b` if and only if `a <= b * r`.
|
NNReal.coe_add
theorem NNReal.coe_add : ∀ (r₁ r₂ : NNReal), ↑(r₁ + r₂) = ↑r₁ + ↑r₂
This theorem, `NNReal.coe_add`, states that for all non-negative real numbers `r₁` and `r₂`, the coercion of the sum of `r₁` and `r₂` to a real number is equal to the sum of the coercions of `r₁` and `r₂` to real numbers. In other words, this theorem ensures that the operation of sum in the set of non-negative real numbers is compatible with the natural inclusion of this set into the set of all real numbers.
More concisely: For all non-negative real numbers `r₁` and `r₂`, Coerce(r₁ + r₂, Real) = Coerce(r₁, Real) + Coerce(r₂, Real).
|
Real.toNNReal_le_iff_le_coe
theorem Real.toNNReal_le_iff_le_coe : ∀ {r : ℝ} {p : NNReal}, r.toNNReal ≤ p ↔ r ≤ ↑p
This theorem states that for any real number `r` and any non-negative real number `p`, the non-negative real number interpretation of `r` is less than or equal to `p` if and only if `r` is less than or equal to the real number representation of `p`. In other words, it allows for a direct comparison between a real number `r` and a non-negative real number `p` by either comparing `r` with the real part of `p`, or comparing the non-negative real interpretation of `r` with `p` itself.
More concisely: For any real numbers r and non-negative real number p, r ≤ p if and only if ℝ≤[r] ≤ p, where ℝ≤[r] denotes the non-negative real interpretation of r.
|
NNReal.coe_prod
theorem NNReal.coe_prod :
∀ {α : Type u_1} {s : Finset α} {f : α → NNReal}, ↑(s.prod fun a => f a) = s.prod fun a => ↑(f a)
The theorem `NNReal.coe_prod` states that for any type `α`, any finite set `s` of type `α`, and any function `f` mapping elements of `α` to nonnegative real numbers (`NNReal`), the real number representation of the product of `f a` for each `a` in `s` is equal to the product of the real number representations of `f a` for each `a` in `s`. This is equivalent to saying that taking the product of the nonnegative real number results first and then converting to real numbers is the same as converting each nonnegative real number result to a real number first and then taking the product.
More concisely: For any type `α`, finite set `s` of `α`, and function `f` mapping `α` to nonnegative real numbers, the real number representation of the product of `f a` for each `a` in `s` equals the product of the real number representations of `f a` for each `a` in `s`.
|
Real.toNNReal_lt_toNNReal_iff'
theorem Real.toNNReal_lt_toNNReal_iff' : ∀ {r p : ℝ}, r.toNNReal < p.toNNReal ↔ r < p ∧ 0 < p
The theorem `Real.toNNReal_lt_toNNReal_iff'` states that for any two real numbers `r` and `p`, the non-negative real number reinterpretation of `r` is less than the non-negative real number reinterpretation of `p` if and only if `r` is less than `p` and `p` is greater than `0`. This theorem relates the ordering of real numbers to the ordering of their non-negative reinterpretations.
More concisely: For any real numbers r and p, r < p and p > 0 if and only if ℝ⁺(r) < ℝ⁺(p), where ℝ⁺ denotes the non-negative real number reinterpretation.
|
NNReal.coe_pos
theorem NNReal.coe_pos : ∀ {r : NNReal}, 0 < ↑r ↔ 0 < r
This theorem states that for every nonnegative real number `r`, the value of `r` is positive if and only if the coercion of `r` (i.e., `r` considered as a real number) is positive. This involves the logical biconditional (`↔`), signifying that the positiveness of the original nonnegative real number and its real number counterpart are equivalent.
More concisely: For every nonnegative real number `r`, `r` is positive if and only if its real number coercion is positive.
|