mathlib documentation

topology.instances.nnreal

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:

topological_space ℝ≥0
topological_semiring ℝ≥0
second_countable_topology ℝ≥0
order_topology ℝ≥0
has_continuous_sub ℝ≥0
has_continuous_inv₀ ℝ≥0 (continuity of x⁻¹ away from 0)
has_continuous_smul ℝ≥0 ℝ

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} : tendsto (λa, (m a : ℝ)) f (𝓝 (x : ℝ)) ↔ 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.

@[protected, instance]

noncomputable def nnreal.topological_space :

topological_space ℝ≥0

Equations

nnreal.topological_space = infer_instance

@[protected, instance]

def nnreal.topological_semiring :

topological_semiring ℝ≥0

@[protected, instance]

def nnreal.topological_space.second_countable_topology :

topological_space.second_countable_topology ℝ≥0

@[protected, instance]

def nnreal.order_topology :

order_topology ℝ≥0

theorem continuous_real_to_nnreal :

continuous real.to_nnreal

theorem nnreal.continuous_coe :

@[simp, norm_cast]

theorem nnreal.tendsto_coe {α : Type u_1} {f : filter α} {m : α → ℝ≥0} {x : ℝ≥0} :

filter.tendsto (λ (a : α), ↑(m a)) f (𝓝 ↑x) ↔ filter.tendsto m f (𝓝 x)

theorem nnreal.tendsto_coe' {α : Type u_1} {f : filter α} [f.ne_bot] {m : α → ℝ≥0} {x : ℝ} :

filter.tendsto (λ (a : α), ↑(m a)) f (𝓝 x) ↔ ∃ (hx : 0 ≤ x), filter.tendsto m f (𝓝 ⟨x, hx⟩)

@[simp]

theorem nnreal.map_coe_at_top :

filter.map coe filter.at_top = filter.at_top

theorem nnreal.comap_coe_at_top :

filter.comap coe filter.at_top = filter.at_top

@[simp, norm_cast]

theorem nnreal.tendsto_coe_at_top {α : Type u_1} {f : filter α} {m : α → ℝ≥0} :

filter.tendsto (λ (a : α), ↑(m a)) f filter.at_top ↔ filter.tendsto m f filter.at_top

theorem nnreal.tendsto_real_to_nnreal {α : Type u_1} {f : filter α} {m : α → ℝ} {x : ℝ} (h : filter.tendsto m f (𝓝 x)) :

filter.tendsto (λ (a : α), (m a).to_nnreal) f (𝓝 x.to_nnreal)

theorem nnreal.nhds_zero :

𝓝 0 = ⨅ (a : ℝ≥0) (H : a ≠ 0), 𝓟 (set.Iio a)

theorem nnreal.nhds_zero_basis :

(𝓝 0).has_basis (λ (a : ℝ≥0), 0 < a) (λ (a : ℝ≥0), set.Iio a)

@[protected, instance]

def nnreal.has_continuous_sub :

has_continuous_sub ℝ≥0

@[protected, instance]

def nnreal.has_continuous_inv₀ :

has_continuous_inv₀ ℝ≥0

@[protected, instance]

def nnreal.real.has_continuous_smul :

has_continuous_smul ℝ≥0 ℝ

@[norm_cast]

theorem nnreal.has_sum_coe {α : Type u_1} {f : α → ℝ≥0} {r : ℝ≥0} :

has_sum (λ (a : α), ↑(f a)) ↑r ↔ has_sum f r

theorem nnreal.has_sum_real_to_nnreal_of_nonneg {α : Type u_1} {f : α → ℝ} (hf_nonneg : ∀ (n : α), 0 ≤ f n) (hf : summable f) :

has_sum (λ (n : α), (f n).to_nnreal) (∑' (n : α), f n).to_nnreal

@[norm_cast]

theorem nnreal.summable_coe {α : Type u_1} {f : α → ℝ≥0} :

summable (λ (a : α), ↑(f a)) ↔ summable f

theorem nnreal.summable_coe_of_nonneg {α : Type u_1} {f : α → ℝ} (hf₁ : ∀ (n : α), 0 ≤ f n) :

summable (λ (n : α), ⟨f n, _⟩) ↔ summable f

@[norm_cast]

theorem nnreal.coe_tsum {α : Type u_1} {f : α → ℝ≥0} :

↑∑' (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 : ℝ≥0) (f : α → ℝ≥0) :

∑' (x : α), a * f x = a * ∑' (x : α), f x

theorem nnreal.tsum_mul_right {α : Type u_1} (f : α → ℝ≥0) (a : ℝ≥0) :

∑' (x : α), (f x) * a = (∑' (x : α), f x) * a

theorem nnreal.summable_comp_injective {α : Type u_1} {β : Type u_2} {f : α → ℝ≥0} (hf : summable f) {i : β → α} (hi : function.injective i) :

summable (f ∘ i)

theorem nnreal.summable_nat_add (f : ℕ → ℝ≥0) (hf : summable f) (k : ℕ) :

summable (λ (i : ℕ), f (i + k))

theorem nnreal.summable_nat_add_iff {f : ℕ → ℝ≥0} (k : ℕ) :

summable (λ (i : ℕ), f (i + k)) ↔ summable f

theorem nnreal.has_sum_nat_add_iff {f : ℕ → ℝ≥0} (k : ℕ) {a : ℝ≥0} :

has_sum (λ (n : ℕ), f (n + k)) a ↔ has_sum f (a + ∑ (i : ℕ) in finset.range k, f i)

theorem nnreal.sum_add_tsum_nat_add {f : ℕ → ℝ≥0} (k : ℕ) (hf : summable f) :

∑' (i : ℕ), f i = ∑ (i : ℕ) in finset.range k, f i + ∑' (i : ℕ), f (i + k)

theorem nnreal.infi_real_pos_eq_infi_nnreal_pos {α : Type u_1} [complete_lattice α] {f : ℝ → α} :

(⨅ (n : ℝ) (h : 0 < n), f n) = ⨅ (n : ℝ≥0) (h : 0 < n), f ↑n

theorem nnreal.tendsto_cofinite_zero_of_summable {α : Type u_1} {f : α → ℝ≥0} (hf : summable f) :

filter.tendsto f filter.cofinite (𝓝 0)

theorem nnreal.tendsto_at_top_zero_of_summable {f : ℕ → ℝ≥0} (hf : summable f) :

filter.tendsto f filter.at_top (𝓝 0)

theorem nnreal.tendsto_tsum_compl_at_top_zero {α : Type u_1} (f : α → ℝ≥0) :

filter.tendsto (λ (s : finset α), ∑' (b : {x // x ∉ s}), f ↑b) filter.at_top (𝓝 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.