Documentation

Mathlib.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.

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

Equations
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem NNReal.tendsto_coe {α : Type u_1} {f : Filter α} {m : αNNReal} {x : NNReal} :
    Filter.Tendsto (fun (a : α) => (m a)) f (nhds x) Filter.Tendsto m f (nhds x)
    theorem NNReal.tendsto_coe' {α : Type u_1} {f : Filter α} [Filter.NeBot f] {m : αNNReal} {x : } :
    Filter.Tendsto (fun (a : α) => (m a)) f (nhds x) ∃ (hx : 0 x), Filter.Tendsto m f (nhds { val := x, property := hx })
    @[simp]
    theorem NNReal.map_coe_atTop :
    Filter.map NNReal.toReal Filter.atTop = Filter.atTop
    theorem NNReal.comap_coe_atTop :
    Filter.comap NNReal.toReal Filter.atTop = Filter.atTop
    @[simp]
    theorem NNReal.tendsto_coe_atTop {α : Type u_1} {f : Filter α} {m : αNNReal} :
    Filter.Tendsto (fun (a : α) => (m a)) f Filter.atTop Filter.Tendsto m f Filter.atTop
    theorem tendsto_real_toNNReal {α : Type u_1} {f : Filter α} {m : α} {x : } (h : Filter.Tendsto m f (nhds x)) :
    Filter.Tendsto (fun (a : α) => Real.toNNReal (m a)) f (nhds (Real.toNNReal x))
    theorem NNReal.nhds_zero :
    nhds 0 = ⨅ (a : NNReal), ⨅ (_ : a 0), Filter.principal (Set.Iio a)
    theorem NNReal.nhds_zero_basis :
    Filter.HasBasis (nhds 0) (fun (a : NNReal) => 0 < a) fun (a : NNReal) => Set.Iio a
    theorem NNReal.hasSum_coe {α : Type u_1} {f : αNNReal} {r : NNReal} :
    HasSum (fun (a : α) => (f a)) r HasSum f r
    theorem HasSum.toNNReal {α : Type u_1} {f : α} {y : } (hf₀ : ∀ (n : α), 0 f n) (hy : HasSum f y) :
    HasSum (fun (x : α) => Real.toNNReal (f x)) (Real.toNNReal y)
    theorem NNReal.hasSum_real_toNNReal_of_nonneg {α : Type u_1} {f : α} (hf_nonneg : ∀ (n : α), 0 f n) (hf : Summable f) :
    HasSum (fun (n : α) => Real.toNNReal (f n)) (Real.toNNReal (∑' (n : α), f n))
    theorem NNReal.summable_coe {α : Type u_1} {f : αNNReal} :
    (Summable fun (a : α) => (f a)) Summable f
    theorem NNReal.summable_mk {α : Type u_1} {f : α} (hf : ∀ (n : α), 0 f n) :
    (Summable fun (n : α) => { val := f n, property := (_ : 0 f n) }) Summable f
    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) :
    { val := ∑' (n : α), f n, property := (_ : 0 ∑' (i : α), f i) } = ∑' (n : α), { val := f n, property := (_ : 0 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 fun (i : ) => f (i + k)
    theorem NNReal.summable_nat_add_iff {f : NNReal} (k : ) :
    (Summable fun (i : ) => f (i + k)) Summable f
    theorem NNReal.hasSum_nat_add_iff {f : NNReal} (k : ) {a : NNReal} :
    HasSum (fun (n : ) => f (n + k)) a HasSum f (a + Finset.sum (Finset.range k) fun (i : ) => f i)
    theorem NNReal.sum_add_tsum_nat_add {f : NNReal} (k : ) (hf : Summable f) :
    ∑' (i : ), f i = (Finset.sum (Finset.range k) fun (i : ) => f i) + ∑' (i : ), f (i + k)
    theorem NNReal.iInf_real_pos_eq_iInf_nnreal_pos {α : Type u_1} [CompleteLattice α] {f : α} :
    ⨅ (n : ), ⨅ (_ : 0 < n), f n = ⨅ (n : NNReal), ⨅ (_ : 0 < n), f n
    theorem NNReal.tendsto_cofinite_zero_of_summable {α : Type u_1} {f : αNNReal} (hf : Summable f) :
    Filter.Tendsto f Filter.cofinite (nhds 0)
    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_1} (f : αNNReal) :
    Filter.Tendsto (fun (s : Finset α) => ∑' (b : { x : α // xs }), 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.

    def NNReal.powOrderIso (n : ) (hn : n 0) :

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For