doc-next-gen

Mathlib.Topology.Instances.NNReal.Lemmas

Module docstring

{"# Topology on ℝ≥0

The basic lemmas for the natural topology on ℝ≥0 .

Main statements

Various mathematically trivial lemmas are proved about the compatibility of limits and sums in ℝ≥0 and ℝ. For example

  • tendsto_coe {f : Filter α} {m : α → ℝ≥0} {x : ℝ≥0} : Filter.Tendsto (fun a, (m a : ℝ)) f (𝓝 (x : ℝ)) ↔ Filter.Tendsto m f (𝓝 x)

says that the limit of a filter along a map to ℝ≥0 is the same in ℝ and ℝ≥0, and

  • coe_tsum {f : α → ℝ≥0} : ((∑'a, f a) : ℝ) = (∑'a, (f a : ℝ))

says that says that a sum of elements in ℝ≥0 is the same in ℝ and ℝ≥0.

Similarly, some mathematically trivial lemmas about infinite sums are proved, a few of which rely on the fact that subtraction is continuous.

"}

NNReal.isOpen_Ico_zero theorem
{x : NNReal} : IsOpen (Set.Ico 0 x)
Full source 
lemma isOpen_Ico_zero {x : NNReal} : IsOpen (Set.Ico 0 x) :=
  Ico_bot (a := x) ▸ isOpen_Iio
Openness of the Interval $[0, x)$ in Non-Negative Reals
Informal description
For any non-negative real number $x \in \mathbb{R}_{\geq 0}$, the left-closed right-open interval $[0, x)$ is an open set in the natural topology on $\mathbb{R}_{\geq 0}$.
ContinuousMap.realToNNReal definition
: C(ℝ, ℝ≥0)
Full source 
/-- `Real.toNNReal` bundled as a continuous map for convenience. -/
@[simps -fullyApplied]
noncomputable def _root_.ContinuousMap.realToNNReal : C(ℝ, ℝ≥0) :=
  .mk Real.toNNReal continuous_real_toNNReal
Continuous non-negative projection on real numbers
Informal description
The continuous map version of the function $\operatorname{toNNReal} : \mathbb{R} \to \mathbb{R}_{\geq 0}$, which maps a real number to its non-negative part.
ContinuousOn.ofReal_map_toNNReal theorem
{f : ℝ≥0 → ℝ≥0} {s : Set ℝ} {t : Set ℝ≥0} (hf : ContinuousOn f t) (h : Set.MapsTo Real.toNNReal s t) : ContinuousOn (fun x ↦ f x.toNNReal : ℝ → ℝ) s
Full source 
lemma _root_.ContinuousOn.ofReal_map_toNNReal {f : ℝ≥0 → ℝ≥0} {s : Set ℝ} {t : Set ℝ≥0}
    (hf : ContinuousOn f t) (h : Set.MapsTo Real.toNNReal s t) :
    ContinuousOn (fun x ↦ f x.toNNReal : ℝ → ℝ) s :=
  continuous_subtype_val.comp_continuousOn <| hf.comp continuous_real_toNNReal.continuousOn h
Continuity of Composition with Nonnegative Projection on Restricted Domain
Informal description
Let $f \colon \mathbb{R}_{\geq 0} \to \mathbb{R}_{\geq 0}$ be a function, $s \subseteq \mathbb{R}$ and $t \subseteq \mathbb{R}_{\geq 0}$ be sets. If $f$ is continuous on $t$ and the nonnegative projection $\operatorname{toNNReal} \colon \mathbb{R} \to \mathbb{R}_{\geq 0}$ maps $s$ into $t$, then the composition $x \mapsto f(x.\operatorname{toNNReal})$ is continuous on $s$.
NNReal.tendsto_coe theorem
{f : Filter α} {m : α → ℝ≥0} {x : ℝ≥0} : Tendsto (fun a => (m a : ℝ)) f (𝓝 (x : ℝ)) ↔ Tendsto m f (𝓝 x)
Full source 
@[simp, norm_cast]
theorem tendsto_coe {f : Filter α} {m : α → ℝ≥0} {x : ℝ≥0} :
    TendstoTendsto (fun a => (m a : ℝ)) f (𝓝 (x : ℝ)) ↔ Tendsto m f (𝓝 x) :=
  tendsto_subtype_rng.symm
Equivalence of Limits in Nonnegative Reals and Their Real Embedding
Informal description
Let $f$ be a filter on a type $\alpha$, $m : \alpha \to \mathbb{R}_{\geq 0}$ be a function, and $x \in \mathbb{R}_{\geq 0}$. Then the limit of the composition $\text{toReal} \circ m$ along $f$ equals the real number $x$ if and only if the limit of $m$ along $f$ equals $x$ in $\mathbb{R}_{\geq 0}$. In other words, the following are equivalent: 1. $\lim_{a \in f} (m(a) : \mathbb{R}) = (x : \mathbb{R})$ 2. $\lim_{a \in f} m(a) = x$ in $\mathbb{R}_{\geq 0}$
NNReal.tendsto_coe' theorem
{f : Filter α} [NeBot f] {m : α → ℝ≥0} {x : ℝ} : Tendsto (fun a => m a : α → ℝ) f (𝓝 x) ↔ ∃ hx : 0 ≤ x, Tendsto m f (𝓝 ⟨x, hx⟩)
Full source 
theorem tendsto_coe' {f : Filter α} [NeBot f] {m : α → ℝ≥0} {x : ℝ} :
    TendstoTendsto (fun a => m a : α → ℝ) f (𝓝 x) ↔ ∃ hx : 0 ≤ x, Tendsto m f (𝓝 ⟨x, hx⟩) :=
  ⟨fun h => ⟨ge_of_tendsto' h fun c => (m c).2, tendsto_coe.1 h⟩, fun ⟨_, hm⟩ => tendsto_coe.2 hm⟩
Limit Equivalence for Nonnegative Reals with Non-Trivial Filter
Informal description
Let $f$ be a non-trivial filter on a type $\alpha$, $m : \alpha \to \mathbb{R}_{\geq 0}$ be a function, and $x \in \mathbb{R}$. Then the following are equivalent: 1. The limit of the composition $\text{toReal} \circ m$ along $f$ equals the real number $x$. 2. There exists a proof $h_x$ that $0 \leq x$, and the limit of $m$ along $f$ equals the nonnegative real number $\langle x, h_x \rangle$. In other words, $\lim_{a \in f} (m(a) : \mathbb{R}) = x$ if and only if $x \geq 0$ and $\lim_{a \in f} m(a) = x$ in $\mathbb{R}_{\geq 0}$.
NNReal.map_coe_atTop theorem
: map toReal atTop = atTop
Full source 
@[simp] theorem map_coe_atTop : map toReal atTop = atTop := map_val_Ici_atTop 0
Preservation of Infinity Filter under Nonnegative Real Embedding
Informal description
The image of the filter `atTop` under the canonical embedding from `ℝ≥0` to `ℝ` is equal to `atTop`. In other words, the map `toReal : ℝ≥0 → ℝ` preserves the filter of neighborhoods at infinity.
NNReal.comap_coe_atTop theorem
: comap toReal atTop = atTop
Full source 
@[simp]
theorem comap_coe_atTop : comap toReal atTop = atTop := (atTop_Ici_eq 0).symm
Preimage of Infinity Filter under Nonnegative Real Embedding
Informal description
The preimage of the filter `atTop` on $\mathbb{R}$ under the canonical embedding from $\mathbb{R}_{\geq 0}$ to $\mathbb{R}$ is equal to the filter `atTop` on $\mathbb{R}_{\geq 0}$. In other words, the canonical embedding preserves the filter of neighborhoods at infinity in both directions.
NNReal.tendsto_coe_atTop theorem
{f : Filter α} {m : α → ℝ≥0} : Tendsto (fun a => (m a : ℝ)) f atTop ↔ Tendsto m f atTop
Full source 
@[simp, norm_cast]
theorem tendsto_coe_atTop {f : Filter α} {m : α → ℝ≥0} :
    TendstoTendsto (fun a => (m a : ℝ)) f atTop ↔ Tendsto m f atTop :=
  tendsto_Ici_atTop.symm
Equivalence of Tendency to Infinity in Nonnegative Reals and Reals
Informal description
For any filter $f$ on a type $\alpha$ and any function $m : \alpha \to \mathbb{R}_{\geq 0}$, the following are equivalent: 1. The function $a \mapsto (m a : \mathbb{R})$ tends to infinity along $f$. 2. The function $m$ tends to infinity along $f$. Here, $\mathbb{R}_{\geq 0}$ denotes the nonnegative real numbers, and "tends to infinity" refers to convergence in the filter `atTop`, which describes behavior as values grow without bound.
tendsto_real_toNNReal theorem
{f : Filter α} {m : α → ℝ} {x : ℝ} (h : Tendsto m f (𝓝 x)) : Tendsto (fun a => Real.toNNReal (m a)) f (𝓝 (Real.toNNReal x))
Full source 
theorem _root_.tendsto_real_toNNReal {f : Filter α} {m : α → ℝ} {x : ℝ} (h : Tendsto m f (𝓝 x)) :
    Tendsto (fun a => Real.toNNReal (m a)) f (𝓝 (Real.toNNReal x)) :=
  (continuous_real_toNNReal.tendsto _).comp h
Continuity of Non-Negative Projection at a Point
Informal description
Let $f$ be a filter on a type $\alpha$, $m : \alpha \to \mathbb{R}$ a function, and $x \in \mathbb{R}$. If $m$ tends to $x$ along $f$ in $\mathbb{R}$, then the composition $\operatorname{toNNReal} \circ m$ tends to $\operatorname{toNNReal}(x)$ along $f$ in $\mathbb{R}_{\geq 0}$.
Real.map_toNNReal_atTop theorem
: map Real.toNNReal atTop = atTop
Full source 
@[simp]
theorem _root_.Real.map_toNNReal_atTop : map Real.toNNReal atTop = atTop := by
  rw [← map_coe_atTop, Function.LeftInverse.filter_map @Real.toNNReal_coe]
Preservation of Infinity Filter under Nonnegative Real Projection
Informal description
The image of the filter `atTop` (neighborhoods of infinity) under the canonical map `Real.toNNReal : ℝ → ℝ≥0` is equal to `atTop`. In other words, the map preserves the filter at infinity.
tendsto_real_toNNReal_atTop theorem
: Tendsto Real.toNNReal atTop atTop
Full source 
theorem _root_.tendsto_real_toNNReal_atTop : Tendsto Real.toNNReal atTop atTop :=
  Real.map_toNNReal_atTop.le
Projection to Non-Negative Reals Preserves Limits at Infinity
Informal description
The canonical projection function $\operatorname{toNNReal} : \mathbb{R} \to \mathbb{R}_{\geq 0}$ preserves limits at infinity, i.e., if a real-valued function tends to infinity, then its non-negative projection also tends to infinity.
Real.comap_toNNReal_atTop theorem
: comap Real.toNNReal atTop = atTop
Full source 
@[simp]
theorem _root_.Real.comap_toNNReal_atTop : comap Real.toNNReal atTop = atTop := by
  refine le_antisymm ?_ tendsto_real_toNNReal_atTop.le_comap
  refine (atTop_basis_Ioi' 0).ge_iff.2 fun a ha ↦ ?_
  filter_upwards [preimage_mem_comap (Ioi_mem_atTop a.toNNReal)] with x hx
  exact (Real.toNNReal_lt_toNNReal_iff_of_nonneg ha.le).1 hx
Preimage of Infinity Filter under Nonnegative Real Projection Equals Infinity Filter
Informal description
The preimage filter of the neighborhood of infinity in $\mathbb{R}_{\geq 0}$ under the canonical projection $\operatorname{toNNReal} : \mathbb{R} \to \mathbb{R}_{\geq 0}$ is equal to the neighborhood of infinity in $\mathbb{R}$. In other words, $\operatorname{toNNReal}^{-1}(\text{atTop}) = \text{atTop}$.
Real.tendsto_toNNReal_atTop_iff theorem
{l : Filter α} {f : α → ℝ} : Tendsto (fun x ↦ (f x).toNNReal) l atTop ↔ Tendsto f l atTop
Full source 
@[simp]
theorem _root_.Real.tendsto_toNNReal_atTop_iff {l : Filter α} {f : α → ℝ} :
    TendstoTendsto (fun x ↦ (f x).toNNReal) l atTop ↔ Tendsto f l atTop := by
  rw [← Real.comap_toNNReal_atTop, tendsto_comap_iff, Function.comp_def]
Equivalence of Tendency to Infinity for Real Function and Its Nonnegative Part
Informal description
For any filter $l$ on a type $\alpha$ and any function $f : \alpha \to \mathbb{R}$, the following are equivalent: 1. The function $x \mapsto \max(f(x), 0)$ tends to infinity along $l$. 2. The function $f$ tends to infinity along $l$. In other words, $\lim_{l} \max(f, 0) = \infty$ if and only if $\lim_{l} f = \infty$.
Real.tendsto_toNNReal_atTop theorem
: Tendsto Real.toNNReal atTop atTop
Full source 
theorem _root_.Real.tendsto_toNNReal_atTop : Tendsto Real.toNNReal atTop atTop :=
  Real.tendsto_toNNReal_atTop_iff.2 tendsto_id
Projection to Nonnegative Reals Preserves Infinity Limit
Informal description
The canonical projection function $\operatorname{toNNReal} : \mathbb{R} \to \mathbb{R}_{\geq 0}$, defined by $x \mapsto \max(x, 0)$, tends to infinity as its input tends to infinity. In other words, $\lim_{x \to \infty} \operatorname{toNNReal}(x) = \infty$.
NNReal.nhds_zero theorem
: 𝓝 (0 : ℝ≥0) = ⨅ (a : ℝ≥0) (_ : a ≠ 0), 𝓟 (Iio a)
Full source 
theorem nhds_zero : 𝓝 (0 : ℝ≥0) = ⨅ (a : ℝ≥0) (_ : a ≠ 0), 𝓟 (Iio a) :=
  nhds_bot_order.trans <| by simp only [bot_lt_iff_ne_bot]; rfl
Neighborhood Filter of Zero in Nonnegative Reals via Intervals
Informal description
The neighborhood filter of $0$ in the space of nonnegative real numbers $\mathbb{R}_{\geq 0}$ is equal to the infimum over all nonzero $a \in \mathbb{R}_{\geq 0}$ of the principal filters generated by the left-infinite right-open intervals $(-\infty, a)$. In other words, $\mathcal{N}(0) = \bigwedge_{a \neq 0} \mathcal{P}(\{x \mid x < a\})$.
NNReal.nhds_zero_basis theorem
: (𝓝 (0 : ℝ≥0)).HasBasis (fun a : ℝ≥0 => 0 < a) fun a => Iio a
Full source 
theorem nhds_zero_basis : (𝓝 (0 : ℝ≥0)).HasBasis (fun a : ℝ≥0 => 0 < a) fun a => Iio a :=
  nhds_bot_basis
Basis of Neighborhoods of Zero in $\mathbb{R}_{\geq 0}$ via Left-Infinite Right-Open Intervals
Informal description
The neighborhood filter $\mathcal{N}(0)$ of zero in $\mathbb{R}_{\geq 0}$ has a basis consisting of the left-infinite right-open intervals $(-\infty, a)$ for all $a > 0$ in $\mathbb{R}_{\geq 0}$. In other words, the filter $\mathcal{N}(0)$ is generated by the sets $\{x \mid x < a\}$ where $a$ ranges over all positive elements of $\mathbb{R}_{\geq 0}$.
NNReal.hasSum_coe theorem
{f : α → ℝ≥0} {r : ℝ≥0} : HasSum (fun a => (f a : ℝ)) (r : ℝ) ↔ HasSum f r
Full source 
@[norm_cast]
theorem hasSum_coe {f : α → ℝ≥0} {r : ℝ≥0} : HasSumHasSum (fun a => (f a : ℝ)) (r : ℝ) ↔ HasSum f r := by
  simp only [HasSum, ← coe_sum, tendsto_coe]
Equivalence of Sum Convergence in $\mathbb{R}_{\geq 0}$ and $\mathbb{R}$
Informal description
For a function $f \colon \alpha \to \mathbb{R}_{\geq 0}$ and an element $r \in \mathbb{R}_{\geq 0}$, the sum of the real-valued function $\lambda a, (f(a) : \mathbb{R})$ converges to $r$ (as a real number) if and only if the sum of $f$ converges to $r$ in $\mathbb{R}_{\geq 0}$.
HasSum.toNNReal theorem
{f : α → ℝ} {y : ℝ} (hf₀ : ∀ n, 0 ≤ f n) (hy : HasSum f y) : HasSum (fun x => Real.toNNReal (f x)) y.toNNReal
Full source 
protected theorem _root_.HasSum.toNNReal {f : α → ℝ} {y : ℝ} (hf₀ : ∀ n, 0 ≤ f n)
    (hy : HasSum f y) : HasSum (fun x => Real.toNNReal (f x)) y.toNNReal := by
  lift y to ℝ≥0 using hy.nonneg hf₀
  lift f to α → ℝ≥0 using hf₀
  simpa [hasSum_coe] using hy
Convergence of Nonnegative Sums to Nonnegative Reals via `toNNReal`
Informal description
For any function $f \colon \alpha \to \mathbb{R}$ with nonnegative values (i.e., $f(n) \geq 0$ for all $n \in \alpha$) and a real number $y \in \mathbb{R}$, if the sum of $f$ converges to $y$ (i.e., $\text{HasSum}\, f\, y$), then the sum of the nonnegative real-valued function $\lambda x, \text{Real.toNNReal}(f(x))$ converges to $\text{Real.toNNReal}(y)$ in $\mathbb{R}_{\geq 0}$.
NNReal.hasSum_real_toNNReal_of_nonneg theorem
{f : α → ℝ} (hf_nonneg : ∀ n, 0 ≤ f n) (hf : Summable f) : HasSum (fun n => Real.toNNReal (f n)) (Real.toNNReal (∑' n, f n))
Full source 
theorem hasSum_real_toNNReal_of_nonneg {f : α → ℝ} (hf_nonneg : ∀ n, 0 ≤ f n) (hf : Summable f) :
    HasSum (fun n => Real.toNNReal (f n)) (Real.toNNReal (∑' n, f n)) :=
  hf.hasSum.toNNReal hf_nonneg
Convergence of Nonnegative Summable Functions to Their Nonnegative Real Sum via `toNNReal`
Informal description
For any function $f \colon \alpha \to \mathbb{R}$ with nonnegative values (i.e., $f(n) \geq 0$ for all $n \in \alpha$) that is summable, the sum of the nonnegative real-valued function $\lambda n, \text{Real.toNNReal}(f(n))$ converges to $\text{Real.toNNReal}(\sum' n, f(n))$ in $\mathbb{R}_{\geq 0}$.
NNReal.summable_coe theorem
{f : α → ℝ≥0} : (Summable fun a => (f a : ℝ)) ↔ Summable f
Full source 
@[norm_cast]
theorem summable_coe {f : α → ℝ≥0} : (Summable fun a => (f a : ℝ)) ↔ Summable f := by
  constructor
  · exact fun ⟨a, ha⟩ => ⟨⟨a, ha.nonneg fun x => (f x).2⟩, hasSum_coe.1 ha⟩
  · exact fun ⟨a, ha⟩ => ⟨a.1, hasSum_coe.2 ha⟩
Summability Equivalence Between $\mathbb{R}_{\geq 0}$ and $\mathbb{R}$
Informal description
For a function $f \colon \alpha \to \mathbb{R}_{\geq 0}$, the real-valued function $\lambda a, (f(a) : \mathbb{R})$ is summable if and only if $f$ is summable in $\mathbb{R}_{\geq 0}$.
NNReal.summable_mk theorem
{f : α → ℝ} (hf : ∀ n, 0 ≤ f n) : (@Summable ℝ≥0 _ _ _ fun n => ⟨f n, hf n⟩) ↔ Summable f
Full source 
theorem summable_mk {f : α → ℝ} (hf : ∀ n, 0 ≤ f n) :
    (@Summable ℝ≥0 _ _ _ fun n => ⟨f n, hf n⟩) ↔ Summable f :=
  Iff.symm <| summable_coe (f := fun x => ⟨f x, hf x⟩)
Summability Equivalence for Nonnegative Real Functions in $\mathbb{R}_{\geq 0}$ and $\mathbb{R}$
Informal description
For a function $f \colon \alpha \to \mathbb{R}$ with $f(n) \geq 0$ for all $n$, the function $\lambda n, \langle f(n), hf(n) \rangle$ (where $\langle \cdot, \cdot \rangle$ constructs an element of $\mathbb{R}_{\geq 0}$) is summable in $\mathbb{R}_{\geq 0}$ if and only if $f$ is summable in $\mathbb{R}$.
NNReal.coe_tsum theorem
{f : α → ℝ≥0} : ↑(∑' a, f a) = ∑' a, (f a : ℝ)
Full source 
@[norm_cast]
theorem coe_tsum {f : α → ℝ≥0} : ↑(∑' a, f a) = ∑' a, (f a : ℝ) := by
  classical
  exact if hf : Summable f then Eq.symm <| (hasSum_coe.2 <| hf.hasSum).tsum_eq
  else by simp [tsum_def, hf, mt summable_coe.1 hf]
Sum Preservation Under Canonical Embedding: $\mathbb{R}_{\geq 0} \to \mathbb{R}$
Informal description
For any function $f \colon \alpha \to \mathbb{R}_{\geq 0}$, the canonical embedding of the sum of $f$ in $\mathbb{R}_{\geq 0}$ into $\mathbb{R}$ is equal to the sum of the embedded function values, i.e., $$ \left(\sum_{a} f(a)\right)_{\mathbb{R}} = \sum_{a} (f(a))_{\mathbb{R}}. $$
NNReal.coe_tsum_of_nonneg theorem
{f : α → ℝ} (hf₁ : ∀ n, 0 ≤ f n) : (⟨∑' n, f n, tsum_nonneg hf₁⟩ : ℝ≥0) = (∑' n, ⟨f n, hf₁ n⟩ : ℝ≥0)
Full source 
theorem coe_tsum_of_nonneg {f : α → ℝ} (hf₁ : ∀ n, 0 ≤ f n) :
    (⟨∑' n, f n, tsum_nonneg hf₁⟩ : ℝ≥0) = (∑' n, ⟨f n, hf₁ n⟩ : ℝ≥0) :=
  NNReal.eq <| Eq.symm <| coe_tsum (f := fun x => ⟨f x, hf₁ x⟩)
Sum Equality for Nonnegative Functions in $\mathbb{R}_{\geq 0}$ via Canonical Embedding
Informal description
For any function $f \colon \alpha \to \mathbb{R}$ with $f(n) \geq 0$ for all $n$, the canonical embedding of the sum $\sum_{n} f(n)$ into $\mathbb{R}_{\geq 0}$ (constructed using the nonnegativity condition $\text{tsum\_nonneg } hf₁$) is equal to the sum of the canonical embeddings $\sum_{n} \langle f(n), hf₁(n) \rangle$ in $\mathbb{R}_{\geq 0}$.
NNReal.tsum_mul_left theorem
(a : ℝ≥0) (f : α → ℝ≥0) : ∑' x, a * f x = a * ∑' x, f x
Full source 
nonrec theorem tsum_mul_left (a : ℝ≥0) (f : α → ℝ≥0) : ∑' x, a * f x = a * ∑' x, f x :=
  NNReal.eq <| by simp only [coe_tsum, NNReal.coe_mul, tsum_mul_left]
Left Multiplication Commutes with Summation in $\mathbb{R}_{\geq 0}$
Informal description
For any nonnegative real number $a \in \mathbb{R}_{\geq 0}$ and any function $f \colon \alpha \to \mathbb{R}_{\geq 0}$, the sum of the products $a \cdot f(x)$ over all $x \in \alpha$ is equal to the product of $a$ with the sum of $f(x)$, i.e., $$ \sum_{x} a \cdot f(x) = a \cdot \left(\sum_{x} f(x)\right). $$
NNReal.tsum_mul_right theorem
(f : α → ℝ≥0) (a : ℝ≥0) : ∑' x, f x * a = (∑' x, f x) * a
Full source 
nonrec theorem tsum_mul_right (f : α → ℝ≥0) (a : ℝ≥0) : ∑' x, f x * a = (∑' x, f x) * a :=
  NNReal.eq <| by simp only [coe_tsum, NNReal.coe_mul, tsum_mul_right]
Right Multiplication Commutes with Summation in $\mathbb{R}_{\geq 0}$
Informal description
For any function $f \colon \alpha \to \mathbb{R}_{\geq 0}$ and any nonnegative real number $a \in \mathbb{R}_{\geq 0}$, the sum of the products $f(x) \cdot a$ over all $x \in \alpha$ is equal to the product of the sum of $f(x)$ with $a$, i.e., $$ \sum_{x} f(x) \cdot a = \left(\sum_{x} f(x)\right) \cdot a. $$
NNReal.summable_comp_injective theorem
{β : Type*} {f : α → ℝ≥0} (hf : Summable f) {i : β → α} (hi : Function.Injective i) : Summable (f ∘ i)
Full source 
theorem summable_comp_injective {β : Type*} {f : α → ℝ≥0} (hf : Summable f) {i : β → α}
    (hi : Function.Injective i) : Summable (f ∘ i) := by
  rw [← summable_coe] at hf ⊢
  exact hf.comp_injective hi
Summability under Injective Composition in $\mathbb{R}_{\geq 0}$
Informal description
Let $f \colon \alpha \to \mathbb{R}_{\geq 0}$ be a summable function, and let $i \colon \beta \to \alpha$ be an injective function. Then the composition $f \circ i \colon \beta \to \mathbb{R}_{\geq 0}$ is also summable.
NNReal.summable_nat_add theorem
(f : ℕ → ℝ≥0) (hf : Summable f) (k : ℕ) : Summable fun i => f (i + k)
Full source 
theorem summable_nat_add (f : ℕ → ℝ≥0) (hf : Summable f) (k : ℕ) : Summable fun i => f (i + k) :=
  summable_comp_injective hf <| add_left_injective k
Summability of Shifted Nonnegative Real Sequences
Informal description
For any summable sequence $f \colon \mathbb{N} \to \mathbb{R}_{\geq 0}$ and any natural number $k$, the shifted sequence $(i \mapsto f(i + k))$ is also summable.
NNReal.summable_nat_add_iff theorem
{f : ℕ → ℝ≥0} (k : ℕ) : (Summable fun i => f (i + k)) ↔ Summable f
Full source 
nonrec theorem summable_nat_add_iff {f : ℕ → ℝ≥0} (k : ℕ) :
    (Summable fun i => f (i + k)) ↔ Summable f := by
  rw [← summable_coe, ← summable_coe]
  exact @summable_nat_add_iff ℝ _ _ _ (fun i => (f i : ℝ)) k
Summability Equivalence for Shifted Nonnegative Real Sequences
Informal description
For a sequence $f \colon \mathbb{N} \to \mathbb{R}_{\geq 0}$ and a natural number $k$, the shifted sequence $(i \mapsto f(i + k))$ is summable if and only if the original sequence $f$ is summable.
NNReal.hasSum_nat_add_iff theorem
{f : ℕ → ℝ≥0} (k : ℕ) {a : ℝ≥0} : HasSum (fun n => f (n + k)) a ↔ HasSum f (a + ∑ i ∈ range k, f i)
Full source 
nonrec theorem hasSum_nat_add_iff {f : ℕ → ℝ≥0} (k : ℕ) {a : ℝ≥0} :
    HasSumHasSum (fun n => f (n + k)) a ↔ HasSum f (a + ∑ i ∈ range k, f i) := by
  rw [← hasSum_coe, hasSum_nat_add_iff (f := fun n => toReal (f n)) k]; norm_cast
Shifted Sum Convergence Equivalence for Nonnegative Real Sequences
Informal description
For a nonnegative real-valued sequence $f \colon \mathbb{N} \to \mathbb{R}_{\geq 0}$, a natural number $k$, and a nonnegative real number $a \in \mathbb{R}_{\geq 0}$, the sum of the shifted sequence $\sum_{n=0}^\infty f(n + k)$ converges to $a$ if and only if the original sum $\sum_{n=0}^\infty f(n)$ converges to $a + \sum_{i=0}^{k-1} f(i)$.
NNReal.sum_add_tsum_nat_add theorem
{f : ℕ → ℝ≥0} (k : ℕ) (hf : Summable f) : ∑' i, f i = (∑ i ∈ range k, f i) + ∑' i, f (i + k)
Full source 
theorem sum_add_tsum_nat_add {f : ℕ → ℝ≥0} (k : ℕ) (hf : Summable f) :
    ∑' i, f i = (∑ i ∈ range k, f i) + ∑' i, f (i + k) :=
  (((summable_nat_add_iff k).2 hf).sum_add_tsum_nat_add').symm
Decomposition of Summable Nonnegative Series into Initial Segment and Shifted Tail
Informal description
For any summable sequence $f \colon \mathbb{N} \to \mathbb{R}_{\geq 0}$ and any natural number $k$, the total sum $\sum_{i=0}^\infty f(i)$ equals the sum of the first $k$ terms $\sum_{i=0}^{k-1} f(i)$ plus the sum of the remaining terms $\sum_{i=0}^\infty f(i + k)$.
NNReal.iInf_real_pos_eq_iInf_nnreal_pos theorem
[CompleteLattice α] {f : ℝ → α} : ⨅ (n : ℝ) (_ : 0 < n), f n = ⨅ (n : ℝ≥0) (_ : 0 < n), f n
Full source 
theorem iInf_real_pos_eq_iInf_nnreal_pos [CompleteLattice α] {f : ℝ → α} :
    ⨅ (n : ℝ) (_ : 0 < n), f n = ⨅ (n : ℝ≥0) (_ : 0 < n), f n :=
  le_antisymm (iInf_mono' fun r => ⟨r, le_rfl⟩) (iInf₂_mono' fun r hr => ⟨⟨r, hr.le⟩, hr, le_rfl⟩)
Infimum Equality for Positive Reals and Nonnegative Reals
Informal description
For any complete lattice $\alpha$ and any function $f \colon \mathbb{R} \to \alpha$, the infimum of $f(n)$ over all positive real numbers $n$ is equal to the infimum of $f(n)$ over all positive nonnegative real numbers $n \in \mathbb{R}_{\geq 0}$. That is, \[ \bigwedge_{n \in \mathbb{R}, \, n > 0} f(n) = \bigwedge_{n \in \mathbb{R}_{\geq 0}, \, n > 0} f(n). \]
NNReal.tendsto_cofinite_zero_of_summable theorem
{α} {f : α → ℝ≥0} (hf : Summable f) : Tendsto f cofinite (𝓝 0)
Full source 
theorem tendsto_cofinite_zero_of_summable {α} {f : α → ℝ≥0} (hf : Summable f) :
    Tendsto f cofinite (𝓝 0) := by
  simp only [← summable_coe, ← tendsto_coe] at hf ⊢
  exact hf.tendsto_cofinite_zero
Summable Nonnegative Real-Valued Functions Tend to Zero Cofinitely
Informal description
For any function $f : \alpha \to \mathbb{R}_{\geq 0}$ such that the sum $\sum_{a \in \alpha} f(a)$ converges, the function $f$ tends to $0$ along the cofinite filter on $\alpha$. In other words, for every $\epsilon > 0$, the set $\{a \in \alpha \mid f(a) \geq \epsilon\}$ is finite.
NNReal.tendsto_atTop_zero_of_summable theorem
{f : ℕ → ℝ≥0} (hf : Summable f) : Tendsto f atTop (𝓝 0)
Full source 
theorem tendsto_atTop_zero_of_summable {f : ℕ → ℝ≥0} (hf : Summable f) : Tendsto f atTop (𝓝 0) := by
  rw [← Nat.cofinite_eq_atTop]
  exact tendsto_cofinite_zero_of_summable hf
Summable Nonnegative Sequences Tend to Zero at Infinity
Informal description
For any summable sequence $f \colon \mathbb{N} \to \mathbb{R}_{\geq 0}$, the sequence $f(n)$ tends to $0$ as $n$ tends to infinity. That is, $\lim_{n \to \infty} f(n) = 0$.
NNReal.tendsto_tsum_compl_atTop_zero theorem
{α : Type*} (f : α → ℝ≥0) : Tendsto (fun s : Finset α => ∑' b : { x // x ∉ s }, f b) atTop (𝓝 0)
Full source 
/-- The sum over the complement of a finset tends to `0` when the finset grows to cover the whole
space. This does not need a summability assumption, as otherwise all sums are zero. -/
nonrec theorem tendsto_tsum_compl_atTop_zero {α : Type*} (f : α → ℝ≥0) :
    Tendsto (fun s : Finset α => ∑' b : { x // x ∉ s }, f b) atTop (𝓝 0) := by
  simp_rw [← tendsto_coe, coe_tsum, NNReal.coe_zero]
  exact tendsto_tsum_compl_atTop_zero fun a : α => (f a : ℝ)
Limit of Sum over Complement Vanishes for Nonnegative Functions
Informal description
For any function $f \colon \alpha \to \mathbb{R}_{\geq 0}$, the sum of $f$ over the complement of any finite subset $s \subset \alpha$ tends to $0$ as $s$ grows to cover all of $\alpha$. In other words, $$ \lim_{s \to \infty} \sum_{b \notin s} f(b) = 0. $$
NNReal.powOrderIso definition
(n : ℕ) (hn : n ≠ 0) : ℝ≥0 ≃o ℝ≥0
Full source 
/-- `x ↦ x ^ n` as an order isomorphism of `ℝ≥0`. -/
def powOrderIso (n : ℕ) (hn : n ≠ 0) : ℝ≥0ℝ≥0 ≃o ℝ≥0 :=
  StrictMono.orderIsoOfSurjective (fun x ↦ x ^ n) (fun x y h =>
      pow_left_strictMonoOn₀ hn (zero_le x) (zero_le y) h) <|
    (continuous_id.pow _).surjective (tendsto_pow_atTop hn) <| by
      simpa [OrderBot.atBot_eq, pos_iff_ne_zero]
Order isomorphism of \( x \mapsto x^n \) on nonnegative reals
Informal description
For any nonzero natural number \( n \), the function \( x \mapsto x^n \) is an order isomorphism on the set of nonnegative real numbers \( \mathbb{R}_{\geq 0} \). This means it is a bijective, strictly increasing function that preserves the order structure, and its inverse is also strictly increasing.
Real.tendsto_of_bddAbove_monotone theorem
{f : ℕ → ℝ} (h_bdd : BddAbove (Set.range f)) (h_mon : Monotone f) : ∃ r : ℝ, Tendsto f atTop (𝓝 r)
Full source 
/-- A monotone, bounded above sequence `f : ℕ → ℝ` has a finite limit. -/
theorem _root_.Real.tendsto_of_bddAbove_monotone {f : ℕ → ℝ} (h_bdd : BddAbove (Set.range f))
    (h_mon : Monotone f) : ∃ r : ℝ, Tendsto f atTop (𝓝 r) := by
  obtain ⟨B, hB⟩ := Real.exists_isLUB (Set.range_nonempty f) h_bdd
  exact ⟨B, tendsto_atTop_isLUB h_mon hB⟩
Convergence of Monotone Bounded Above Sequences in $\mathbb{R}$
Informal description
For any monotone sequence $f \colon \mathbb{N} \to \mathbb{R}$ that is bounded above, there exists a real number $r$ such that $f$ converges to $r$ as $n \to \infty$.
Real.tendsto_of_bddBelow_antitone theorem
{f : ℕ → ℝ} (h_bdd : BddBelow (Set.range f)) (h_ant : Antitone f) : ∃ r : ℝ, Tendsto f atTop (𝓝 r)
Full source 
/-- An antitone, bounded below sequence `f : ℕ → ℝ` has a finite limit. -/
theorem _root_.Real.tendsto_of_bddBelow_antitone {f : ℕ → ℝ} (h_bdd : BddBelow (Set.range f))
    (h_ant : Antitone f) : ∃ r : ℝ, Tendsto f atTop (𝓝 r) := by
  obtain ⟨B, hB⟩ := Real.exists_isGLB (Set.range_nonempty f) h_bdd
  exact ⟨B, tendsto_atTop_isGLB h_ant hB⟩
Convergence of Bounded Below Antitone Sequences in $\mathbb{R}$
Informal description
For any antitone sequence $f \colon \mathbb{N} \to \mathbb{R}$ that is bounded below, there exists a real number $r$ such that $f$ converges to $r$ as $n \to \infty$.
NNReal.tendsto_of_antitone theorem
{f : ℕ → ℝ≥0} (h_ant : Antitone f) : ∃ r : ℝ≥0, Tendsto f atTop (𝓝 r)
Full source 
/-- An antitone sequence `f : ℕ → ℝ≥0` has a finite limit. -/
theorem tendsto_of_antitone {f : ℕ → ℝ≥0} (h_ant : Antitone f) :
    ∃ r : ℝ≥0, Tendsto f atTop (𝓝 r) := by
  have h_bdd_0 : (0 : ℝ) ∈ lowerBounds (Set.range fun n : ℕ => (f n : ℝ)) := by
    rintro r ⟨n, hn⟩
    simp_rw [← hn]
    exact NNReal.coe_nonneg _
  obtain ⟨L, hL⟩ := Real.tendsto_of_bddBelow_antitone ⟨0, h_bdd_0⟩ h_ant
  have hL0 : 0 ≤ L :=
    haveI h_glb : IsGLB (Set.range fun n => (f n : ℝ)) L := isGLB_of_tendsto_atTop h_ant hL
    (le_isGLB_iff h_glb).mpr h_bdd_0
  exact ⟨⟨L, hL0⟩, NNReal.tendsto_coe.mp hL⟩
Convergence of Antitone Sequences in Nonnegative Reals
Informal description
For any antitone sequence $f \colon \mathbb{N} \to \mathbb{R}_{\geq 0}$, there exists a limit $r \in \mathbb{R}_{\geq 0}$ such that $f(n)$ converges to $r$ as $n \to \infty$.
NNReal.iSup_pow_of_ne_zero theorem
(hn : n ≠ 0) (f : ι → ℝ≥0) : (⨆ i, f i) ^ n = ⨆ i, f i ^ n
Full source 
lemma iSup_pow_of_ne_zero (hn : n ≠ 0) (f : ι → ℝ≥0) : (⨆ i, f i) ^ n = ⨆ i, f i ^ n :=
 (NNReal.powOrderIso n hn).map_ciSup' _
Supremum commutes with power for nonnegative reals when exponent is nonzero
Informal description
For any nonzero natural number $n$ and any family of nonnegative real numbers $(f_i)_{i \in \iota}$, the $n$-th power of the supremum of the family equals the supremum of the $n$-th powers of the family members, i.e., \[ \left( \sup_{i \in \iota} f_i \right)^n = \sup_{i \in \iota} (f_i^n). \]
NNReal.iSup_pow theorem
[Nonempty ι] (f : ι → ℝ≥0) (n : ℕ) : (⨆ i, f i) ^ n = ⨆ i, f i ^ n
Full source 
lemma iSup_pow [Nonempty ι] (f : ι → ℝ≥0) (n : ℕ) : (⨆ i, f i) ^ n = ⨆ i, f i ^ n := by
  by_cases hn : n = 0
  · simp [hn]
  · exact iSup_pow_of_ne_zero hn _
Supremum Commutes with Power for Nonnegative Reals
Informal description
For any nonempty index set $\iota$, any family of nonnegative real numbers $(f_i)_{i \in \iota}$, and any natural number $n$, the $n$-th power of the supremum of the family equals the supremum of the $n$-th powers of the family members, i.e., \[ \left( \sup_{i \in \iota} f_i \right)^n = \sup_{i \in \iota} (f_i^n). \]
ENNReal.powOrderIso definition
(n : ℕ) (hn : n ≠ 0) : ℝ≥0∞ ≃o ℝ≥0∞
Full source 
/-- `x ↦ x ^ n` as an order isomorphism of `ℝ≥0∞`.

See also `ENNReal.orderIsoRpow`. -/
def powOrderIso (n : ℕ) (hn : n ≠ 0) : ℝ≥0∞ℝ≥0∞ ≃o ℝ≥0∞ :=
  (NNReal.powOrderIso n hn).withTopCongr.copy (· ^ n) _
    (by cases n; (· cases hn rfl); · ext (_ | _) <;> rfl) rfl
Order isomorphism of \( x \mapsto x^n \) on extended nonnegative reals
Informal description
For any nonzero natural number \( n \), the function \( x \mapsto x^n \) is an order isomorphism on the extended nonnegative real numbers \( \mathbb{R}_{\geq 0} \cup \{\infty\} \). This means it is a bijective, strictly increasing function that preserves the order structure, and its inverse is also strictly increasing.
ENNReal.iSup_pow_of_ne_zero theorem
(hn : n ≠ 0) (f : ι → ℝ≥0∞) : (⨆ i, f i) ^ n = ⨆ i, f i ^ n
Full source 
lemma iSup_pow_of_ne_zero (hn : n ≠ 0) (f : ι → ℝ≥0∞) : (⨆ i, f i) ^ n = ⨆ i, f i ^ n :=
  (powOrderIso n hn).map_iSup _
Supremum Commutes with Power for Extended Nonnegative Reals (Nonzero Exponent)
Informal description
For any nonzero natural number $n$ and any family of extended nonnegative real numbers $(f_i)_{i \in \iota}$, the $n$-th power of the supremum of the family equals the supremum of the $n$-th powers of the family members, i.e., \[ \left( \sup_{i \in \iota} f_i \right)^n = \sup_{i \in \iota} (f_i^n). \]
ENNReal.iSup_pow theorem
[Nonempty ι] (f : ι → ℝ≥0∞) (n : ℕ) : (⨆ i, f i) ^ n = ⨆ i, f i ^ n
Full source 
lemma iSup_pow [Nonempty ι] (f : ι → ℝ≥0∞) (n : ℕ) : (⨆ i, f i) ^ n = ⨆ i, f i ^ n := by
  by_cases hn : n = 0
  · simp [hn]
  · exact iSup_pow_of_ne_zero hn _
Supremum Commutes with Power for Extended Nonnegative Reals
Informal description
For any nonempty index set $\iota$, any family of extended nonnegative real numbers $(f_i)_{i \in \iota}$, and any natural number $n$, the $n$-th power of the supremum of the family equals the supremum of the $n$-th powers of the family members, i.e., \[ \left( \sup_{i \in \iota} f_i \right)^n = \sup_{i \in \iota} (f_i^n). \]
Real.iSup_pow theorem
[Nonempty ι] {f : ι → ℝ} (hf : ∀ i, 0 ≤ f i) (n : ℕ) : (⨆ i, f i) ^ n = ⨆ i, f i ^ n
Full source 
lemma Real.iSup_pow [Nonempty ι] {f : ι → ℝ} (hf : ∀ i, 0 ≤ f i) (n : ℕ) :
    (⨆ i, f i) ^ n = ⨆ i, f i ^ n := by
  lift f to ι → ℝ≥0 using hf; dsimp; exact mod_cast NNReal.iSup_pow f n
Supremum Commutes with Power for Nonnegative Real Functions
Informal description
For any nonempty index set $\iota$, any family of nonnegative real numbers $(f_i)_{i \in \iota}$ (i.e., $f_i \geq 0$ for all $i \in \iota$), and any natural number $n$, the $n$-th power of the supremum of the family equals the supremum of the $n$-th powers of the family members, i.e., \[ \left( \sup_{i \in \iota} f_i \right)^n = \sup_{i \in \iota} (f_i^n). \]
Real.iSup_pow_of_ne_zero theorem
{f : ι → ℝ} (hf : ∀ i, 0 ≤ f i) (hn : n ≠ 0) : (⨆ i, f i) ^ n = ⨆ i, f i ^ n
Full source 
lemma Real.iSup_pow_of_ne_zero {f : ι → ℝ} (hf : ∀ i, 0 ≤ f i) (hn : n ≠ 0) :
    (⨆ i, f i) ^ n = ⨆ i, f i ^ n := by
  cases isEmpty_or_nonempty ι
  · simp [hn]
  · exact iSup_pow hf _
Supremum-Power Commutation for Nonnegative Reals with Nonzero Exponent
Informal description
For any family of nonnegative real numbers $(f_i)_{i \in \iota}$ (i.e., $f_i \geq 0$ for all $i \in \iota$) and any nonzero natural number $n$, the $n$-th power of the supremum of the family equals the supremum of the $n$-th powers of the family members, i.e., \[ \left( \sup_{i \in \iota} f_i \right)^n = \sup_{i \in \iota} (f_i^n). \]