Topology on ℝ≥0 #
The basic lemmas for the natural topology on ℝ≥0 .
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} : Filter.Tendsto (fun a, (m a : ℝ)) f (𝓝 (x : ℝ)) ↔ Filter.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.
Real.toNNReal bundled as a continuous map for convenience.
Instances For
@[simp]
@[simp]
theorem
ContinuousOn.ofReal_map_toNNReal
{f : NNReal → NNReal}
{s : Set ℝ}
{t : Set NNReal}
(hf : ContinuousOn f t)
(h : Set.MapsTo Real.toNNReal s t)
:
ContinuousOn (fun (x : ℝ) => ↑(f x.toNNReal)) s
@[simp]
theorem
NNReal.tendsto_coe'
{α : Type u_2}
{f : Filter α}
[f.NeBot]
{m : α → NNReal}
{x : ℝ}
:
Filter.Tendsto (fun (a : α) => ↑(m a)) f (nhds x) ↔ ∃ (hx : 0 ≤ x), Filter.Tendsto m f (nhds ⟨x, hx⟩)
@[simp]
theorem
tendsto_real_toNNReal
{α : Type u_2}
{f : Filter α}
{m : α → ℝ}
{x : ℝ}
(h : Filter.Tendsto m f (nhds x))
:
Filter.Tendsto (fun (a : α) => (m a).toNNReal) f (nhds x.toNNReal)
@[simp]
theorem
NNReal.summable_comp_injective
{α : Type u_2}
{β : Type u_3}
{f : α → NNReal}
(hf : Summable f)
{i : β → α}
(hi : Function.Injective i)
:
theorem
NNReal.tendsto_cofinite_zero_of_summable
{α : Type u_3}
{f : α → NNReal}
(hf : Summable f)
:
theorem
NNReal.tendsto_atTop_zero_of_summable
{f : ℕ → NNReal}
(hf : Summable f)
:
Filter.Tendsto f Filter.atTop (nhds 0)
theorem
NNReal.tendsto_tsum_compl_atTop_zero
{α : Type u_3}
(f : α → NNReal)
:
Filter.Tendsto (fun (s : Finset α) => ∑' (b : { x : α // x ∉ s }), f ↑b) Filter.atTop (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.