continuous_real_toNNReal
theorem continuous_real_toNNReal : Continuous Real.toNNReal
The theorem `continuous_real_toNNReal` states that the function `Real.toNNReal`, which reinterprets a real number as a non-negative real number (returning `0` if the real number is less than `0`), is continuous. In other words, for any sequence of real numbers that converges to a limit, the sequence of their non-negative reinterpretations also converges to the non-negative reinterpretation of the limit.
More concisely: The function `Real.toNNReal : Real → ℝ⁺` is continuous, where `ℝ⁺` denotes the set of non-negative real numbers. That is, for any real number sequence `(x_n)` that converges to a limit `x`, `(Real.toNNReal x_n)` converges to `Real.toNNReal x`.
|
Mathlib.Topology.Instances.NNReal._auxLemma.6
theorem Mathlib.Topology.Instances.NNReal._auxLemma.6 :
∀ {α : Type u_1} {f : α → NNReal}, (Summable fun a => ↑(f a)) = Summable f
This theorem states that for any type `α` and any function `f` from `α` to nonnegative real numbers (notated as `NNReal`), the property that the function mapped to its real number equivalents (using the `↑` operator) is summable is equivalent to the property that the function `f` itself is summable. In other words, `f` is summable over its values in `NNReal` if and only if its real number equivalents are also summable. Summability, in this context, meaning there exists an (infinite) sum of the sequence generated by the function. The proof of this theorem is not provided (`by sorry`).
More concisely: For any type `α` and function `f` from `α` to nonnegative real numbers, `f` is summable if and only if its real number equivalents are summable.
|
NNReal.tendsto_coe
theorem NNReal.tendsto_coe :
∀ {α : Type u_1} {f : Filter α} {m : α → NNReal} {x : NNReal},
Filter.Tendsto (fun a => ↑(m a)) f (nhds ↑x) ↔ Filter.Tendsto m f (nhds x)
This theorem states that for any type `α`, any filter on `α` named `f`, any function `m` from `α` to the nonnegative real numbers `NNReal`, and any nonnegative real number `x`, the function `m` tends towards `x` with respect to the filter `f` if and only if the real part of the function `m`, denoted by `(fun a => ↑(m a))`, tends towards the real part of `x` with respect to the filter `f`. This basically connects the limit concepts in the context of nonnegative real numbers and their real counter-part.
More concisely: For any type `α`, filter `f` on `α`, function `m` from `α` to `NNReal`, and real number `x`, the function `m` tends towards `x` with respect to `f` if and only if the real part of `m` tends towards the real part of `x` with respect to `f`.
|
NNReal.coe_tsum
theorem NNReal.coe_tsum : ∀ {α : Type u_1} {f : α → NNReal}, ↑(∑' (a : α), f a) = ∑' (a : α), ↑(f a)
This theorem states that for any type `α` and any function `f` from `α` to the set of nonnegative real numbers (`NNReal`), the sum of the images of `f` (denoted as `(∑' (a : α), f a)`) is the same as the sum of the images of `f` after they have been converted to real numbers (denoted as `∑' (a : α), ↑(f a)`). In other words, the conversion to real numbers (`↑` or `coe`) commutes with the operation of taking the sum over all elements of type `α`.
More concisely: For any type `α` and function `f` from `α` to `NNReal`, the sum of `f` applied to all elements of `α` is equal to the sum of the real numbers obtained by applying `f` to each element and then converting to real numbers. In Lean syntax, `(∑' (a : α), f a) = ∑' (a : α), ↑(f a)`.
|
NNReal.tendsto_tsum_compl_atTop_zero
theorem NNReal.tendsto_tsum_compl_atTop_zero :
∀ {α : Type u_1} (f : α → NNReal), Filter.Tendsto (fun s => ∑' (b : { x // x ∉ s }), f ↑b) Filter.atTop (nhds 0)
This theorem states that for a function `f` mapping from any type `α` to the nonnegative real numbers (`NNReal`), the sum of `f` over the complement of a finset tends towards `0` as the finset grows to cover the entire space. Here, the complement of a finset is the set of all elements that are not included in the finset, and this sum is taken over all such elements. The theorem does not require an assumption of summability because if this were not the case, all of the sums would be zero. In terms of filters, this is saying that the function mapping a finset to the sum over its complement is tending to `0` at the filter `atTop`, which represents the limit as the finset becomes larger and larger.
More concisely: For any real-valued function `f` on type `α`, the limit as the complement of a growing finset approaches the entire space is the sum of `f` over the complement tending towards 0.
|
NNReal.hasSum_coe
theorem NNReal.hasSum_coe : ∀ {α : Type u_1} {f : α → NNReal} {r : NNReal}, HasSum (fun a => ↑(f a)) ↑r ↔ HasSum f r
This theorem states that for any type `α` and any function `f` from `α` to non-negative real numbers (`NNReal`), and any nonnegative real number `r`, the function `f` has a sum equal to `r` if and only if the function obtained by applying the coercion function (which converts nonnegative real numbers to real numbers) to `f` also has a sum equal to the coercion of `r`. In other words, if you sum the outputs of the function `f` and get `r`, then if you convert all the outputs of `f` and `r` to real numbers and then sum, you should still get the same sum.
More concisely: For any function `f` from type `α` to non-negative real numbers `NNReal` and any `r` in `NNReal`, the condition that `∑x:α. f x = r` if and only if `∑x:α. coe to Real (f x) = coe to Real r` holds.
|
HasSum.toNNReal
theorem HasSum.toNNReal :
∀ {α : Type u_1} {f : α → ℝ} {y : ℝ},
(∀ (n : α), 0 ≤ f n) → HasSum f y → HasSum (fun x => (f x).toNNReal) y.toNNReal
This theorem states that for any type `α`, any function `f` from `α` to the real numbers `ℝ`, and any real number `y`, if all values of `f` are non-negative (i.e., for every `n` in `α`, `f(n)` is greater than or equal to 0), and `f` has a sum `y`, then the function which converts each value of `f` to a non-negative real number using `Real.toNNReal` also has a sum, which is the non-negative real number corresponding to `y` obtained via `Real.toNNReal`. In essence, it asserts that summing a sequence of real numbers (which are all non-negative) and then converting the sum to a non-negative real number is the same as first converting every term in the sequence to a non-negative real number and then summing them.
More concisely: For any function `f` from a type `α` to `ℝ` with non-negative values, and any `y` being the sum of `f`, the function `Real.toNNReal ∘ f` also has `Real.toNNReal y` as its sum.
|
NNReal.continuous_coe
theorem NNReal.continuous_coe : Continuous NNReal.toReal
This theorem states that the function `NNReal.toReal`, which coerces non-negative real numbers (`ℝ≥0`) to real numbers (`ℝ`), is continuous. In terms of mathematical language, this means that for every real number `r`, if we consider a sequence of non-negative real numbers that converges to `r`, then the corresponding sequence of coerced values in `ℝ` also converges to `r`.
More concisely: The function `NNReal.toReal` is continuous from the ordered field of non-negative real numbers to the real numbers.
|
NNReal.summable_coe
theorem NNReal.summable_coe : ∀ {α : Type u_1} {f : α → NNReal}, (Summable fun a => ↑(f a)) ↔ Summable f
This theorem states that for any type `α` and function `f` from `α` to nonnegative real numbers (`NNReal`), the function `f` is summable (i.e., it has an infinite sum) if and only if the function that takes `a` in `α` to the real number equivalent of `f(a)` (denoted by `↑(f a)`) is summable. In other words, `f` and the function mapping each `a` to its real-valued counterpart have the same summability status.
More concisely: The function `f : α -> NNReal` is summable if and only if the function `↑(f) : α -> Real` is summable.
|