# 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.

source
theorem NNReal.isOpen_Ico_zero {x : NNReal} :
IsOpen (Set.Ico 0 x)
source
theorem continuous_real_toNNReal :
Continuous Real.toNNReal
source
noncomputable def ContinuousMap.realToNNReal :
C(ℝ, NNReal)

`Real.toNNReal` bundled as a continuous map for convenience.

Equations

- ContinuousMap.realToNNReal = { toFun := Real.toNNReal, continuous_toFun := continuous_real_toNNReal }

Instances For

source
@[simp]
theorem ContinuousMap.realToNNReal_apply :
⇑realToNNReal = Real.toNNReal
source
theorem ContinuousOn.ofReal_map_toNNReal {f : NNReal → NNReal} {s : Set ℝ} {t : Set NNReal} (hf : ContinuousOn f t) (h : Set.MapsTo Real.toNNReal s t) :
ContinuousOn (fun (x : ℝ) => ↑(f x.toNNReal)) s
source
@[simp]
theorem NNReal.tendsto_coe {α : Type u_2} {f : Filter α} {m : α → NNReal} {x : NNReal} :
Filter.Tendsto (fun (a : α) => ↑(m a)) f (nhds ↑x) ↔ Filter.Tendsto m f (nhds x)
source
theorem NNReal.tendsto_coe' {α : Type u_2} {f : Filter α} [f.NeBot] {m : α → NNReal} {x : ℝ} :
Filter.Tendsto (fun (a : α) => ↑(m a)) f (nhds x) ↔ ∃ (hx : 0 ≤ x), Filter.Tendsto m f (nhds ⟨x, hx⟩)
source
@[simp]
theorem NNReal.map_coe_atTop :
Filter.map toReal Filter.atTop = Filter.atTop
source
@[simp]
theorem NNReal.comap_coe_atTop :
Filter.comap toReal Filter.atTop = Filter.atTop
source
@[simp]
theorem NNReal.tendsto_coe_atTop {α : Type u_2} {f : Filter α} {m : α → NNReal} :
Filter.Tendsto (fun (a : α) => ↑(m a)) f Filter.atTop ↔ Filter.Tendsto m f Filter.atTop
source
theorem tendsto_real_toNNReal {α : Type u_2} {f : Filter α} {m : α → ℝ} {x : ℝ} (h : Filter.Tendsto m f (nhds x)) :
Filter.Tendsto (fun (a : α) => (m a).toNNReal) f (nhds x.toNNReal)
source
@[simp]
theorem Real.map_toNNReal_atTop :
Filter.map toNNReal Filter.atTop = Filter.atTop
source
theorem tendsto_real_toNNReal_atTop :
Filter.Tendsto Real.toNNReal Filter.atTop Filter.atTop
source
@[simp]
theorem Real.comap_toNNReal_atTop :
Filter.comap toNNReal Filter.atTop = Filter.atTop
source
@[simp]
theorem Real.tendsto_toNNReal_atTop_iff {α : Type u_2} {l : Filter α} {f : α → ℝ} :
Filter.Tendsto (fun (x : α) => (f x).toNNReal) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop
source
theorem Real.tendsto_toNNReal_atTop :
Filter.Tendsto toNNReal Filter.atTop Filter.atTop
source
theorem NNReal.nhds_zero :
nhds 0 = ⨅ (a : NNReal), ⨅ (_ : a ≠ 0), Filter.principal (Set.Iio a)
source
theorem NNReal.nhds_zero_basis :
(nhds 0).HasBasis (fun (a : NNReal) => 0 < a) fun (a : NNReal) => Set.Iio a
source
theorem NNReal.hasSum_coe {α : Type u_2} {L : SummationFilter α} {f : α → NNReal} {r : NNReal} :
HasSum (fun (a : α) => ↑(f a)) (↑r) L ↔ HasSum f r L
source
theorem HasSum.toNNReal {α : Type u_2} {L : SummationFilter α} {f : α → ℝ} {y : ℝ} (hf₀ : ∀ (n : α), 0 ≤ f n) (hy : HasSum f y L) :
HasSum (fun (x : α) => (f x).toNNReal) y.toNNReal L
source
theorem NNReal.hasSum_real_toNNReal_of_nonneg {α : Type u_2} {L : SummationFilter α} {f : α → ℝ} (hf_nonneg : ∀ (n : α), 0 ≤ f n) (hf : Summable f L) :
HasSum (fun (n : α) => (f n).toNNReal) (∑'[L] (n : α), f n).toNNReal L
source
theorem NNReal.summable_coe {α : Type u_2} {L : SummationFilter α} {f : α → NNReal} :
Summable (fun (a : α) => ↑(f a)) L ↔ Summable f L
source
theorem NNReal.summable_mk {α : Type u_2} {L : SummationFilter α} {f : α → ℝ} (hf : ∀ (n : α), 0 ≤ f n) :
Summable (fun (n : α) => ⟨f n, ⋯⟩) L ↔ Summable f L
source
theorem NNReal.coe_tsum {α : Type u_2} {L : SummationFilter α} {f : α → NNReal} :
↑(∑'[L] (a : α), f a) = ∑'[L] (a : α), ↑(f a)
source
theorem NNReal.coe_tsum_of_nonneg {α : Type u_2} {L : SummationFilter α} {f : α → ℝ} (hf₁ : ∀ (n : α), 0 ≤ f n) :
⟨∑'[L] (n : α), f n, ⋯⟩ = ∑'[L] (n : α), ⟨f n, ⋯⟩
source
theorem NNReal.tsum_mul_left {α : Type u_2} {L : SummationFilter α} (a : NNReal) (f : α → NNReal) :
∑'[L] (x : α), a * f x = a * ∑'[L] (x : α), f x
source
theorem NNReal.tsum_mul_right {α : Type u_2} {L : SummationFilter α} (f : α → NNReal) (a : NNReal) :
∑'[L] (x : α), f x * a = (∑'[L] (x : α), f x) * a
source
theorem NNReal.summable_comp_injective {α : Type u_2} {β : Type u_3} {f : α → NNReal} (hf : Summable f) {i : β → α} (hi : Function.Injective i) :
Summable (f ∘ i)
source
theorem NNReal.summable_nat_add (f : ℕ → NNReal) (hf : Summable f) (k : ℕ) :
Summable fun (i : ℕ) => f (i + k)
source
theorem NNReal.summable_nat_add_iff {f : ℕ → NNReal} (k : ℕ) :
(Summable fun (i : ℕ) => f (i + k)) ↔ Summable f
source
theorem NNReal.hasSum_nat_add_iff {f : ℕ → NNReal} (k : ℕ) {a : NNReal} :
HasSum (fun (n : ℕ) => f (n + k)) a ↔ HasSum f (a + ∑ i ∈ Finset.range k, f i)
source
theorem NNReal.sum_add_tsum_nat_add {f : ℕ → NNReal} (k : ℕ) (hf : Summable f) :
∑' (i : ℕ), f i = ∑ i ∈ Finset.range k, f i + ∑' (i : ℕ), f (i + k)
source
theorem NNReal.iInf_real_pos_eq_iInf_nnreal_pos {α : Type u_2} [CompleteLattice α] {f : ℝ → α} :
⨅ (n : ℝ), ⨅ (_ : 0 < n), f n = ⨅ (n : NNReal), ⨅ (_ : 0 < n), f ↑n
source
theorem NNReal.tendsto_cofinite_zero_of_summable {α : Type u_3} {f : α → NNReal} (hf : Summable f) :
Filter.Tendsto f Filter.cofinite (nhds 0)
source
theorem NNReal.tendsto_atTop_zero_of_summable {f : ℕ → NNReal} (hf : Summable f) :
Filter.Tendsto f Filter.atTop (nhds 0)
source
theorem NNReal.tendsto_tsum_compl_atTop_zero {α : Type u_3} (f : α → NNReal) :
Filter.Tendsto (fun (s : Finset α) => ∑' (b : { x : α // x ∉ s }), f ↑b) Filter.atTop (nhds 0)

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.

source
def NNReal.powOrderIso (n : ℕ) (hn : n ≠ 0) :
NNReal ≃o NNReal

`x ↦ x ^ n` as an order isomorphism of `ℝ≥0`.

Equations

- NNReal.powOrderIso n hn = StrictMono.orderIsoOfSurjective (fun (x : NNReal) => x ^ n) ⋯ ⋯

Instances For

source
theorem Real.tendsto_of_bddAbove_monotone {f : ℕ → ℝ} (h_bdd : BddAbove (Set.range f)) (h_mon : Monotone f) :
∃ (r : ℝ), Filter.Tendsto f Filter.atTop (nhds r)

A monotone, bounded above sequence `f : ℕ → ℝ` has a finite limit.

source
theorem Real.tendsto_of_bddBelow_antitone {f : ℕ → ℝ} (h_bdd : BddBelow (Set.range f)) (h_ant : Antitone f) :
∃ (r : ℝ), Filter.Tendsto f Filter.atTop (nhds r)

An antitone, bounded below sequence `f : ℕ → ℝ` has a finite limit.

source
theorem NNReal.tendsto_of_antitone {f : ℕ → NNReal} (h_ant : Antitone f) :
∃ (r : NNReal), Filter.Tendsto f Filter.atTop (nhds r)

An antitone sequence `f : ℕ → ℝ≥0` has a finite limit.

source
theorem NNReal.iSup_pow_of_ne_zero {ι : Sort u_1} {n : ℕ} (hn : n ≠ 0) (f : ι → NNReal) :
(⨆ (i : ι), f i) ^ n = ⨆ (i : ι), f i ^ n
source
theorem NNReal.iSup_pow {ι : Sort u_1} [Nonempty ι] (f : ι → NNReal) (n : ℕ) :
(⨆ (i : ι), f i) ^ n = ⨆ (i : ι), f i ^ n
source
def ENNReal.powOrderIso (n : ℕ) (hn : n ≠ 0) :
ENNReal ≃o ENNReal

`x ↦ x ^ n` as an order isomorphism of `ℝ≥0∞`.

See also `ENNReal.orderIsoRpow`.

Equations

- ENNReal.powOrderIso n hn = RelIso.copy (NNReal.powOrderIso n hn).withTopCongr (fun (x : WithTop NNReal) => x ^ n) ⇑(RelIso.symm (NNReal.powOrderIso n hn).withTopCongr) ⋯ ⋯

Instances For

source
theorem ENNReal.iSup_pow_of_ne_zero {ι : Sort u_1} {n : ℕ} (hn : n ≠ 0) (f : ι → ENNReal) :
(⨆ (i : ι), f i) ^ n = ⨆ (i : ι), f i ^ n
source
theorem ENNReal.iSup_pow {ι : Sort u_1} [Nonempty ι] (f : ι → ENNReal) (n : ℕ) :
(⨆ (i : ι), f i) ^ n = ⨆ (i : ι), f i ^ n
source
theorem ENNReal.iSup₂_pow_of_ne_zero {ι : Sort u_1} {κ : ι → Sort u_2} (f : (i : ι) → κ i → ENNReal) {n : ℕ} (hn : n ≠ 0) :
(⨆ (i : ι), ⨆ (j : κ i), f i j) ^ n = ⨆ (i : ι), ⨆ (j : κ i), f i j ^ n
source
theorem Real.iSup_pow {ι : Sort u_1} [Nonempty ι] {f : ι → ℝ} (hf : ∀ (i : ι), 0 ≤ f i) (n : ℕ) :
(⨆ (i : ι), f i) ^ n = ⨆ (i : ι), f i ^ n
source
theorem Real.iSup_pow_of_ne_zero {ι : Sort u_1} {n : ℕ} {f : ι → ℝ} (hf : ∀ (i : ι), 0 ≤ f i) (hn : n ≠ 0) :
(⨆ (i : ι), f i) ^ n = ⨆ (i : ι), f i ^ n