mathlib3documentation

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:

• 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 α (whenever α has a continuous mul_action ℝ α)

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]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]

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

Equations
@[simp]
@[protected, instance]
def nnreal.continuous_map.can_lift {X : Type u_1}  :
(λ (f : C(X, )), (x : X), 0 f x)
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) (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), (nhds x, hx⟩)
@[simp]
@[simp, norm_cast]
theorem nnreal.tendsto_coe_at_top {α : Type u_1} {f : filter α} {m : α nnreal} :
filter.tendsto (λ (a : α), (m a)) f filter.at_top
theorem tendsto_real_to_nnreal {α : Type u_1} {f : filter α} {m : α } {x : } (h : (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),
theorem nnreal.nhds_zero_basis  :
(nhds 0).has_basis (λ (a : nnreal), 0 < a) (λ (a : nnreal), set.Iio a)
@[protected, instance]
@[protected, instance]
@[protected, instance]
def nnreal.has_continuous_smul {α : Type u_1} [ α]  :
@[norm_cast]
theorem nnreal.has_sum_coe {α : Type u_1} {f : α nnreal} {r : nnreal} :
has_sum (λ (a : α), (f a)) r 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))
theorem nnreal.summable_coe_of_nonneg {α : Type u_1} {f : α } (hf₁ : (n : α), 0 f n) :
summable (λ (n : α), f n, _⟩)
@[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))
theorem nnreal.has_sum_nat_add_iff {f : nnreal} (k : ) {a : nnreal} :
has_sum (λ (n : ), f (n + k)) a (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} {f : α} :
( (n : ) (h : 0 < n), f n) = (n : nnreal) (h : 0 < n), f n
theorem nnreal.tendsto_cofinite_zero_of_summable {α : Type u_1} {f : α nnreal} (hf : summable f) :
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