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:

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

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

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.

@[simp]
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.tendsto_coe_at_top {α : Type u_1} {f : filter α} {m : α → ℝ≥0} :
theorem nnreal.tendsto_of_real {α : 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)
@[instance]
Equations
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_of_real_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
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
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) :
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) :
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.