LeanAide GPT-4 documentation

Module: Mathlib.Topology.Instances.ENNReal

Mathlib.Topology.Instances.ENNReal._auxLemma.48

theorem Mathlib.Topology.Instances.ENNReal._auxLemma.48 : ∀ {β : Type u_2} {f : β → NNReal}, Summable f = (∑' (b : β), ↑(f b) ≠ ⊤)

This theorem states that for any type `β` and any function `f` from `β` to nonnegative real numbers (denoted by `NNReal`), the function `f` is summable (meaning it has some infinite sum) if and only if the infinite sum of the function values (obtained by applying `f` to every element of `β` and then taking the sum) is not equal to positive infinity. This is denoted by the `≠ ⊤` symbol. In other words, it's saying that a function `f` has some infinite sum as long as that sum doesn't turn out to be infinity.

More concisely: A function from a type to non-negative real numbers is summable if and only if the sum of its values is finite.

ENNReal.le_tsum

theorem ENNReal.le_tsum : ∀ {α : Type u_1} {f : α → ENNReal} (a : α), f a ≤ ∑' (a : α), f a

This theorem states that for any type `α` and for any function `f` from `α` to the extended nonnegative real numbers (`ENNReal`), for any element `a` of `α`, the value of the function `f` at `a` is less than or equal to the sum over all elements of `α` of the function `f`. In other words, in mathematical notation, for all `a` in `α`, we have `f(a) ≤ Σ f(a')` where the sum is taken over all `a'` in `α`. This represents a fundamental property of sums in the context of measure theory.

More concisely: For any function `f` from a type `α` to extended nonnegative real numbers, and for any `a` in `α`, we have `f(a) ≤ Σ (f a')` where the sum is taken over all `a'` in `α`.

ENNReal.sum_le_tsum

theorem ENNReal.sum_le_tsum : ∀ {α : Type u_1} {f : α → ENNReal} (s : Finset α), (s.sum fun x => f x) ≤ ∑' (x : α), f x

This theorem states that for any function `f` from an arbitrary type `α` to the extended nonnegative real numbers (`ENNReal`), and for any finite set `s` of type `α`, the sum of the function values over this finite set, denoted as `(Finset.sum s fun x => f x)`, is less than or equal to the total sum of the function values over all elements of type `α`, denoted as `∑' (x : α), f x`. In other words, the total measure of a finite subset will always be less than or equal to the total measure of the entire set.

More concisely: For any function from an arbitrary type to extended nonnegative real numbers, the sum of the function values over a finite subset is less than or equal to the sum of the function values over the entire set.

ENNReal.tsum_comm

theorem ENNReal.tsum_comm : ∀ {α : Type u_1} {β : Type u_2} {f : α → β → ENNReal}, ∑' (a : α) (b : β), f a b = ∑' (b : β) (a : α), f a b := by sorry

This theorem, `ENNReal.tsum_comm`, states that for any two types `α` and `β`, and any function `f` mapping from `α` to `β` to the extended nonnegative real numbers `ENNReal`, the sum over `α` first and then `β` is equal to the sum over `β` first and then `α`. In mathematical terms, the theorem asserts the commutativity of the double summation, i.e., $\sum'_{a} \sum'_{b} f(a, b) = \sum'_{b} \sum'_{a} f(a, b)$, where the summation is over all elements of the respective types.

More concisely: The theorem asserts that for any function from two types to extended nonnegative real numbers, the order of double summation commutes: $\sum'_{a} \sum'_{b} f(a, b) = \sum'_{b} \sum'_{a} f(a, b)$.

ENNReal.continuousAt_mul_const

theorem ENNReal.continuousAt_mul_const : ∀ {a b : ENNReal}, a ≠ ⊤ ∨ b ≠ 0 → ContinuousAt (fun x => x * a) b

This theorem states that for any two extended nonnegative real numbers `a` and `b`, if `a` is different from positive infinity or `b` is different from zero, then the function that multiplies `x` by `a` is continuous at `b`. In terms of mathematics, if we have two numbers `a` and `b` from the set [0, ∞], and if `a` is any number other than ∞ or `b` is any number other than 0, then the function `f(x) = xa` is continuous at `x = b`.

More concisely: For any `a in [0, ∞)` different from positive infinity and `b in (0, ∞]`, the function `f(x) = x * a` is continuous at `x = b`.

EMetric.diam_closure

theorem EMetric.diam_closure : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (s : Set α), EMetric.diam (closure s) = EMetric.diam s

This theorem, `EMetric.diam_closure`, states that for any set `s` in a pseudoemetric space `α`, the diameter of the closure of `s` is equal to the diameter of `s` itself. Here, the diameter of a set in a pseudoemetric space is defined as the supremum of the extended distances between any two points in the set, and the closure of a set is the smallest closed set that contains the original set.

More concisely: In a pseudometric space, the diameter of a set equals the diameter of its closure.

Mathlib.Topology.Instances.ENNReal._auxLemma.45

theorem Mathlib.Topology.Instances.ENNReal._auxLemma.45 : ∀ {α : Type u_1} {f : α → ENNReal}, (∑' (i : α), f i = 0) = ∀ (i : α), f i = 0

The theorem states that for any type `α` and any function `f` from `α` to the extended nonnegative real numbers (usually denoted as [0, ∞]), the sum over all `α` of the function `f` is equal to 0 if and only if for all `α`, the function `f` at `α` is equal to 0. In mathematical terms, given a set `α` and a function `f : α → [0, ∞]`, we have `∑' f = 0` if and only if `∀ i ∈ α, f(i) = 0`.

More concisely: The theorem asserts that a function `f : α → [0, ∞]` sums to zero over all `α` if and only if each `i ∈ α` has `f(i) = 0`.

Mathlib.Topology.Instances.ENNReal._auxLemma.12

theorem Mathlib.Topology.Instances.ENNReal._auxLemma.12 : ∀ {α : Type u} {β : Type v} {γ : Type w} {f : β → γ} {g : α → β} {x : Filter α} {y : Filter γ}, Filter.Tendsto f (Filter.map g x) y = Filter.Tendsto (f ∘ g) x y

This theorem states that for any types `α`, `β`, and `γ`, along with any functions `f : β → γ` and `g : α → β`, and any filters `x : Filter α` and `y : Filter γ`, the tendency of function `f` over the filter obtained by mapping `g` over `x` towards `y` is equivalent to the tendency of the composition of `f` and `g` over the filter `x` towards `y`. In other words, it asserts that the limits when taken in sequence or when taken after composition of functions, are the same. This is a key property in the analysis related to the continuity and limits of function compositions.

More concisely: For any types `α`, `β`, and `γ`, functions `f : β → γ` and `g : α → β`, filters `x : Filter α` and `y : Filter γ`, the tendency of `f` over `g(x)` towards `y` equals the tendency of `f ∘ g` over `x` towards `y`.

NNReal.summable_of_le

theorem NNReal.summable_of_le : ∀ {β : Type u_2} {f g : β → NNReal}, (∀ (b : β), g b ≤ f b) → Summable f → Summable g

The theorem `NNReal.summable_of_le` is about the convergence comparison test of series with nonnegative real values (`ℝ≥0`). It states that for any two functions `f` and `g` from an arbitrary type `β` to nonnegative real numbers (`NNReal`), if for all `b` in `β`, `g(b)` is less than or equal to `f(b)`, and if the series formed by `f` is summable (i.e., it has a finite sum), then the series formed by `g` is also summable. This is a formal statement of the comparison test for convergence of series in real analysis.

More concisely: If `f` is a function from a type `β` to nonnegative real numbers with a sum, and `g` is another such function with `g(b) ≤ f(b)` for all `b` in `β`, then the series formed by `g` is summable.

ENNReal.tendsto_nhds

theorem ENNReal.tendsto_nhds : ∀ {α : Type u_1} {f : Filter α} {u : α → ENNReal} {a : ENNReal}, a ≠ ⊤ → (Filter.Tendsto u f (nhds a) ↔ ∀ ε > 0, ∀ᶠ (x : α) in f, u x ∈ Set.Icc (a - ε) (a + ε))

The theorem `ENNReal.tendsto_nhds` characterizes what it means for a function to have a limit in the extended nonnegative real numbers (i.e., numbers from 0 to infinity). Specifically, for any type `α`, any filter `f` on `α`, any function `u` from `α` to the extended nonnegative real numbers, and any extended nonnegative real number `a` that is not infinity, the function `u` tends towards `a` with respect to the filter `f` if and only if for every positive number `ε`, eventually (i.e., for all sufficiently large elements `x` in the filter `f`), the value of `u(x)` lies in the closed interval from `a - ε` to `a + ε`. This is a generalization of the standard limit concept to include the possibility of the limit being infinity.

More concisely: A function from a filter on a type to extended nonnegative real numbers has a limit with respect to that filter if and only if for every positive ε, the values of the function approach the limit from below and above, up to ε, for all sufficiently large elements in the filter.

Mathlib.Topology.Instances.ENNReal._auxLemma.35

theorem Mathlib.Topology.Instances.ENNReal._auxLemma.35 : ∀ {α : Type u} {β : Type v} {f : Filter α} {m : α → β} {P : β → Prop}, (∀ᶠ (b : β) in Filter.map m f, P b) = ∀ᶠ (a : α) in f, P (m a)

This theorem states that for any types `α` and `β`, any filter `f` of type `α`, any function `m` from `α` to `β`, and any property `P` of type `β`, the property `P` holds eventually for all elements `b` in the filter obtained by mapping `f` through `m` if and only if `P` holds eventually for all elements `a` in `f` when applied to the function `m`. In other words, it states that mapping a filter and checking a property is the same as checking the property after applying the function inside the original filter.

More concisely: For any filters $f$ on type $\alpha$, functions $m:\alpha \to \beta$, and properties $P:\beta$, $P$ holds eventually for $m(\overline{x})$ as $x$ ranges over $f$ if and only if $P$ holds eventually for $x$ as $x$ ranges over $f$.

ENNReal.tendsto_nhds_top_iff_nnreal

theorem ENNReal.tendsto_nhds_top_iff_nnreal : ∀ {α : Type u_1} {m : α → ENNReal} {f : Filter α}, Filter.Tendsto m f (nhds ⊤) ↔ ∀ (x : NNReal), ∀ᶠ (a : α) in f, ↑x < m a

This theorem states that for any type `α`, a function `m` from `α` to the extended nonnegative real numbers (`ENNReal`), and a filter `f` on `α`, the function `m` converges to infinity with respect to the filter `f` (denoted as `Filter.Tendsto m f (nhds ⊤)`) if and only if for every nonnegative real number `x`, eventually (for all elements `a : α` in the filter `f`), the real number `x` is less than the output of the function `m` at `a` (expressed as `↑x < m a`). Here, 'eventually' is a concept in filter theory, meaning that the statement holds true at least from a certain point onwards in the filter. The `↑x` notation is used to denote the embedding of the nonnegative real number `x` into the extended nonnegative real numbers.

More concisely: A function from a type to extended nonnegative real numbers converges to infinity with respect to a filter if and only if for every non-negative real number, there exists a filter element such that the function value at that element is strictly greater than the number.

ENNReal.biSup_add'

theorem ENNReal.biSup_add' : ∀ {a : ENNReal} {ι : Sort u_4} {p : ι → Prop}, (∃ i, p i) → ∀ {f : ι → ENNReal}, (⨆ i, ⨆ (_ : p i), f i) + a = ⨆ i, ⨆ (_ : p i), f i + a

The theorem `ENNReal.biSup_add'` states that for any extended nonnegative real number 'a', and any indexed family of extended nonnegative real numbers 'f' indexed by a type 'ι', where at least one element 'i' of type 'ι' satisfies a certain property 'p', the supremum of 'f' under the constraint 'p' plus 'a' is equal to the supremum of the sum of 'f' and 'a' under the same constraint 'p'. In mathematical terms, it states that if ∃i, p(i) is true, then sup{i | p(i)} (f(i) + a) = sup{i | p(i)} f(i) + a.

More concisely: For any extended nonnegative real number 'a' and indexed family 'f' of extended nonnegative real numbers indexed by type 'ι', where there exists an 'i' in 'ι' satisfying property 'p', the supremum of 'f(i) + a' under constraint 'p' equals the sum of the supremum of 'f' under constraint 'p' and 'a'.

ENNReal.tendsto_coe

theorem ENNReal.tendsto_coe : ∀ {α : Type u_1} {f : Filter α} {m : α → NNReal} {a : NNReal}, Filter.Tendsto (fun a => ↑(m a)) f (nhds ↑a) ↔ Filter.Tendsto m f (nhds a)

This theorem, `ENNReal.tendsto_coe`, states that for any type `α`, any filter `f` on `α`, any function `m` from `α` to the nonnegative real numbers (NNReal), and any nonnegative real number `a`, the function `m` tends to the neighborhood filter of `a` with respect to the filter `f` if and only if the function that applies `m` and then takes the real part also tends to the neighborhood filter of the real part of `a` with respect to the filter `f`. In mathematical terms, $\lim_{x \to a} m(x) = a$ if and only if $\lim_{x \to a} \text{Re}(m(x)) = \text{Re}(a)$, where the limits are taken with respect to the filter `f`.

More concisely: For any filter `f` on type `α`, function `m` from `α` to NNReal, and real number `a`, `m` tends to the neighborhood filter of `a` with respect to `f` if and only if the real part of `m` tends to the neighborhood filter of the real part of `a` with respect to `f`. In Lean notation: `ENNReal.tendsto_coe ∘ m ≃ₛ[f] a ↔ ENNReal.tendsto_coe (Real.map Re) ∘ m ≃ₛ[f] (Real.re a)`.

ENNReal.tsum_le_tsum

theorem ENNReal.tsum_le_tsum : ∀ {α : Type u_1} {f g : α → ENNReal}, (∀ (a : α), f a ≤ g a) → ∑' (a : α), f a ≤ ∑' (a : α), g a

The theorem `ENNReal.tsum_le_tsum` states that for any type `α` and for any two functions `f` and `g` from `α` to the extended nonnegative real numbers (`ENNReal`), if each value of `f` is less than or equal to the corresponding value of `g` for all elements of type `α`, then the sum of all values of `f` is less than or equal to the sum of all values of `g`. In mathematical notation, if $\forall a \in \alpha, f(a) \leq g(a)$, then $\sum_{a \in \alpha} f(a) \leq \sum_{a \in \alpha} g(a)$.

More concisely: For any type `α` and functions `f` and `g` from `α` to `ENNReal` with `f(a) ≤ g(a)` for all `a`, we have `∑(a ∈ α) f(a) ≤ ∑(a ∈ α) g(a)`.

ENNReal.nhdsWithin_Ioi_coe_neBot

theorem ENNReal.nhdsWithin_Ioi_coe_neBot : ∀ {r : NNReal}, (nhdsWithin (↑r) (Set.Ioi ↑r)).NeBot

The theorem `ENNReal.nhdsWithin_Ioi_coe_neBot` states that for every nonnegative real number `r`, the filter, that is the intersection of the neighborhood filter around the point `r` and the filter principal of the set of real numbers greater than `r`, is not a bottom (empty) filter. In other words, there always exists a set in the neighborhood of `r` that intersects with the set of real numbers greater than `r`, and this intersection is not an empty set.

More concisely: For every non-negative real number `r`, the filter of neighborhoods of `r` intersecting the set of real numbers strictly greater than `r` is non-empty.

NNReal.hasSum_iff_tendsto_nat

theorem NNReal.hasSum_iff_tendsto_nat : ∀ {f : ℕ → NNReal} {r : NNReal}, HasSum f r ↔ Filter.Tendsto (fun n => (Finset.range n).sum fun i => f i) Filter.atTop (nhds r)

This theorem states that for any series of non-negative real numbers defined by a function `f` from natural numbers to non-negative real numbers and a specific non-negative real number `r`, the series is said to have a sum equal to `r` (in the sense of the `HasSum` property) if and only if the sequence of partial sums of the series, calculated as the sum of function values over the range from `0` to `n`, converges to `r`. Convergence here is defined using the concept of topological filters, specifically, it means that for any neighborhood of `r`, there exists a natural number `N` such that for all `n >= N`, the `n-th` partial sum of the series is in that neighborhood. This is equivalent to saying that the function mapping each natural number `n` to the `n-th` partial sum of the series approaches `r` as `n` goes to infinity.

More concisely: A series of non-negative real numbers defined by a function `f` from natural numbers to non-negative real numbers has sum `r` if and only if the sequence of partial sums converges to `r`.

Summable.countable_support_nnreal

theorem Summable.countable_support_nnreal : ∀ {α : Type u_1} (f : α → NNReal), Summable f → (Function.support f).Countable

This theorem states that for any function `f` mapping from an arbitrary type `α` to non-negative real numbers (`NNReal`), if the function `f` is summable (i.e., the infinite sum of its output exists), then the set of `α` values for which `f` is non-zero (termed as the "support" of `f`) is countable. In other words, the number of values that the function `f` maps to non-zero numbers is countable when the function is summable.

More concisely: If a function from an arbitrary type to non-negative real numbers is summable, then the support of the function, i.e., the set of inputs mapping to non-zero values, is countable.

hasSum_iff_tendsto_nat_of_nonneg

theorem hasSum_iff_tendsto_nat_of_nonneg : ∀ {f : ℕ → ℝ}, (∀ (i : ℕ), 0 ≤ f i) → ∀ (r : ℝ), HasSum f r ↔ Filter.Tendsto (fun n => (Finset.range n).sum fun i => f i) Filter.atTop (nhds r)

This theorem states that for any sequence of non-negative real numbers `f`, the series formed by `f` converges to a real number `r` (in the sense of `HasSum`) if and only if the sequence of its partial sums tends to `r`. In other words, the cumulative sum of the elements of `f` up to the `n`th index, where `n` tends to infinity, converges to `r`. This is equivalent to saying that for every neighborhood of `r`, there exists a natural number `N` such that for all `n` greater than or equal to `N`, the `n`th partial sum of `f` is in that neighborhood of `r`.

More concisely: A real sequence `f` converges to a real number `r` in the sense of `HasSum` if and only if the sequence of its partial sums converges to `r`.

Real.diam_eq

theorem Real.diam_eq : ∀ {s : Set ℝ}, Bornology.IsBounded s → Metric.diam s = sSup s - sInf s

The theorem `Real.diam_eq` states that for any set `s` of real numbers that is bounded (according to the definition provided by `Bornology.IsBounded`), the diameter of `s` (as defined by `Metric.diam`) is equal to the difference between the least upper bound (`sSup s`) and the greatest lower bound (`sInf s`) of the set `s`. In other words, in a bounded set of real numbers, the 'width' of the set, or the greatest distance between any two points in the set, is equal to the difference between the supremum and infimum of the set.

More concisely: The diameter of a bounded set of real numbers equals the difference between its supremum and infimum.

EMetric.cauchySeq_iff_le_tendsto_0

theorem EMetric.cauchySeq_iff_le_tendsto_0 : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : Nonempty β] [inst_2 : SemilatticeSup β] {s : β → α}, CauchySeq s ↔ ∃ b, (∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N) ∧ Filter.Tendsto b Filter.atTop (nhds 0)

This theorem states that for a sequence `s` of elements in a pseudoemetric space `α` indexed by an ordered set `β`, the sequence is a Cauchy sequence if and only if there exists a function `b : β → α` such that for all `n`, `m` and `N` in `β` with `N ≤ n` and `N ≤ m`, the extended distance between `s n` and `s m` is less than or equal to `b N`, and the function `b` tends to 0 as its argument tends to infinity. In other words, the distance between any two sufficiently far along elements of a Cauchy sequence can be controlled by a function that approaches zero as its input grows without bound.

More concisely: A sequence in a pseudometric space is Cauchy if and only if there exists a function tending to 0, such that the extended distance between any two of its terms is less than or equal to the value of the function at their common index.

ENNReal.monotone_truncateToReal

theorem ENNReal.monotone_truncateToReal : ∀ {t : ENNReal}, t ≠ ⊤ → Monotone t.truncateToReal

The theorem `ENNReal.monotone_truncateToReal` states that for all instances of the extended nonnegative real numbers (`ENNReal`), if a given number `t` is not infinity (`∞`), then the function `truncateToReal` applied to `t` is monotone. In other words, if `a` and `b` are any two extended nonnegative real numbers such that `a` is less than or equal to `b`, then the `truncateToReal` operation applied to `a` is less than or equal to the `truncateToReal` operation applied to `b`, provided that `t` is not infinity. This theorem is a cornerstone in the theory of measures where extended nonnegative real numbers are relevant as the codomain of a measure.

More concisely: For all `ENNReal` instances `t` finite, `truncateToReal` is a monotone function on extended nonnegative real numbers: if `a ≤ b`, then `truncateToReal a ≤ truncateToReal b`.

ENNReal.tsum_mul_right

theorem ENNReal.tsum_mul_right : ∀ {α : Type u_1} {a : ENNReal} {f : α → ENNReal}, ∑' (i : α), f i * a = (∑' (i : α), f i) * a

This theorem states that for any type `α`, any extended nonnegative real number `a`, and any function `f` mapping `α` to extended nonnegative real numbers, the sum of the product of `f(i)` and `a` for all `i` in `α` is equal to the product of `a` and the sum of all `f(i)` for all `i` in `α`. In other words, this theorem expresses the property of distributivity of multiplication over infinite summation in the context of extended nonnegative real numbers. This can be written in mathematical notation as follows: $\sum_{i \in \alpha} f(i) \cdot a = (\sum_{i \in \alpha} f(i)) \cdot a$.

More concisely: For any type `α`, any extended nonnegative real number `a`, and any function `f` from `α` to extended nonnegative real numbers, the product of `a` and the sum of `f(i)` for all `i` in `α` is equal to the sum of the products `a` and `f(i)` for all `i` in `α` (distributivity of multiplication over infinite summation in extended nonnegative real numbers).

Mathlib.Topology.Instances.ENNReal._auxLemma.29

theorem Mathlib.Topology.Instances.ENNReal._auxLemma.29 : ∀ {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b₁ b₂ : β}, ((a₁, b₁) = (a₂, b₂)) = (a₁ = a₂ ∧ b₁ = b₂)

This theorem states that for any types `α` and `β`, and any elements `a₁`, `a₂` of type `α` and `b₁`, `b₂` of type `β`, the equality of the pairs `(a₁, b₁)` and `(a₂, b₂)` is equivalent to the conjunction of the equality of `a₁` and `a₂` and the equality of `b₁` and `b₂`. In simpler terms, two pairs are equal if and only if their corresponding elements are equal.

More concisely: For any types `α` and `β`, and any `a₁, a₂ : α` and `b₁, b₂ : β`, `(a₁, b₁) = (a₂, b₂)` if and only if `a₁ = a₂` and `b₁ = b₂`.

continuous_of_le_add_edist

theorem continuous_of_le_add_edist : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {f : α → ENNReal} (C : ENNReal), C ≠ ⊤ → (∀ (x y : α), f x ≤ f y + C * edist x y) → Continuous f

This theorem states that for any type 'α' that is a pseudo emetric space and a function 'f' that maps from 'α' to the extended nonnegative real numbers (ENNReal), if there exists a value 'C' in ENNReal where 'C' is not equal to infinity (∞) and for every pair (x, y) in 'α', the value of f at 'x' is less than or equal to the value of f at 'y' plus 'C' times the extended distance between 'x' and 'y', then the function 'f' is continuous. This is a condition of continuity of 'f' in terms of bounds involving the extended distance and some constant factor 'C'.

More concisely: If 'α' is a pseudo metric space, 'f' : 'α' -> ENNReal is a function with 'C' in ENNReal such that for all x, y in 'α', f(x) ≤ f(y) + C · d(x, y), then 'f' is continuous.

Summable.countable_support_ennreal

theorem Summable.countable_support_ennreal : ∀ {α : Type u_1} {f : α → ENNReal}, ∑' (i : α), f i ≠ ⊤ → (Function.support f).Countable

This theorem states that for any function `f` mapping from an arbitrary type `α` to the extended nonnegative real numbers (denoted `[0, ∞]`), if the infinite series sum of `f` over all `i` in `α` is not infinite (`⊤`), then the set of points where `f` is not zero (the support of `f`) is countable. In other words, only countably many values `i` in `α` result in `f(i)` being non-zero if the series sum of `f` is finite.

More concisely: If a function `f` from type `α` to `[0, ∞]` has a finite sum, then the support of `f` (i.e., the set of `i` in `α` such that `f(i) ≠ 0`) is countable.

ENNReal.nhds_zero_basis

theorem ENNReal.nhds_zero_basis : (nhds 0).HasBasis (fun a => 0 < a) fun a => Set.Iio a

The theorem `ENNReal.nhds_zero_basis` states that the neighborhood filter at zero for the extended nonnegative real numbers has a basis. This basis is made up of the sets which are left-infinite right-open intervals (denoted as `Set.Iio a` in Lean), for all `a` greater than zero. In other words, it affirms that the filter of neighborhoods around zero is generated by all the open intervals from negative infinity to a positive real number `a`.

More concisely: The neighborhood filter at zero in the extended nonnegative real numbers has a basis consisting of all left-infinite right-open intervals.

ENNReal.Tendsto.mul_const

theorem ENNReal.Tendsto.mul_const : ∀ {α : Type u_1} {f : Filter α} {m : α → ENNReal} {a b : ENNReal}, Filter.Tendsto m f (nhds a) → a ≠ 0 ∨ b ≠ ⊤ → Filter.Tendsto (fun x => m x * b) f (nhds (a * b))

This theorem is about the limit of a function with extended nonnegative real numbers as output. It states that for any type `α`, any filter `f` on `α`, any function `m` from `α` to the extended nonnegative real numbers, and any two extended nonnegative real numbers `a` and `b`, if the function `m` tends to `a` under the filter `f` (i.e., for every neighborhood of `a`, the preimage under `m` is a neighborhood under `f`), and if either `a` is not zero or `b` is not infinite, then the function that maps every `x` in `α` to the product of `m(x)` and `b` also tends to the product of `a` and `b` under the filter `f`. In simpler terms, under certain conditions, the limit of the product of a function and a constant is the product of the limit of the function and the constant.

More concisely: If a function from a type `α` to extended nonnegative real numbers tends to limit `a` under filter `f`, and either `a` is nonzero or the limit of the function is finite (i.e., not infinite), then the function that maps every `x` in `α` to the product of `m(x)` and a constant `b` tends to the product of `a` and `b` under filter `f`.

ENNReal.tsum_coe_eq

theorem ENNReal.tsum_coe_eq : ∀ {α : Type u_1} {r : NNReal} {f : α → NNReal}, HasSum f r → ∑' (a : α), ↑(f a) = ↑r := by sorry

The theorem `ENNReal.tsum_coe_eq` states that for any type `α`, any nonnegative real number `r`, and any function `f` from `α` to nonnegative real numbers, if the series of `f` has a sum equal to `r`, then the infinite sum (denoted by `∑'`) of the co-domain values of `f` (obtained by applying the function to each element of the original domain `α`), when each is coerced (or casted) into an extended nonnegative real number (`↑(f a)`), is equal to `r` casted into an extended nonnegative real number (`↑r`). In other words, the summation of the function values remains the same even when the values are interpreted as extended nonnegative real numbers.

More concisely: For any type α, nonnegative real number r, and function f from α to nonnegative real numbers with the sum of f equal to r, the sum of the coerced values of f (denoted by ∑↑(fa)) equals the coerced sum of r (denoted by ↑r).

ENNReal.tsum_eq_iSup_nat

theorem ENNReal.tsum_eq_iSup_nat : ∀ {f : ℕ → ENNReal}, ∑' (i : ℕ), f i = ⨆ i, (Finset.range i).sum fun a => f a := by sorry

This theorem states that for any given function `f` which maps natural numbers to the extended nonnegative real numbers (`ENNReal`), the infinite sum (or series) of `f(i)` over all natural numbers `i` is equal to the least upper bound (or supremum, denoted by `⨆`) of the finite sums of `f(a)` over the range set `{0, 1, 2, ..., i-1}` for each `i`. In other words, the value of an infinite sum in the extended nonnegative reals can be found by considering the supremum of the values of the finite sums over all natural number ranges.

More concisely: For any function `f` mapping natural numbers to extended nonnegative reals, the infinite series $\sum\_{i=0}^{\infty} f(i)$ equals the supremum of the finite sums $\sum\_{j=0}^{i-1} f(j)$ over all natural numbers `i`.

Mathlib.Topology.Instances.ENNReal._auxLemma.4

theorem Mathlib.Topology.Instances.ENNReal._auxLemma.4 : ∀ {α : Type u} {β : Type v} {f : α → β} {l : Filter α} {s : Set β}, Filter.Tendsto f l (Filter.principal s) = ∀ᶠ (a : α) in l, f a ∈ s

This theorem states that for any given types `α` and `β`, a function `f` from `α` to `β`, a filter `l` on `α`, and a set `s` of `β`, the property `Filter.Tendsto f l (Filter.principal s)` holds if and only if almost every `a` in the filter `l` satisfies `f a ∈ s`. In other words, the function `f` tends to the principal filter of `s` with respect to the filter `l` if and only if, for almost every element in the filter `l`, its image under `f` belongs to `s`.

More concisely: For types `α` and `β`, a function `f: α → β`, filter `l` on `α`, and set `s ⊆ β`, the function `f` tends to the principal filter of `s` with respect to `l` if and only if almost every element in `l` maps to an element in `s` under `f`.

Continuous.edist

theorem Continuous.edist : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : TopologicalSpace β] {f g : β → α}, Continuous f → Continuous g → Continuous fun b => edist (f b) (g b)

This theorem states that for any two functions `f` and `g` from a topological space `β` to a pseudo-emetric space `α`, if both `f` and `g` are continuous, then the function that maps each point `b` in `β` to the extended distance (edist) between `f(b)` and `g(b)` in `α` is also continuous. In other words, the continuousness of `f` and `g` ensures the continuousness of the function that calculates the distances between their corresponding outputs.

More concisely: If `f` and `g` are continuous functions from a topological space `β` to a pseudo-metric space `α`, then the function mapping each `b` in `β` to the extended distance between `f(b)` and `g(b)` is also continuous.

edist_le_tsum_of_edist_le_of_tendsto₀

theorem edist_le_tsum_of_edist_le_of_tendsto₀ : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {f : ℕ → α} (d : ℕ → ENNReal), (∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n) → ∀ {a : α}, Filter.Tendsto f Filter.atTop (nhds a) → edist (f 0) a ≤ ∑' (m : ℕ), d m

The theorem `edist_le_tsum_of_edist_le_of_tendsto₀` states that for any type `α` equipped with a pseudo-emetric space structure, given a sequence of elements of `α` denoted by `f : ℕ → α` and a function `d : ℕ → ENNReal` (extended nonnegative real numbers), if the extended distance between consecutive terms of the sequence `f` are bounded above by the values of the function `d` (i.e., `∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n`), then for any limit point `a` of the sequence `f` (i.e., `Filter.Tendsto f Filter.atTop (nhds a)`), the extended distance between the initial term of the sequence (`f 0`) and the limit point `a` is bounded by the sum of the sequence given by `d` (i.e., `edist (f 0) a ≤ ∑' (m : ℕ), d m`). This sum is possibly infinite since `d` takes values in the extended nonnegative real numbers.

More concisely: For any sequence `f : ℕ → α` in a pseudo-metric space, if the extended distance between consecutive terms is bounded above by the values of a function `d : ℕ → ENNReal`, then the extended distance from the first term `f 0` to any limit point `a` of the sequence is less than or equal to the sum of the function `d`.

ENNReal.hasSum_coe

theorem ENNReal.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 `α`, any function `f` that maps from `α` to nonnegative real numbers (`NNReal`), and any nonnegative real number `r`, the property of `f` having a sum equal to `r` (denoted by `HasSum f r`) is equivalent to the property that the function obtained by applying the embedding from `NNReal` to `Real` to `f` has a sum equal to the embedding of `r` (denoted by `HasSum (fun a => ↑(f a)) ↑r`). In other words, summing the function values in the real number domain is the same as summing the function values in the nonnegative real number domain and then embedding the sum into the real number domain.

More concisely: For any function `f: α → NNReal` and real number `r`, the property `HasSum f r` is equivalent to `HasSum (fun a => ↑(f a)) ↑r`.

ENNReal.tsum_add

theorem ENNReal.tsum_add : ∀ {α : Type u_1} {f g : α → ENNReal}, ∑' (a : α), (f a + g a) = ∑' (a : α), f a + ∑' (a : α), g a

The theorem `ENNReal.tsum_add` states that for any type `α` and any two functions `f` and `g` from `α` to the extended nonnegative real numbers (`ENNReal`), the sum over all `α` of the sums of `f(a)` and `g(a)` is equal to the sum of the sum over all `α` of `f(a)` and the sum over all `α` of `g(a)`. This principle is essentially the distributive law of addition over summation, asserting that the sum of two series is equal to the series of their sums, where the series and the sums are in the extended nonnegative real numbers.

More concisely: For any type `α` and functions `f` and `g` from `α` to the extended nonnegative real numbers (`ENNReal`), the sum of the pointwise sum of `f` and `g` over all `α` is equal to the sum of the sums of `f` and `g` over all `α`.

ENNReal.tsum_eq_top_of_eq_top

theorem ENNReal.tsum_eq_top_of_eq_top : ∀ {α : Type u_1} {f : α → ENNReal}, (∃ a, f a = ⊤) → ∑' (a : α), f a = ⊤ := by sorry

The theorem `ENNReal.tsum_eq_top_of_eq_top` states that for any type `α` and any function `f` from `α` to the extended nonnegative real numbers (`ENNReal`), if there exists an element `a` in `α` such that `f(a)` equals infinity (`⊤`), then the sum over all elements of `α` under function `f` also equals infinity (`⊤`). That is, it's saying if any value of the function is infinity, then the total sum is also infinity.

More concisely: If a function from a type `α` to the extended nonnegative real numbers `ENNReal` has an element `α` mapping to infinity (`⊤`), then the sum of the function over all elements in `α` is also infinity (`⊤`).

Real.ediam_eq

theorem Real.ediam_eq : ∀ {s : Set ℝ}, Bornology.IsBounded s → EMetric.diam s = ENNReal.ofReal (sSup s - sInf s) := by sorry

This theorem states that for any set of real numbers `s` that is bounded (as specified by the condition `Bornology.IsBounded s`), the diameter of the set `s` (given by `EMetric.diam s`) is equal to the supremum of the set `s` (`sSup s`) minus its infimum (`sInf s`). This difference is then converted to the type `ℝ≥0∞` (non-negative extended real numbers) using the function `ENNReal.ofReal`. The diameter of a set in this context refers to the greatest distance between any two points in the set, and `sSup` and `sInf` represent the least upper bound and the greatest lower bound of the set, respectively.

More concisely: For any bounded set of real numbers `s`, the diameter is equal to the supremum minus the infimum, or equivalently, the difference between the supremum and infimum of `s` in the extended real numbers.

ENNReal.ne_top_of_tsum_ne_top

theorem ENNReal.ne_top_of_tsum_ne_top : ∀ {α : Type u_1} {f : α → ENNReal}, ∑' (a : α), f a ≠ ⊤ → ∀ (a : α), f a ≠ ⊤

The theorem `ENNReal.ne_top_of_tsum_ne_top` states that for any type `α` and any function `f` from `α` to the extended nonnegative real numbers (denoted as `ENNReal`), if the infinite sum (also known as series) of `f(a)` for all `a` from `α` is not equal to positive infinity (`⊤`), then `f(a)` is not equal to positive infinity for all `a` in `α`. In other words, if the series of values of a function doesn't reach infinity, then the function itself doesn't reach infinity for any of its inputs.

More concisely: If the series of a function from a type to the extended nonnegative real numbers is finite, then the function is bounded.

ENNReal.tsum_coe_ne_top_iff_summable

theorem ENNReal.tsum_coe_ne_top_iff_summable : ∀ {β : Type u_2} {f : β → NNReal}, ∑' (b : β), ↑(f b) ≠ ⊤ ↔ Summable f

This theorem, `ENNReal.tsum_coe_ne_top_iff_summable`, states that for all types `β` and all functions `f` from `β` to nonnegative real numbers (`NNReal`), the infinite sum of the values of `f` (the sum of the real number representations of `f(b)` for all `b` in `β`) is not equal to positive infinity if and only if `f` is summable. Here, a function `f` is said to be summable if there exists some value such that `f` has a convergent infinite sum to that value.

More concisely: A function from a type to nonnegative real numbers has a finite sum if and only if it is summable.

continuous_edist

theorem continuous_edist : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α], Continuous fun p => edist p.1 p.2

This theorem states that for any type `α` which has a structure of a pseudo emetric space (a generalization of the concept of a metric space, where the distance between two points can possibly be infinite), the function which calculates the extended distance (`edist`) between a pair of points in `α` is a continuous function. Continuity here means that small changes in the input points result in small changes in their distance.

More concisely: For any pseudo metric space `α`, the extended distance function `edist` is a continuous function.

ENNReal.Tendsto.mul

theorem ENNReal.Tendsto.mul : ∀ {α : Type u_1} {f : Filter α} {ma mb : α → ENNReal} {a b : ENNReal}, Filter.Tendsto ma f (nhds a) → a ≠ 0 ∨ b ≠ ⊤ → Filter.Tendsto mb f (nhds b) → b ≠ 0 ∨ a ≠ ⊤ → Filter.Tendsto (fun a => ma a * mb a) f (nhds (a * b))

This theorem states that for a certain type `α`, a given filter `f` on `α`, two functions `ma` and `mb` from `α` to the extended nonnegative real numbers (`ENNReal`), and two extended nonnegative real numbers `a` and `b`, if `ma` tends towards `a` with respect to the filter `f` and either `a` is not zero or `b` is not infinity, and if `mb` tends towards `b` with respect to the filter `f` and either `b` is not zero or `a` is not infinity, then the function defined by the product of `ma` and `mb` also tends towards the product of `a` and `b` with respect to the filter `f`. This is a result about the limit behavior of a product of functions in the context of extended nonnegative real numbers and general topological spaces.

More concisely: If functions `ma : α -> ENNReal` and `mb : α -> ENNReal` tend to `a, b ∈ ENNReal` (not zero if one is infinity) with respect to filter `f` on `α`, then their product `ma * mb` tends to `a * b` with respect to filter `f`.

ENNReal.tendsto_toNNReal

theorem ENNReal.tendsto_toNNReal : ∀ {a : ENNReal}, a ≠ ⊤ → Filter.Tendsto ENNReal.toNNReal (nhds a) (nhds a.toNNReal)

This theorem, `ENNReal.tendsto_toNNReal`, states that for all extended nonnegative real numbers `a` that are not infinity, the function `ENNReal.toNNReal`, which takes an extended nonnegative real number and returns a nonnegative real number (or 0 if `a` is not a real number), has a limit at `a`. More specifically, for every neighborhood of `a.toNNReal`, the preimage under `ENNReal.toNNReal` of this neighborhood is a neighborhood of `a`. In other words, `ENNReal.toNNReal` is continuous at `a` in the topology of the extended nonnegative real numbers.

More concisely: The function `ENNReal.toNNReal` from extended nonnegative real numbers to nonnegative real numbers is continuous at every finite extended nonnegative real number.

NNReal.tsum_eq_toNNReal_tsum

theorem NNReal.tsum_eq_toNNReal_tsum : ∀ {β : Type u_2} {f : β → NNReal}, ∑' (b : β), f b = (∑' (b : β), ↑(f b)).toNNReal

The theorem `NNReal.tsum_eq_toNNReal_tsum` states that for any type `β` and function `f` from `β` to the nonnegative real numbers (NNReal), the sum of the series generated by applying `f` to elements of `β` is equal to the sum of the series generated by applying the function which first applies `f` and then the embedding of NNReal in the reals to elements of `β`, where the sums are interpreted as nonnegative real numbers. In short, summing first and then embedding into the reals gives the same result as embedding into the reals first and then summing.

More concisely: For any type `β` and function `f` from `β` to the nonnegative real numbers, the series sum of applying `f` to elements of `β` equals the series sum of applying `f` and the NNReal embedding function to elements of `β`, where the series sums are interpreted as nonnegative real numbers.

ENNReal.coe_tsum

theorem ENNReal.coe_tsum : ∀ {α : Type u_1} {f : α → NNReal}, Summable f → ↑(tsum f) = ∑' (a : α), ↑(f a)

The theorem `ENNReal.coe_tsum` states that for any type `α` and function `f` from `α` to nonnegative real numbers (`NNReal`), if `f` is summable, then the coercive function (denoted as `↑`) applied to the total sum (`tsum`) of `f` is equal to the infinite sum (`∑' (a : α), ↑(f a)`) of the coercive function applied to each `f(a)`. In simpler terms, it states that the sum of the coerced values of the sequence is the same as the coerced value of the sum of the sequence, given that the series represented by the sequence is summable.

More concisely: For any summable function `f` from type `α` to nonnegative reals, `↑(tsum (map ↑ f) : NNReal) = ∑' (a : α), ↑(f a)`.

ENNReal.tendsto_nat_nhds_top

theorem ENNReal.tendsto_nat_nhds_top : Filter.Tendsto (fun n => ↑n) Filter.atTop (nhds ⊤)

This theorem states that the sequence of natural numbers, when converted to extended non-negative real numbers (that's what `↑n` means), tends to infinity (`nhds ⊤`). More formally, for every neighborhood `U` of infinity in the extended non-negative real numbers, there exists a natural number `N` such that for all natural numbers `n` greater than `N`, `n` is an element of `U`. The function `Filter.Tendsto` is used to express this concept of limit in Lean 4. This theorem is usually used when dealing with sequences or functions that grow without bounds in the context of extended real numbers.

More concisely: Given any neighborhood U of infinity in the extended non-negative real numbers, there exists a natural number N such that all natural numbers greater than N lie in U. (In Lean 4, this is expressed using the `Filter.Tendsto` function.)

ENNReal.continuousOn_sub

theorem ENNReal.continuousOn_sub : ContinuousOn (fun p => p.1 - p.2) {p | p ≠ (⊤, ⊤)}

This theorem states that the function defined as the subtraction of the pair of elements `(p.1 - p.2)` is continuous on a set of pairs `p`, excluding the pair `(⊤, ⊤)`. Here, the continuity is defined in the topological sense, meaning that the function satisfies the condition of being continuous at every point within this subset. In other words, for all pairs `p` except `(⊤, ⊤)`, the difference between the two elements of the pair changes continuously as you move around in this set.

More concisely: The function subtracting the first component from the second component of a pair is continuous on the set of pairs excluding `(⊤, ⊤)`.

ENNReal.tsum_eq_iSup_sum

theorem ENNReal.tsum_eq_iSup_sum : ∀ {α : Type u_1} {f : α → ENNReal}, ∑' (a : α), f a = ⨆ s, s.sum fun a => f a := by sorry

This theorem states that for any function `f` mapping from an arbitrary type `α` to the extended nonnegative real numbers (represented by `ENNReal`), the sum over all elements of type `α` (notated as `∑' (a : α), f a`) is equal to the supremum (notated as `⨆ s`) of the sum over a finite set `s` of elements of type `α` (notated as `Finset.sum s fun a => f a`). In simpler terms, it says that the total sum of the function `f` applied to all elements of a type is the greatest possible sum we can get by applying `f` to any finite subset of that type.

More concisely: For any function from a type to extended nonnegative real numbers, the sum over the entire type equals the supremum of the sums over finite subsets.

ENNReal.finset_card_const_le_le_of_tsum_le

theorem ENNReal.finset_card_const_le_le_of_tsum_le : ∀ {ι : Type u_4} {a : ι → ENNReal} {c : ENNReal}, c ≠ ⊤ → ∑' (i : ι), a i ≤ c → ∀ {ε : ENNReal}, ε ≠ 0 → ∃ (hf : {i | ε ≤ a i}.Finite), ↑hf.toFinset.card ≤ c / ε

This theorem, called Markov's Inequality for `Finset.card` and `tsum` in `ℝ≥0∞`, states that for any type `ι` and a function `a` from `ι` to the extended nonnegative real numbers `ENNReal`, and any `c` in `ENNReal` not equal to infinity, if the sum over all `i` in `ι` of `a i` is less than or equal to `c`, then for any `ε` in `ENNReal` not equal to zero, there exists a finite set `hf` of `i` where `ε ≤ a i` such that the cardinality of `hf` as a finite set, when converted to the extended nonnegative real numbers, is less than or equal to `c / ε`. In other words, it is a version of Markov's inequality that relates the size of a subset of elements whose associated values exceed a given threshold, to the total sum of the associated values and the threshold.

More concisely: For any function `a` from a type `ι` to the extended nonnegative real numbers `ENNReal`, and `c` in `ENNReal` not equal to infinity, if the sum of `a i` over all `i` in `ι` is less than or equal to `c`, then there exists a finite subset `hf` of `ι` such that the cardinality of `hf` as a real number is less than or equal to `c / sup i. a i`, where the supremum is taken over all `i` in `ι`.

ENNReal.continuous_sub_left

theorem ENNReal.continuous_sub_left : ∀ {a : ENNReal}, a ≠ ⊤ → Continuous fun x => a - x

This theorem states that for every extended nonnegative real number `a` that is not equal to infinity, the operation of subtracting another extended nonnegative real number `x` from `a` is a continuous function. In the context of topology, a function is continuous if the preimage of every open set is open. Here, the subtraction operation is viewed as a function that maps from the set of all extended nonnegative real numbers to itself.

More concisely: For every extended nonnegative real number `a` not equal to infinity, the function `x => a - x` from extended nonnegative real numbers to itself is continuous.

ENNReal.tsum_eq_zero

theorem ENNReal.tsum_eq_zero : ∀ {α : Type u_1} {f : α → ENNReal}, ∑' (i : α), f i = 0 ↔ ∀ (i : α), f i = 0

This theorem states that for any type `α` and a function `f` from `α` to the extended nonnegative real numbers (usually denoted as `[0, ∞]`), the sum of the sequence `f` equals zero if and only if every element in the sequence `f` equals zero. In mathematical terms, it says that `∑' (i : α), f i = 0` if and only if `∀ (i : α), f i = 0`.

More concisely: For any function `f` from type `α` to the extended nonnegative real numbers, the sum of `f` equals zero if and only if every element in `f` is zero.

Mathlib.Topology.Instances.ENNReal._auxLemma.3

theorem Mathlib.Topology.Instances.ENNReal._auxLemma.3 : ∀ {α : Type u} {β : Type v} {ι : Sort x} {f : α → β} {x : Filter α} {y : ι → Filter β}, Filter.Tendsto f x (⨅ i, y i) = ∀ (i : ι), Filter.Tendsto f x (y i)

This theorem states that for all types `α`, `β`, and `ι`, and for all function `f` from `α` to `β`, filter `x` on `α` and a collection of filters `y` indexed by `ι` on `β`, the function `f` tending towards the infimum of the filters `y` (denoted `⨅ i, y i`) from the filter `x` is equivalent to the function `f` tending towards each filter `y i` from the filter `x` for all `i` in `ι`. In other words, in terms of limit, it states that the limit of the function `f` as `x` approaches the limit of the `y` filters is the same as the limit of the function `f` as `x` approaches each individual `y` filter.

More concisely: For all types `α`, `β`, and index type `ι`, and for all functions `f` from `α` to `β`, if `x` tends to the infimum of filters `y_i` on `β` as `i` ranges over `ι` from filter `x` on `α`, then `f(x)` tends to the limit of `f(y_i)` for all `i` in `ι`.

Mathlib.Topology.Instances.ENNReal._auxLemma.32

theorem Mathlib.Topology.Instances.ENNReal._auxLemma.32 : ∀ {α : Sort u_1} {p : α → Prop}, (¬∃ x, p x) = ∀ (x : α), ¬p x

This theorem states that for any type `α` and any predicate `p` over `α`, the statement that there does not exist an `x` of type `α` such that `p(x)` holds is equivalent to the statement that for all `x` of type `α`, `p(x)` does not hold. This is a generalization of the principle of negation in classical logic, translating the non-existence of an element satisfying a property into the universal non-satisfaction of that property.

More concisely: For any type `α` and predicate `p` over `α`, the lack of existence of an `x` with `p(x)` is equivalent to `p` being universally false for all `x` of type `α`.

ENNReal.tsum_eq_iSup_nat'

theorem ENNReal.tsum_eq_iSup_nat' : ∀ {f : ℕ → ENNReal} {N : ℕ → ℕ}, Filter.Tendsto N Filter.atTop Filter.atTop → ∑' (i : ℕ), f i = ⨆ i, (Finset.range (N i)).sum fun a => f a

This theorem states that for any sequence of extended nonnegative real numbers `f` and a sequence of natural numbers `N` that tends to infinity, the series sum of `f` is equal to the least upper bound of the finite sums of `f` over the range of `N`. In other words, given a function `f` from natural numbers to extended nonnegative real numbers and another function `N` from natural numbers to natural numbers that tends to infinity, the sum over all natural numbers of `f` equals the supremum over all natural numbers of the sum of `f` over the set of natural numbers less than the value of `N` at that number.

More concisely: For any sequence `(f : ℕ → ℝᵤᵇ)` of extended nonnegative real-valued functions and `(N : ℕ → ℕ)` tending to infinity, $\sum\_{n=0}^\infty f(n) = \sup\_{n\in\mathbb{N}} \sum\_{i=0}^{N(n)-1} f(i).$

ENNReal.continuous_ofReal

theorem ENNReal.continuous_ofReal : Continuous ENNReal.ofReal

This theorem states that the function `ENNReal.ofReal`, which maps a real number to its nonnegative counterpart (or zero if it's negative), is continuous. In mathematical terms, it implies that for any sequence of real numbers that converges to a limit, their corresponding sequence in the extended nonnegative real number system (obtained through `ENNReal.ofReal`) also converges, and its limit is `ENNReal.ofReal` of the original limit.

More concisely: The function `ENNReal.ofReal` from real numbers to nonnegative extended real numbers is continuous, meaning that any convergent sequence of real numbers maps to a convergent sequence of nonnegative extended real numbers with the same limit.

ENNReal.hasBasis_nhds_of_ne_top'

theorem ENNReal.hasBasis_nhds_of_ne_top' : ∀ {x : ENNReal}, x ≠ ⊤ → (nhds x).HasBasis (fun x => x ≠ 0) fun ε => Set.Icc (x - ε) (x + ε)

The theorem `ENNReal.hasBasis_nhds_of_ne_top'` states that for any extended nonnegative real number `x` that is not infinity, the neighborhood filter at `x` (denoted by `nhds x`) has a basis consisting of closed intervals `Set.Icc (x - ε) (x + ε)` for each `ε ≠ 0`. In other words, every neighborhood of `x` contains such an interval, and for every such interval, there exists a neighborhood of `x` contained in it. The use of `Set.Icc`, the set of all elements `x` such that `a ≤ x ≤ b`, instead of `Set.Ioo`, is specifically because it allows the statement to hold even for `x = 0`.

More concisely: For every extended non-negative real number `x` not equal to infinity, the neighborhood filter of `x` has a basis consisting of closed intervals `Icc (x - ε, x + ε)` for all `ε ≠ 0`.

ENNReal.iSup_add

theorem ENNReal.iSup_add : ∀ {a : ENNReal} {ι : Sort u_4} {s : ι → ENNReal} [inst : Nonempty ι], iSup s + a = ⨆ b, s b + a

The theorem `ENNReal.iSup_add` states that for any extended non-negative real number `a` and for any function `s` from an arbitrary index set `ι` to the set of extended non-negative real numbers, given that the index set `ι` is non-empty, the supremum (iSup) of `s` added to `a` equals the supremum over all `b` in the index set of the sum of `s b` and `a`. In other words, this theorem states the property that adding a fixed extended non-negative real number to the supremum of a set of extended non-negative real numbers is the same as taking the supremum of the set obtained by adding the fixed number to each element of the original set.

More concisely: For any non-empty index set `ι` and extended non-negative real number `a`, the supremum of the function `s : ι → ℝ����fu` is equal to the supremum of `a + s(x)` over all `x` in `ι`.

ENNReal.continuousOn_toNNReal

theorem ENNReal.continuousOn_toNNReal : ContinuousOn ENNReal.toNNReal {a | a ≠ ⊤}

The theorem `ENNReal.continuousOn_toNNReal` states that the function `toNNReal`, which maps an extended non-negative real number to a non-negative real number (returning the number itself if it is real, and 0 if it is not), is continuous on the set of all extended non-negative real numbers that are not equal to positive infinity. In other words, `toNNReal` has the property that for every point in this set, the function `toNNReal` is continuous at that point within the set. This essentially means that `toNNReal` does not exhibit any abrupt changes in value within this set.

More concisely: The extended non-negative real function `toNNReal` is continuous on the set of all extended non-negative real numbers that are finite.

NNReal.tendsto_sum_nat_add

theorem NNReal.tendsto_sum_nat_add : ∀ (f : ℕ → NNReal), Filter.Tendsto (fun i => ∑' (k : ℕ), f (k + i)) Filter.atTop (nhds 0)

The theorem `NNReal.tendsto_sum_nat_add` states that for a function `f` mapping from natural numbers to nonnegative real numbers, the shifted sum `∑' k, f (k + i)` tends to zero as `i` goes to infinity. Here, the sum is a formal sum over all natural numbers `k`, with the `i`th term is `f(k + i)`. No assumptions are made regarding the summability of `f`, as the theorem holds true even if the sum of all terms of `f` is zero. In other words, the average of the terms of the series `f` decreases to zero when the series is shifted towards the right, regardless of the overall sum of the series.

More concisely: For any function `f` mapping natural numbers to non-negative reals, the shifted sum `∑' k, f (k + i)` converges to zero as `i` approaches infinity.

NNReal.exists_le_hasSum_of_le

theorem NNReal.exists_le_hasSum_of_le : ∀ {β : Type u_2} {f g : β → NNReal} {r : NNReal}, (∀ (b : β), g b ≤ f b) → HasSum f r → ∃ p ≤ r, HasSum g p := by sorry

This theorem states that for any type 'β', given two functions `f` and `g` from 'β' to the set of nonnegative real numbers (denoted as `NNReal`), and a nonnegative real number `r`, if for all `b` in 'β', `g(b)` is less than or equal to `f(b)`, and the series formed by `f(b)` has a sum `r`, then there exists a nonnegative real number `p` less than or equal to `r` such that the series formed by `g(b)` has a sum `p`. This is known as the comparison test of convergence for series with nonnegative real number terms.

More concisely: If `f` and `g` are functions from type `β` to `NNReal` with `g ≤ f`, and the series `Σ(b:β) f(b)` converges to `r`, then there exists `p ≤ r` such that the series `Σ(b:β) g(b)` converges to `p`.

edist_le_tsum_of_edist_le_of_tendsto

theorem edist_le_tsum_of_edist_le_of_tendsto : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {f : ℕ → α} (d : ℕ → ENNReal), (∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n) → ∀ {a : α}, Filter.Tendsto f Filter.atTop (nhds a) → ∀ (n : ℕ), edist (f n) a ≤ ∑' (m : ℕ), d (n + m)

The theorem states that if the extended distance (including infinite distances) between successive applications of a function `f : ℕ → α` on natural numbers is bounded above by another function `d : ℕ → ENNReal`, where `α` is a type with a pseudo-emetric space structure, then the extended distance from `f n` to the limit of `f` as `n` goes to infinity is bounded by the series sum of `d` starting from `n`. This limit is described by the predicate `Filter.Tendsto f Filter.atTop (nhds a)`, meaning that `f` tends towards `a` as `n` goes to infinity. In other words, for any point in the sequence generated by `f`, the distance to the limit point `a` is at most the sum of the remaining terms in the bounding function `d`.

More concisely: If the sequence `(f (n+1) - f n)` is bounded above by a function `d`, then the distance between `f n` and the limit of `f` is at most the sum of `d` from `n` to infinity.

ENNReal.finite_const_le_of_tsum_ne_top

theorem ENNReal.finite_const_le_of_tsum_ne_top : ∀ {ι : Type u_4} {a : ι → ENNReal}, ∑' (i : ι), a i ≠ ⊤ → ∀ {ε : ENNReal}, ε ≠ 0 → {i | ε ≤ a i}.Finite

This theorem states that for any series (a sum of an infinite sequence) of extended nonnegative real numbers, if the sum of the series is not infinite (denoted as `⊤`), then for any positive threshold `ε`, there can only be a finite number of terms in the series that are greater than or equal to this threshold `ε`. Here, "extended nonnegative real numbers" refers to the set of all nonnegative real numbers along with positive infinity. This theorem basically captures the intuitive idea that if a series of nonnegative numbers does not add up to infinity, you cannot have an infinite number of large terms in it.

More concisely: For any series of extended nonnegative real numbers that does not converge to infinity, there exist finitely many terms greater than a given positive threshold.

Mathlib.Topology.Instances.ENNReal._auxLemma.70

theorem Mathlib.Topology.Instances.ENNReal._auxLemma.70 : ∀ {α : Type u} [inst : LinearOrder α] [inst_1 : OrderTop α] {a b : α}, (min a b = ⊤) = (a = ⊤ ∧ b = ⊤)

This theorem, `Mathlib.Topology.Instances.ENNReal._auxLemma.70`, states that for any type `α` that is endowed with a linear order and a top element, given any two elements `a` and `b` from `α`, the minimum of `a` and `b` being equal to the top element is equivalent to both `a` and `b` being equal to the top element. In other words, in such a setup, the only way for the minimum of `a` and `b` to be the top element is if both `a` and `b` themselves are the top element.

More concisely: For any type endowed with a linear order and a top element, the minimum of two elements is the top element if and only if both elements are the top element.

ENNReal.openEmbedding_coe

theorem ENNReal.openEmbedding_coe : OpenEmbedding ENNReal.ofNNReal

This theorem states that the function `ENNReal.ofNNReal`, which maps from the set of non-negative real numbers (`NNReal`) to the extended non-negative real numbers (`ENNReal`), is an open embedding. In topology, an open embedding is a function between topological spaces which is both an embedding (injective and homeomorphic to its image) and open (the image of an open set is open). Therefore, the 'openness' property of this function ensures that it preserves the topology, i.e., the open set structures of `NNReal` and `ENNReal`.

More concisely: The function `ENNReal.ofNNReal` is an open embedding from the non-negative real numbers to the extended non-negative real numbers.

ENNReal.tsum_mul_left

theorem ENNReal.tsum_mul_left : ∀ {α : Type u_1} {a : ENNReal} {f : α → ENNReal}, ∑' (i : α), a * f i = a * ∑' (i : α), f i

This theorem states that for any type `α`, any extended nonnegative real number `a`, and any function `f` mapping `α` to extended nonnegative real numbers, the sum of the products of `a` and `f i` for all `i` in `α` is equal to the product of `a` and the sum of `f i` for all `i` in `α`. In simple mathematical terms, it expresses the property of distributivity of multiplication over infinite summation in the domain of extended nonnegative real numbers. This is similar to saying $\sum_{i \in \alpha} (a * f(i)) = a * \sum_{i \in \alpha} f(i)$.

More concisely: For any type `α`, any extended nonnegative real number `a`, and any function `f` from `α` to extended nonnegative real numbers, the sum of the products `a * f i` over all `i` in `α` equals the product of `a` and the sum of `f i` over all `i` in `α`. In symbols, $\sum\_{i \in \alpha} a \cdot f(i) = a \cdot \sum\_{i \in \alpha} f(i)$.

ENNReal.limsup_toReal_eq

theorem ENNReal.limsup_toReal_eq : ∀ {ι : Type u_5} {F : Filter ι} [inst : F.NeBot] {b : ENNReal}, b ≠ ⊤ → ∀ {xs : ι → ENNReal}, (∀ᶠ (i : ι) in F, xs i ≤ b) → Filter.limsup (fun i => (xs i).toReal) F = (Filter.limsup xs F).toReal

The theorem `ENNReal.limsup_toReal_eq` states that for any type `ι`, any filter `F` on `ι` that is not the bottom filter, any extended nonnegative real number `b` that is not infinity, and any function `xs` from `ι` to the extended nonnegative real numbers which is bounded by `b` (almost everywhere with respect to the filter `F`), the limit superior of the real part of `xs` with respect to `F` equals the real part of the limit superior of `xs` with respect to `F`. In mathematical notation, this is expressed as, if `xs : ι → ℝ≥0∞` is bounded, then `limsup (toReal ∘ xs) = toReal (limsup xs)`.

More concisely: For any filter `F` on a type `ι`, if `xs : ι → ℝ≥0∞` is a bounded function and `b : ℝ≥0∞` is not infinity, then `limsup (toReal . xs) = toReal (limsup xs)`.

cauchySeq_of_edist_le_of_summable

theorem cauchySeq_of_edist_le_of_summable : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {f : ℕ → α} (d : ℕ → NNReal), (∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)) → Summable d → CauchySeq f

This theorem states that for a given sequence of elements in a pseudo-emetric space, if the extended distance between consecutive elements of this sequence is bounded by a summable series of nonnegative real numbers, then the original sequence is a Cauchy sequence. Here, a pseudo-emetric space is a set endowed with a metric-like function (the extended distance); a Cauchy sequence is a sequence where the distance between any two subsequent elements can be made arbitrarily small by going sufficiently far into the sequence; and a series is summable if the infinite series of its terms converges to a finite limit.

More concisely: In a pseudo-metric space, if the sequence of extended distances between consecutive elements is bounded by a summable series, then the sequence is a Cauchy sequence.

ENNReal.summable

theorem ENNReal.summable : ∀ {α : Type u_1} {f : α → ENNReal}, Summable f

The theorem states that for any type `α` and any function `f` from `α` to the extended nonnegative real numbers `ENNReal`, the function `f` is summable. This means there exists some (possibly infinite) sum of the series generated by `f`. The type `ENNReal` represents the set of nonnegative real numbers including infinity, used typically as the codomain of a measure.

More concisely: For any type `α` and function `f` from `α` to the extended nonnegative real numbers `ENNReal`, there exists a sum of the series generated by `f`.

Real.ediam_Icc

theorem Real.ediam_Icc : ∀ (a b : ℝ), EMetric.diam (Set.Icc a b) = ENNReal.ofReal (b - a)

This theorem, named `Real.ediam_Icc`, states that for any two real numbers `a` and `b`, the diameter of the set that is the left-closed right-closed interval from `a` to `b` is equal to the non-negative part of the difference `b - a`. In other words, in a set of real numbers where the set is an interval that includes both ends (`a` and `b`), the "distance" between the furthest apart elements in the set (which is the diameter) is exactly the non-negative difference between `b` and `a`. This distance is zero if `b - a` is negative and `b - a` otherwise.

More concisely: The diameter of the interval [a, b] equals |b - a|.

Summable.of_nonneg_of_le

theorem Summable.of_nonneg_of_le : ∀ {β : Type u_2} {f g : β → ℝ}, (∀ (b : β), 0 ≤ g b) → (∀ (b : β), g b ≤ f b) → Summable f → Summable g

This is the comparison test for the convergence of series of non-negative real numbers. Given two functions `f` and `g` from an arbitrary type `β` to the real numbers, if for all `b` in `β`, the value of `g b` is non-negative and less than or equal to `f b`, and if the sum of the series formed by `f` exists (i.e., `f` is summable), then the sum of the series formed by `g` also exists (`g` is also summable).

More concisely: If `f(x)` is a summable series of non-negative real numbers and `g(x) ≤ f(x)` for all `x`, then `g(x)` is also summable.

ENNReal.nhds_coe_coe

theorem ENNReal.nhds_coe_coe : ∀ {r p : NNReal}, nhds (↑r, ↑p) = Filter.map (fun p => (↑p.1, ↑p.2)) (nhds (r, p)) := by sorry

This theorem, `ENNReal.nhds_coe_coe`, states that for any two nonnegative real numbers `r` and `p`, the neighborhood filter of the pair `(↑r, ↑p)` (where `↑r` and `↑p` denote the embeddings of `r` and `p` into the real numbers) is equal to the forward map, under the function that maps a pair to its embeddings into the real numbers, of the neighborhood filter of the pair `(r, p)`. In other words, the local topological structure at `(↑r, ↑p)` in the real numbers is exactly the same as the local topological structure at `(r, p)` in the nonnegative real numbers, when the latter is viewed as a subspace of the real numbers.

More concisely: The neighborhood filters of `(r, p)` in the nonnegative real numbers and of `(↑r, ↑p)` in the real numbers are equal.

Real.ediam_Ioo

theorem Real.ediam_Ioo : ∀ (a b : ℝ), EMetric.diam (Set.Ioo a b) = ENNReal.ofReal (b - a)

The theorem `Real.ediam_Ioo` states that for any two real numbers `a` and `b`, the diameter of the set of real numbers which is strictly greater than `a` and strictly less than `b` (known as a left-open right-open interval, or `Set.Ioo a b` in Lean) is equal to the nonnegative part of the difference `b - a`. In mathematical terms, we can interpret this theorem as saying that the "diameter" of the interval $(a, b)$ in the real numbers is simply the length of that interval, i.e., $b - a$ if $b > a$, and $0$ otherwise.

More concisely: The theorem `Real.ediam_Ioo` asserts that the diameter of the real interval `(a, b)` is equal to `abs (b - a)`.

ENNReal.tendsto_tsum_compl_atTop_zero

theorem ENNReal.tendsto_tsum_compl_atTop_zero : ∀ {α : Type u_4} {f : α → ENNReal}, ∑' (x : α), f x ≠ ⊤ → Filter.Tendsto (fun s => ∑' (b : { x // x ∉ s }), f ↑b) Filter.atTop (nhds 0)

The theorem `ENNReal.tendsto_tsum_compl_atTop_zero` states that for any type `α` and a function `f` from `α` to the extended nonnegative real numbers (`ENNReal`), if the series sum of `f` over all elements of `α` is not infinity, then as we consider finite subsets (`s`) of `α` and sum `f` over their complements (`b`), this sum tends to zero as the finite subsets grow to cover the whole space `α`. This is expressed by saying the function mapping `s` to this sum is tending to zero at infinity (`Filter.Tendsto (fun s => ∑' (b : { x // x ∉ s }), f ↑b) Filter.atTop (nhds 0)`). This theorem does not require an assumption of summability for `f`, because if `f` isn't summable, all the sums are zero.

More concisely: Given a function `f : α -> ENNReal` such that the sum of `f` over all elements of `α` is finite, the function that maps each finite subset `s` of `α` to the sum of `f` over the complement of `s` tends to zero as the size of `s` approaches the whole space `α`.

ENNReal.Tendsto.const_mul

theorem ENNReal.Tendsto.const_mul : ∀ {α : Type u_1} {f : Filter α} {m : α → ENNReal} {a b : ENNReal}, Filter.Tendsto m f (nhds b) → b ≠ 0 ∨ a ≠ ⊤ → Filter.Tendsto (fun b => a * m b) f (nhds (a * b))

The theorem `ENNReal.Tendsto.const_mul` states that for all types `α`, filters `f` on `α`, functions `m` from `α` to the extended nonnegative real numbers `ENNReal`, and extended nonnegative real numbers `a` and `b`, if the function `m` tends to `b` as `f` tends to the neighborhood filter at `b` (expressed as `Filter.Tendsto m f (nhds b)`), and either `b` is not zero or `a` is not infinity, then the function that multiplies `a` with the image of `m` (`fun b => a * m b`) also tends to `a * b` as `f` tends to the neighborhood filter at `a * b` (expressed as `Filter.Tendsto (fun b => a * m b) f (nhds (a * b))`). In simpler terms, this theorem states that the limit of the product of a constant and a function, under certain conditions, is the product of the constant and the limit of the function.

More concisely: If a function `m` tends to `b` as filter `f` approaches `b`, and either `b` is nonzero or `a` is finite, then the function `a * m` tends to `a * b` as filter `f` approaches `a * b`.

Mathlib.Topology.Instances.ENNReal._auxLemma.1

theorem Mathlib.Topology.Instances.ENNReal._auxLemma.1 : ∀ {α : Type u_1} {f : Filter α} {m : α → NNReal} {a : NNReal}, Filter.Tendsto (fun a => ↑(m a)) f (nhds ↑a) = Filter.Tendsto m f (nhds a)

This theorem states that for any type `α`, any filter `f` over `α`, any function `m` from `α` to the nonnegative real numbers (`NNReal`), and any nonnegative real number `a`, the function `m` tends to `a` (i.e., the limit of `m` as it approaches `a` exists) under the filter `f` if and only if the function that takes each element of `α` to the real part of its image under `m` also tends to `a` under the filter `f`. In other words, the limit behaviors of the function `m` and the function that maps each element of `α` to the real part of its image under `m` are the same.

More concisely: For any type `α`, filter `f` over `α`, function `m` from `α` to `NNReal`, and real number `a`, the function `m` tends to `a` under `f` if and only if the function `x ↦ Re(m x)` tends to `a` under `f`.

ENNReal.mul_iSup

theorem ENNReal.mul_iSup : ∀ {ι : Sort u_4} {f : ι → ENNReal} {a : ENNReal}, a * iSup f = ⨆ i, a * f i

This theorem 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 product of `a` and the indexed supremum (`iSup`) of `f` is equal to the supremum (denoted by `⨆ i`) of `a` times `f i` across all `i` in `ι`. In other words, multiplication distributes over the supremum in the extended nonnegative real numbers.

More concisely: For any index type `ι`, any function `f` from `ι` to the extended nonnegative real numbers `ENNReal`, and any `ENNReal` number `a`, we have `a * ⨆ (i : ι) (a * f i) = ⨆ (i : ι) (a * f i)`.

Mathlib.Topology.Instances.ENNReal._auxLemma.22

theorem Mathlib.Topology.Instances.ENNReal._auxLemma.22 : (¬False) = True

This theorem states that the negation of 'False' is 'True'. In the context of boolean logic, where '¬' represents the logical 'not' operation, this theorem asserts the fundamental law that 'not False' equates to 'True'.

More concisely: The theorem asserts that the negation of False is True, or equivalently, not False equals True.

ENNReal.embedding_coe

theorem ENNReal.embedding_coe : Embedding ENNReal.ofNNReal

This theorem states that the function `ENNReal.ofNNReal`, which converts a non-negative real number (`NNReal`) to an extended non-negative real number (`ENNReal`), is an embedding. In mathematical terms, this means that this function injects `NNReal` into `ENNReal`, preserving the distinctness of elements and the structure of the domain.

More concisely: The function `ENNReal.ofNNReal` is an injection from the non-negative real numbers to the extended non-negative real numbers.

ENNReal.tendsto_inv_iff

theorem ENNReal.tendsto_inv_iff : ∀ {α : Type u_1} {f : Filter α} {m : α → ENNReal} {a : ENNReal}, Filter.Tendsto (fun x => (m x)⁻¹) f (nhds a⁻¹) ↔ Filter.Tendsto m f (nhds a)

This theorem states that for any type `α`, any filter `f` on `α`, any function `m` from `α` to the extended nonnegative real numbers (`ENNReal`), and any extended nonnegative real number `a`, the function `m` tends to `a` with respect to filter `f` if and only if the reciprocal function of `m` tends to the reciprocal of `a` with respect to the same filter `f`. In simpler terms, a function converges to a value if and only if its reciprocal converges to the reciprocal of that value.

More concisely: For any type `α`, filter `f` on `α`, function `m` from `α` to `ENNReal`, and extended nonnegative real number `a`, `m` tends to `a` with respect to `f` if and only if the reciprocal function of `m` tends to the reciprocal of `a` with respect to `f`.

edist_ne_top_of_mem_ball

theorem edist_ne_top_of_mem_ball : ∀ {β : Type u_2} [inst : EMetricSpace β] {a : β} {r : ENNReal} (x y : ↑(EMetric.ball a r)), edist ↑x ↑y ≠ ⊤ := by sorry

The theorem `edist_ne_top_of_mem_ball` states that for any type `β` with an `EMetricSpace` structure, any `a` of type `β`, and any radius `r` of type `ENNReal`, the extended metric distance between any two points `x` and `y` within the `EMetric.ball` centered at `a` with radius `r` is always finite. In other words, in an extended metric ball of any kind, there are no two points that are infinitely far from each other.

More concisely: For any extended metric space `(β, d)`, given `a : β`, `r : ENCReal`, and `x, y : EMetric.ball a r`, the extended metric distance `d(x, y)` is finite.

ENNReal.liminf_toReal_eq

theorem ENNReal.liminf_toReal_eq : ∀ {ι : Type u_5} {F : Filter ι} [inst : F.NeBot] {b : ENNReal}, b ≠ ⊤ → ∀ {xs : ι → ENNReal}, (∀ᶠ (i : ι) in F, xs i ≤ b) → Filter.liminf (fun i => (xs i).toReal) F = (Filter.liminf xs F).toReal

The theorem `ENNReal.liminf_toReal_eq` states that for any function `xs` mapping from an arbitrary type `ι` to the extended nonnegative real numbers (often denoted as [0, ∞]) that is bounded by a value `b` which is not infinite, we have that the limit inferior (liminf) of the real part of `xs` is equal to the real part of the limit inferior of `xs`. Here, the limit inferior is taken with respect to a non-empty filter `F`. In mathematical terms, it means that if `xs : ι → ℝ≥0∞` is bounded, then `liminf (toReal ∘ xs) = toReal (liminf xs)`, where `toReal` is a function converting the extended nonnegative real numbers to real numbers.

More concisely: For any bounded function `xs : ι → ℝ≥0∞` and non-empty filter `F`, the real part of the limit inferior of `xs` is equal to the limit inferior of the real parts of `xs`. In other words, `toReal (liminf xs) = liminf (toReal ∘ xs)`.

ENNReal.tendsto_ofReal

theorem ENNReal.tendsto_ofReal : ∀ {α : Type u_1} {f : Filter α} {m : α → ℝ} {a : ℝ}, Filter.Tendsto m f (nhds a) → Filter.Tendsto (fun a => ENNReal.ofReal (m a)) f (nhds (ENNReal.ofReal a))

The theorem `ENNReal.tendsto_ofReal` states that, for any type `α`, a filter `f` on `α`, a function `m` mapping from `α` to real numbers, and a real number `a`, if the function `m` tends towards `a` with respect to the filter `f` (that is, for every neighborhood of `a`, the preimage of that neighborhood under `m` is in the filter `f`), then the function obtained by applying `ENNReal.ofReal` (which maps a real number to its nonnegative counterpart or zero if it's negative) to `m` also tends towards the nonnegative counterpart of `a` (or zero if `a` is negative) with respect to the same filter `f`. Essentially, this theorem is asserting that if a function tends towards a real number, then the nonnegative part of that function tends towards the nonnegative part of that real number.

More concisely: If a function from a type to real numbers tends to a real number with respect to a filter, then the pointwise non-negative part of the function tends to the non-negative part of that real number with respect to the same filter.

ENNReal.continuous_coe

theorem ENNReal.continuous_coe : Continuous ENNReal.ofNNReal

This theorem asserts that the function `ENNReal.ofNNReal` is continuous. In more mathematical terms, it says that the function which coerces (or converts) a non-negative real number (represented by `NNReal`) to a non-negative extended real number (represented by `ENNReal`) is a continuous function. Here, "continuous" means that for any sequence of non-negative real numbers, the sequence of their images under this function will converge to the image of the limit of the original sequence. This ensures that no "gaps" or "jumps" appear when we map these numbers from `NNReal` to `ENNReal`.

More concisely: The function `ENNReal.ofNNReal` is a continuous mapping from the non-negative real numbers to the non-negative extended real numbers.

ENNReal.continuous_truncateToReal

theorem ENNReal.continuous_truncateToReal : ∀ {t : ENNReal}, t ≠ ⊤ → Continuous t.truncateToReal

This theorem states that the truncated cast `ENNReal.truncateToReal t : ℝ≥0∞ → ℝ`, which maps from the extended nonnegative real numbers (usually denoted [0, ∞]) to the real numbers, is continuous as long as the input `t` is not equal to infinity. In other words, the function is continuous everywhere in its domain except at the point infinity.

More concisely: The truncation function from the extended non-negative real numbers to the real numbers, defined as `ENNReal.truncateToReal`, is continuous for all finite arguments.