# Topology on ℝ≥0#

The natural topology on ℝ≥0 (the one induced from ℝ), and a basic API.

## Main definitions #

Instances for the following typeclasses are defined:

• TopologicalSpace ℝ≥0
• TopologicalSemiring ℝ≥0
• SecondCountableTopology ℝ≥0
• OrderTopology ℝ≥0
• ProperSpace ℝ≥0
• ContinuousSub ℝ≥0
• HasContinuousInv₀ ℝ≥0 (continuity of x⁻¹ away from 0)
• ContinuousSMul ℝ≥0 α (whenever α has a continuous MulAction ℝ α)

Everything is inherited from the corresponding structures on the reals.

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

Equations
Equations
Equations
Equations
Equations
@[simp]
noncomputable def ContinuousMap.realToNNReal :

Real.toNNReal bundled as a continuous map for convenience.

Equations
Instances For
@[simp]

Embedding of ℝ≥0 to ℝ as a bundled continuous map.

Equations
Instances For
instance NNReal.ContinuousMap.canLift {X : Type u_2} [] :
CanLift fun (f : ) => ∀ (x : X), 0 f x
Equations
• =
@[simp]
theorem NNReal.tendsto_coe {α : Type u_1} {f : } {m : αNNReal} {x : NNReal} :
Filter.Tendsto (fun (a : α) => (m a)) f (nhds x) Filter.Tendsto m f (nhds x)
theorem NNReal.tendsto_coe' {α : Type u_1} {f : } [f.NeBot] {m : αNNReal} {x : } :
Filter.Tendsto (fun (a : α) => (m a)) f (nhds x) ∃ (hx : 0 x), Filter.Tendsto m f (nhds x, hx)
@[simp]
theorem NNReal.map_coe_atTop :
Filter.map NNReal.toReal Filter.atTop = Filter.atTop
@[simp]
theorem NNReal.comap_coe_atTop :
Filter.comap NNReal.toReal Filter.atTop = Filter.atTop
@[simp]
theorem NNReal.tendsto_coe_atTop {α : Type u_1} {f : } {m : αNNReal} :
Filter.Tendsto (fun (a : α) => (m a)) f Filter.atTop Filter.Tendsto m f Filter.atTop
theorem tendsto_real_toNNReal {α : Type u_1} {f : } {m : α} {x : } (h : Filter.Tendsto m f (nhds x)) :
Filter.Tendsto (fun (a : α) => (m a).toNNReal) f (nhds x.toNNReal)
@[simp]
theorem Real.map_toNNReal_atTop :
Filter.map Real.toNNReal Filter.atTop = Filter.atTop
@[simp]
theorem Real.comap_toNNReal_atTop :
Filter.comap Real.toNNReal Filter.atTop = Filter.atTop
@[simp]
theorem Real.tendsto_toNNReal_atTop_iff {α : Type u_1} {l : } {f : α} :
Filter.Tendsto (fun (x : α) => (f x).toNNReal) l Filter.atTop Filter.Tendsto f l Filter.atTop
theorem NNReal.nhds_zero :
nhds 0 = ⨅ (a : NNReal), ⨅ (_ : a 0),
theorem NNReal.nhds_zero_basis :
(nhds 0).HasBasis (fun (a : NNReal) => 0 < a) fun (a : NNReal) =>
Equations
Equations
instance NNReal.instContinuousSMulOfReal {α : Type u_1} [] [] [] :
Equations
• =
theorem NNReal.hasSum_coe {α : Type u_1} {f : αNNReal} {r : NNReal} :
HasSum (fun (a : α) => (f a)) r HasSum f r
theorem HasSum.toNNReal {α : Type u_1} {f : α} {y : } (hf₀ : ∀ (n : α), 0 f n) (hy : HasSum f y) :
HasSum (fun (x : α) => (f x).toNNReal) y.toNNReal
theorem NNReal.hasSum_real_toNNReal_of_nonneg {α : Type u_1} {f : α} (hf_nonneg : ∀ (n : α), 0 f n) (hf : ) :
HasSum (fun (n : α) => (f n).toNNReal) (∑' (n : α), f n).toNNReal
theorem NNReal.summable_coe {α : Type u_1} {f : αNNReal} :
(Summable fun (a : α) => (f a))
theorem NNReal.summable_mk {α : Type u_1} {f : α} (hf : ∀ (n : α), 0 f n) :
(Summable fun (n : α) => f n, )
theorem NNReal.coe_tsum {α : Type u_1} {f : αNNReal} :
(∑' (a : α), f a) = ∑' (a : α), (f a)
theorem NNReal.coe_tsum_of_nonneg {α : Type u_1} {f : α} (hf₁ : ∀ (n : α), 0 f n) :
∑' (n : α), f n, = ∑' (n : α), f n,
theorem NNReal.tsum_mul_left {α : Type u_1} (a : NNReal) (f : αNNReal) :
∑' (x : α), a * f x = a * ∑' (x : α), f x
theorem NNReal.tsum_mul_right {α : Type u_1} (f : αNNReal) (a : NNReal) :
∑' (x : α), f x * a = (∑' (x : α), f x) * a
theorem NNReal.summable_comp_injective {α : Type u_1} {β : Type u_2} {f : αNNReal} (hf : ) {i : βα} (hi : ) :
theorem NNReal.summable_nat_add (f : ) (hf : ) (k : ) :
Summable fun (i : ) => f (i + k)
theorem NNReal.summable_nat_add_iff {f : } (k : ) :
(Summable fun (i : ) => f (i + k))
theorem NNReal.hasSum_nat_add_iff {f : } (k : ) {a : NNReal} :
HasSum (fun (n : ) => f (n + k)) a HasSum f (a + i, f i)
theorem NNReal.sum_add_tsum_nat_add {f : } (k : ) (hf : ) :
∑' (i : ), f i = i, f i + ∑' (i : ), f (i + k)
theorem NNReal.iInf_real_pos_eq_iInf_nnreal_pos {α : Type u_1} [] {f : α} :
⨅ (n : ), ⨅ (_ : 0 < n), f n = ⨅ (n : NNReal), ⨅ (_ : 0 < n), f n
theorem NNReal.tendsto_cofinite_zero_of_summable {α : Type u_1} {f : αNNReal} (hf : ) :
Filter.Tendsto f Filter.cofinite (nhds 0)
theorem NNReal.tendsto_atTop_zero_of_summable {f : } (hf : ) :
Filter.Tendsto f Filter.atTop (nhds 0)
theorem NNReal.tendsto_tsum_compl_atTop_zero {α : Type u_1} (f : αNNReal) :
Filter.Tendsto (fun (s : ) => ∑' (b : { x : α // xs }), 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.

def NNReal.powOrderIso (n : ) (hn : n 0) :

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

Equations
Instances For
theorem Real.tendsto_of_bddAbove_monotone {f : } (h_bdd : ) (h_mon : ) :
∃ (r : ), Filter.Tendsto f Filter.atTop (nhds r)

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

theorem Real.tendsto_of_bddBelow_antitone {f : } (h_bdd : ) (h_ant : ) :
∃ (r : ), Filter.Tendsto f Filter.atTop (nhds r)

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

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

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

Equations