mathlib3 documentation

topology.instances.nnreal

Topology on ℝ≥0 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

@[protected, instance]

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

Equations
@[simp, norm_cast]
theorem nnreal.tendsto_coe {α : Type u_1} {f : filter α} {m : α nnreal} {x : nnreal} :
filter.tendsto (λ (a : α), (m a)) f (nhds x) filter.tendsto m f (nhds x)
theorem nnreal.tendsto_coe' {α : Type u_1} {f : filter α} [f.ne_bot] {m : α nnreal} {x : } :
filter.tendsto (λ (a : α), (m a)) f (nhds x) (hx : 0 x), filter.tendsto m f (nhds x, hx⟩)
@[simp, norm_cast]
theorem nnreal.tendsto_coe_at_top {α : Type u_1} {f : filter α} {m : α nnreal} :
theorem tendsto_real_to_nnreal {α : Type u_1} {f : filter α} {m : α } {x : } (h : filter.tendsto m f (nhds x)) :
filter.tendsto (λ (a : α), (m a).to_nnreal) f (nhds x.to_nnreal)
theorem nnreal.nhds_zero  :
nhds 0 = (a : nnreal) (H : a 0), filter.principal (set.Iio a)
theorem nnreal.nhds_zero_basis  :
(nhds 0).has_basis (λ (a : nnreal), 0 < a) (λ (a : nnreal), set.Iio a)
@[norm_cast]
theorem nnreal.has_sum_coe {α : Type u_1} {f : α nnreal} {r : nnreal} :
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 : α nnreal} :
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 : α 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 : summable f) {i : β α} (hi : function.injective i) :
theorem nnreal.summable_nat_add (f : nnreal) (hf : summable f) (k : ) :
summable (λ (i : ), f (i + k))
theorem nnreal.summable_nat_add_iff {f : nnreal} (k : ) :
summable (λ (i : ), f (i + k)) summable f
theorem nnreal.has_sum_nat_add_iff {f : nnreal} (k : ) {a : nnreal} :
has_sum (λ (n : ), f (n + k)) a has_sum f (a + (finset.range k).sum (λ (i : ), f i))
theorem nnreal.sum_add_tsum_nat_add {f : nnreal} (k : ) (hf : summable f) :
∑' (i : ), f i = (finset.range k).sum (λ (i : ), 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 : nnreal) (h : 0 < n), f n
theorem nnreal.tendsto_tsum_compl_at_top_zero {α : Type u_1} (f : α nnreal) :
filter.tendsto (λ (s : finset α), ∑' (b : {x // x s}), f b) filter.at_top (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.

noncomputable def nnreal.pow_order_iso (n : ) (hn : n 0) :

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

Equations