mathlibdocumentation

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

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

Equations
@[simp]
@[protected, instance]
noncomputable def nnreal.continuous_map.can_lift {X : Type u_1}  :
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 nnreal.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]
@[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.