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:

TopologicalSpace ℝ≥0
TopologicalSemiring ℝ≥0
SecondCountableTopology ℝ≥0
OrderTopology ℝ≥0
ContinuousSub ℝ≥0
HasContinuousInv₀ ℝ≥0 (continuity of x⁻¹ away from 0)
ContinuousSMul ℝ≥0 α (whenever α has a continuous MulAction ℝ α)

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} : 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.

instance NNReal.instTopologicalSpaceNNReal :

TopologicalSpace NNReal

Equations

NNReal.instTopologicalSpaceNNReal = inferInstance

instance NNReal.instTopologicalSemiringNNRealInstTopologicalSpaceNNRealToNonUnitalNonAssocSemiringToNonAssocSemiringInstNNRealSemiring :

TopologicalSemiring NNReal

Equations

NNReal.instTopologicalSemiringNNRealInstTopologicalSpaceNNRealToNonUnitalNonAssocSemiringToNonAssocSemiringInstNNRealSemiring = ⋯

instance NNReal.instSecondCountableTopologyNNRealInstTopologicalSpaceNNReal :

SecondCountableTopology NNReal

Equations

NNReal.instSecondCountableTopologyNNRealInstTopologicalSpaceNNReal = ⋯

instance NNReal.instOrderTopologyNNRealInstTopologicalSpaceNNRealToPreorderToPartialOrderInstNNRealStrictOrderedSemiring :

OrderTopology NNReal

Equations

NNReal.instOrderTopologyNNRealInstTopologicalSpaceNNRealToPreorderToPartialOrderInstNNRealStrictOrderedSemiring = ⋯

instance NNReal.instCompleteSpaceNNRealToUniformSpaceInstPseudoMetricSpaceNNReal :

CompleteSpace NNReal

Equations

NNReal.instCompleteSpaceNNRealToUniformSpaceInstPseudoMetricSpaceNNReal = ⋯

instance NNReal.instContinuousStarNNRealInstTopologicalSpaceNNRealToStarToInvolutiveStarToAddMonoidToAddMonoidWithOneToAddCommMonoidWithOneToNonAssocSemiringInstNNRealSemiringToStarAddMonoidToNonUnitalNonAssocSemiringInstStarRingNNRealToNonUnitalNonAssocSemiringToNonAssocSemiringInstNNRealSemiring :

ContinuousStar NNReal

Equations

One or more equations did not get rendered due to their size.

theorem continuous_real_toNNReal :

Continuous Real.toNNReal

@[simp]

theorem ContinuousMap.realToNNReal_apply :

⇑ContinuousMap.realToNNReal = Real.toNNReal

noncomputable def ContinuousMap.realToNNReal :

C(ℝ , NNReal )

Real.toNNReal bundled as a continuous map for convenience.

Equations

ContinuousMap.realToNNReal = { toFun := Real.toNNReal, continuous_toFun := continuous_real_toNNReal }

Instances For

theorem NNReal.continuous_coe :

Continuous NNReal.toReal

@[simp]

theorem ContinuousMap.coeNNRealReal_apply :

⇑ContinuousMap.coeNNRealReal = NNReal.toReal

def ContinuousMap.coeNNRealReal :

C(NNReal , ℝ )

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

Equations

ContinuousMap.coeNNRealReal = { toFun := NNReal.toReal, continuous_toFun := NNReal.continuous_coe }

Instances For

instance NNReal.ContinuousMap.canLift {X : Type u_2} [TopologicalSpace X] :

CanLift C(X, ℝ ) C(X, NNReal ) (ContinuousMap.comp ContinuousMap.coeNNRealReal) fun (f : C(X, ℝ )) => ∀ (x : X), 0 ≤ f x

Equations

⋯ = ⋯

@[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 tendsto_real_toNNReal_atTop :

Filter.Tendsto Real.toNNReal Filter.atTop Filter.atTop

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

instance NNReal.instContinuousSubNNRealInstTopologicalSpaceNNRealInstSubNNReal :

ContinuousSub NNReal

Equations

NNReal.instContinuousSubNNRealInstTopologicalSpaceNNRealInstSubNNReal = ⋯

instance NNReal.instHasContinuousInv₀NNRealInstNNRealZeroToInvInstCanonicallyLinearOrderedSemifieldNNRealInstTopologicalSpaceNNReal :

HasContinuousInv₀ NNReal

Equations

NNReal.instHasContinuousInv₀NNRealInstNNRealZeroToInvInstCanonicallyLinearOrderedSemifieldNNRealInstTopologicalSpaceNNReal = ⋯

instance NNReal.instContinuousSMulNNRealToSMulToMonoidToMonoidWithZeroInstNNRealSemiringInstMulActionNNRealToMonoidToMonoidWithZeroInstNNRealSemiringInstTopologicalSpaceNNReal {α : Type u_1} [TopologicalSpace α] [MulAction ℝ α] [ContinuousSMul ℝ α] :

ContinuousSMul NNReal α

Equations

⋯ = ⋯

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 := ⋯ }) ↔ 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 := ⋯ } = ∑' (n : α), { val := f n, property := ⋯ }

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) :

Summable (f ∘ 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 : α // 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.

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

NNReal ≃o NNReal

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

Equations

NNReal.powOrderIso n hn = StrictMono.orderIsoOfSurjective (fun (x : NNReal) => x ^ n) ⋯ ⋯

Instances For