# mathlibdocumentation

topology.instances.ennreal

# Extended non-negative reals

@[instance]

Topology on ennreal.

Note: this is different from the emetric_space topology. The emetric_space topology has is_open {⊤}, while this topology doesn't have singleton elements.

Equations
@[instance]

@[instance]

theorem ennreal.tendsto_coe {α : Type u_1} {f : filter α} {m : α → ℝ≥0} {a : ℝ≥0} :
filter.tendsto (λ (a : α), (m a)) f (𝓝 a) (𝓝 a)

theorem ennreal.continuous_coe_iff {α : Type u_1} {f : α → ℝ≥0} :
continuous (λ (a : α), (f a))

theorem ennreal.nhds_coe {r : ℝ≥0} :
𝓝 r = (𝓝 r)

theorem ennreal.nhds_coe_coe {r p : ℝ≥0} :
𝓝 (r, p) = filter.map (λ (p : , ((p.fst), (p.snd))) (𝓝 (r, p))

theorem ennreal.tendsto_of_real {α : Type u_1} {f : filter α} {m : α → } {a : } :
(𝓝 a)filter.tendsto (λ (a : α), ennreal.of_real (m a)) f (𝓝 (ennreal.of_real a))

The set of finite ennreal numbers is homeomorphic to nnreal.

Equations

The set of finite ennreal numbers is homeomorphic to nnreal.

Equations
theorem ennreal.nhds_top  :
= ⨅ (a : ennreal) (H : a ), 𝓟 (set.Ioi a)

theorem ennreal.nhds_top'  :
= ⨅ (r : ℝ≥0), 𝓟 (set.Ioi r)

theorem ennreal.tendsto_nhds_top_iff_nnreal {α : Type u_1} {m : α → ennreal} {f : filter α} :
(𝓝 ) ∀ (x : ℝ≥0), ∀ᶠ (a : α) in f, x < m a

theorem ennreal.tendsto_nhds_top_iff_nat {α : Type u_1} {m : α → ennreal} {f : filter α} :
(𝓝 ) ∀ (n : ), ∀ᶠ (a : α) in f, n < m a

theorem ennreal.tendsto_nhds_top {α : Type u_1} {m : α → ennreal} {f : filter α} :
(∀ (n : ), ∀ᶠ (a : α) in f, n < m a) (𝓝 )

@[simp]
theorem ennreal.tendsto_coe_nhds_top {α : Type u_1} {f : α → ℝ≥0} {l : filter α} :
filter.tendsto (λ (x : α), (f x)) l (𝓝 )

theorem ennreal.nhds_zero  :
𝓝 0 = ⨅ (a : ennreal) (H : a 0), 𝓟 (set.Iio a)

theorem ennreal.Icc_mem_nhds {x ε : ennreal} :
x 0 < εset.Icc (x - ε) (x + ε) 𝓝 x

theorem ennreal.nhds_of_ne_top {x : ennreal} :
x (𝓝 x = ⨅ (ε : ennreal) (H : ε > 0), 𝓟 (set.Icc (x - ε) (x + ε)))

theorem ennreal.tendsto_nhds {α : Type u_1} {f : filter α} {u : α → ennreal} {a : ennreal} :
a f (𝓝 a) ∀ (ε : ennreal), ε > 0(∀ᶠ (x : α) in f, u x set.Icc (a - ε) (a + ε)))

Characterization of neighborhoods for ennreal numbers. See also tendsto_order for a version with strict inequalities.

theorem ennreal.tendsto_at_top {β : Type u_2} [nonempty β] {f : β → ennreal} {a : ennreal} :
a (𝓝 a) ∀ (ε : ennreal), ε > 0(∃ (N : β), ∀ (n : β), n Nf n set.Icc (a - ε) (a + ε)))

@[instance]

theorem ennreal.tendsto_mul {a b : ennreal} :
a 0 b b 0 a filter.tendsto (λ (p : , (p.fst) * p.snd) (𝓝 (a, b)) (𝓝 (a * b))

theorem ennreal.tendsto.mul {α : Type u_1} {f : filter α} {ma mb : α → ennreal} {a b : ennreal} :
f (𝓝 a)a 0 b f (𝓝 b)b 0 a filter.tendsto (λ (a : α), (ma a) * mb a) f (𝓝 (a * b))

theorem ennreal.tendsto.const_mul {α : Type u_1} {f : filter α} {m : α → ennreal} {a b : ennreal} :
(𝓝 b)b 0 a filter.tendsto (λ (b : α), a * m b) f (𝓝 (a * b))

theorem ennreal.tendsto.mul_const {α : Type u_1} {f : filter α} {m : α → ennreal} {a b : ennreal} :
(𝓝 a)a 0 b filter.tendsto (λ (x : α), (m x) * b) f (𝓝 (a * b))

theorem ennreal.continuous_at_const_mul {a b : ennreal} :
a b 0 b

theorem ennreal.continuous_at_mul_const {a b : ennreal} :
a b 0continuous_at (λ (x : ennreal), x * a) b

theorem ennreal.continuous_mul_const {a : ennreal} :
a continuous (λ (x : ennreal), x * a)

theorem ennreal.infi_mul_left {ι : Sort u_1} [nonempty ι] {f : ι → ennreal} {a : ennreal} :
(a = (⨅ (i : ι), f i) = 0(∃ (i : ι), f i = 0))((⨅ (i : ι), a * f i) = a * ⨅ (i : ι), f i)

theorem ennreal.infi_mul_right {ι : Sort u_1} [nonempty ι] {f : ι → ennreal} {a : ennreal} :
(a = (⨅ (i : ι), f i) = 0(∃ (i : ι), f i = 0))(⨅ (i : ι), (f i) * a) = (⨅ (i : ι), f i) * a

@[simp]
theorem ennreal.tendsto_inv_iff {α : Type u_1} {f : filter α} {m : α → ennreal} {a : ennreal} :
filter.tendsto (λ (x : α), (m x)⁻¹) f (𝓝 a⁻¹) (𝓝 a)

theorem ennreal.tendsto.div {α : Type u_1} {f : filter α} {ma mb : α → ennreal} {a b : ennreal} :
f (𝓝 a)a 0 b 0 f (𝓝 b)b a filter.tendsto (λ (a : α), ma a / mb a) f (𝓝 (a / b))

theorem ennreal.tendsto.const_div {α : Type u_1} {f : filter α} {m : α → ennreal} {a b : ennreal} :
(𝓝 b)b a filter.tendsto (λ (b : α), a / m b) f (𝓝 (a / b))

theorem ennreal.tendsto.div_const {α : Type u_1} {f : filter α} {m : α → ennreal} {a b : ennreal} :
(𝓝 a)a 0 b 0filter.tendsto (λ (x : α), m x / b) f (𝓝 (a / b))

theorem ennreal.Sup_add {a : ennreal} {s : set ennreal} :
s.nonempty(Sup s + a = ⨆ (b : ennreal) (H : b s), b + a)

theorem ennreal.supr_add {a : ennreal} {ι : Sort u_1} {s : ι → ennreal} [h : nonempty ι] :
supr s + a = ⨆ (b : ι), s b + a

theorem ennreal.add_supr {a : ennreal} {ι : Sort u_1} {s : ι → ennreal} [h : nonempty ι] :
a + supr s = ⨆ (b : ι), a + s b

theorem ennreal.supr_add_supr {ι : Sort u_1} {f g : ι → ennreal} :
(∀ (i j : ι), ∃ (k : ι), f i + g j f k + g k)(supr f + supr g = ⨆ (a : ι), f a + g a)

theorem ennreal.supr_add_supr_of_monotone {ι : Type u_1} {f g : ι → ennreal} :
(supr f + supr g = ⨆ (a : ι), f a + g a)

theorem ennreal.finset_sum_supr_nat {α : Type u_1} {ι : Type u_2} {s : finset α} {f : α → ι → ennreal} :
(∀ (a : α), monotone (f a))(∑ (a : α) in s, supr (f a) = ⨆ (n : ι), ∑ (a : α) in s, f a n)

theorem ennreal.mul_Sup {s : set ennreal} {a : ennreal} :
a * Sup s = ⨆ (i : ennreal) (H : i s), a * i

theorem ennreal.mul_supr {ι : Sort u_1} {f : ι → ennreal} {a : ennreal} :
a * supr f = ⨆ (i : ι), a * f i

theorem ennreal.supr_mul {ι : Sort u_1} {f : ι → ennreal} {a : ennreal} :
(supr f) * a = ⨆ (i : ι), (f i) * a

theorem ennreal.tendsto_coe_sub {r : ℝ≥0} {b : ennreal} :
filter.tendsto (λ (b : ennreal), r - b) (𝓝 b) (𝓝 (r - b))

theorem ennreal.sub_supr {a : ennreal} {ι : Sort u_1} [hι : nonempty ι] {b : ι → ennreal} :
a < ((a - ⨆ (i : ι), b i) = ⨅ (i : ι), a - b i)

theorem ennreal.has_sum_coe {α : Type u_1} {f : α → ℝ≥0} {r : ℝ≥0} :
has_sum (λ (a : α), (f a)) r r

theorem ennreal.tsum_coe_eq {α : Type u_1} {r : ℝ≥0} {f : α → ℝ≥0} :
r(∑' (a : α), (f a)) = r

theorem ennreal.coe_tsum {α : Type u_1} {f : α → ℝ≥0} :
((tsum f) = ∑' (a : α), (f a))

theorem ennreal.has_sum {α : Type u_1} {f : α → ennreal} :
(⨆ (s : finset α), ∑ (a : α) in s, f a)

@[simp]
theorem ennreal.summable {α : Type u_1} {f : α → ennreal} :

theorem ennreal.tsum_coe_ne_top_iff_summable {β : Type u_2} {f : β → ℝ≥0} :
(∑' (b : β), (f b))

theorem ennreal.tsum_eq_supr_sum {α : Type u_1} {f : α → ennreal} :
(∑' (a : α), f a) = ⨆ (s : finset α), ∑ (a : α) in s, f a

theorem ennreal.tsum_eq_supr_sum' {α : Type u_1} {f : α → ennreal} {ι : Type u_2} (s : ι → ) :
(∀ (t : finset α), ∃ (i : ι), t s i)((∑' (a : α), f a) = ⨆ (i : ι), ∑ (a : α) in s i, f a)

theorem ennreal.tsum_sigma {α : Type u_1} {β : α → Type u_2} (f : Π (a : α), β aennreal) :
(∑' (p : Σ (a : α), β a), f p.fst p.snd) = ∑' (a : α) (b : β a), f a b

theorem ennreal.tsum_sigma' {α : Type u_1} {β : α → Type u_2} (f : (Σ (a : α), β a)ennreal) :
(∑' (p : Σ (a : α), β a), f p) = ∑' (a : α) (b : β a), f a, b⟩

theorem ennreal.tsum_prod {α : Type u_1} {β : Type u_2} {f : α → β → ennreal} :
(∑' (p : α × β), f p.fst p.snd) = ∑' (a : α) (b : β), f a b

theorem ennreal.tsum_comm {α : Type u_1} {β : Type u_2} {f : α → β → ennreal} :
(∑' (a : α) (b : β), f a b) = ∑' (b : β) (a : α), f a b

theorem ennreal.tsum_add {α : Type u_1} {f g : α → ennreal} :
(∑' (a : α), f a + g a) = (∑' (a : α), f a) + ∑' (a : α), g a

theorem ennreal.tsum_le_tsum {α : Type u_1} {f g : α → ennreal} :
(∀ (a : α), f a g a)((∑' (a : α), f a) ∑' (a : α), g a)

theorem ennreal.sum_le_tsum {α : Type u_1} {f : α → ennreal} (s : finset α) :
∑ (x : α) in s, f x ∑' (x : α), f x

theorem ennreal.tsum_eq_supr_nat' {f : ennreal} {N : } :
((∑' (i : ), f i) = ⨆ (i : ), ∑ (a : ) in finset.range (N i), f a)

theorem ennreal.tsum_eq_supr_nat {f : ennreal} :
(∑' (i : ), f i) = ⨆ (i : ), ∑ (a : ) in , f a

theorem ennreal.le_tsum {α : Type u_1} {f : α → ennreal} (a : α) :
f a ∑' (a : α), f a

theorem ennreal.tsum_eq_top_of_eq_top {α : Type u_1} {f : α → ennreal} :
(∃ (a : α), f a = )(∑' (a : α), f a) =

theorem ennreal.ne_top_of_tsum_ne_top {α : Type u_1} {f : α → ennreal} (h : (∑' (a : α), f a) ) (a : α) :
f a

theorem ennreal.tsum_mul_left {α : Type u_1} {a : ennreal} {f : α → ennreal} :
(∑' (i : α), a * f i) = a * ∑' (i : α), f i

theorem ennreal.tsum_mul_right {α : Type u_1} {a : ennreal} {f : α → ennreal} :
(∑' (i : α), (f i) * a) = (∑' (i : α), f i) * a

@[simp]
theorem ennreal.tsum_supr_eq {α : Type u_1} (a : α) {f : α → ennreal} :
(∑' (b : α), ⨆ (h : a = b), f b) = f a

theorem ennreal.has_sum_iff_tendsto_nat {f : ennreal} (r : ennreal) :
r filter.tendsto (λ (n : ), ∑ (i : ) in , f i) filter.at_top (𝓝 r)

theorem ennreal.to_nnreal_apply_of_tsum_ne_top {α : Type u_1} {f : α → ennreal} (hf : (∑' (i : α), f i) ) (x : α) :
x) = f x

theorem ennreal.summable_to_nnreal_of_tsum_ne_top {α : Type u_1} {f : α → ennreal} :
(∑' (i : α), f i)

theorem ennreal.tsum_apply {ι : Type u_1} {α : Type u_2} {f : ι → α → ennreal} {x : α} :
(∑' (i : ι), f i) x = ∑' (i : ι), f i x

theorem ennreal.tsum_sub {f g : ennreal} :
(∑' (i : ), g i) < g f((∑' (i : ), f i - g i) = (∑' (i : ), f i) - ∑' (i : ), g i)

theorem nnreal.exists_le_has_sum_of_le {β : Type u_2} {f g : β → ℝ≥0} {r : ℝ≥0} :
(∀ (b : β), g b f b) r(∃ (p : ℝ≥0) (H : p r), p)

Comparison test of convergence of ℝ≥0-valued series.

theorem nnreal.summable_of_le {β : Type u_2} {f g : β → ℝ≥0} :
(∀ (b : β), g b f b)

Comparison test of convergence of ℝ≥0-valued series.

theorem nnreal.has_sum_iff_tendsto_nat {f : ℝ≥0} {r : ℝ≥0} :
r filter.tendsto (λ (n : ), ∑ (i : ) in , f i) filter.at_top (𝓝 r)

A series of non-negative real numbers converges to r in the sense of has_sum if and only if the sequence of partial sum converges to r.

theorem nnreal.tsum_comp_le_tsum_of_inj {α : Type u_1} {β : Type u_2} {f : α → ℝ≥0} (hf : summable f) {i : β → α} :
((∑' (x : β), f (i x)) ∑' (x : α), f x)

theorem nnreal.tendsto_sum_nat_add (f : ℝ≥0) :
filter.tendsto (λ (i : ), ∑' (k : ), f (k + i)) filter.at_top (𝓝 0)

If f : ℕ → ℝ≥0 and ∑' f exists, then ∑' k, f (k + i) tends to zero.

theorem ennreal.tendsto_sum_nat_add (f : ennreal) :
(∑' (i : ), f i) filter.tendsto (λ (i : ), ∑' (k : ), f (k + i)) filter.at_top (𝓝 0)

theorem tsum_comp_le_tsum_of_inj {α : Type u_1} {β : Type u_2} {f : α → } (hf : summable f) (hn : ∀ (a : α), 0 f a) {i : β → α} :
tsum (f i) tsum f

theorem summable_of_nonneg_of_le {β : Type u_2} {f g : β → } :
(∀ (b : β), 0 g b)(∀ (b : β), g b f b)

Comparison test of convergence of series of non-negative real numbers.

theorem has_sum_iff_tendsto_nat_of_nonneg {f : } (hf : ∀ (i : ), 0 f i) (r : ) :
r filter.tendsto (λ (n : ), ∑ (i : ) in , f i) filter.at_top (𝓝 r)

A series of non-negative real numbers converges to r in the sense of has_sum if and only if the sequence of partial sum converges to r.

theorem not_summable_iff_tendsto_nat_at_top_of_nonneg {f : } :
(∀ (n : ), 0 f n)(¬ filter.tendsto (λ (n : ), ∑ (i : ) in , f i) filter.at_top filter.at_top)

theorem edist_ne_top_of_mem_ball {β : Type u_2} {a : β} {r : ennreal} (x y : r)) :

In an emetric ball, the distance between points is everywhere finite

def metric_space_emetric_ball {β : Type u_2} (a : β) (r : ennreal) :

Each ball in an extended metric space gives us a metric space, as the edist is everywhere finite.

Equations
theorem nhds_eq_nhds_emetric_ball {β : Type u_2} (a x : β) (r : ennreal) (h : x r) :
𝓝 x = (𝓝 x, h⟩)

theorem tendsto_iff_edist_tendsto_0 {α : Type u_1} {β : Type u_2} {l : filter β} {f : β → α} {y : α} :
(𝓝 y) filter.tendsto (λ (x : β), edist (f x) y) l (𝓝 0)

theorem emetric.cauchy_seq_iff_le_tendsto_0 {α : Type u_1} {β : Type u_2} [nonempty β] {s : β → α} :
∃ (b : β → ennreal), (∀ (n m N : β), N nN medist (s n) (s m) b N) (𝓝 0)

Yet another metric characterization of Cauchy sequences on integers. This one is often the most efficient.

theorem continuous_of_le_add_edist {α : Type u_1} {f : α → ennreal} (C : ennreal) :
C (∀ (x y : α), f x f y + C * y)

theorem continuous_edist {α : Type u_1}  :
continuous (λ (p : α × α), edist p.fst p.snd)

theorem continuous.edist {α : Type u_1} {β : Type u_2} {f g : β → α} :
continuous (λ (b : β), edist (f b) (g b))

theorem filter.tendsto.edist {α : Type u_1} {β : Type u_2} {f g : β → α} {x : filter β} {a b : α} :
(𝓝 a) (𝓝 b)filter.tendsto (λ (x : β), edist (f x) (g x)) x (𝓝 (edist a b))

theorem cauchy_seq_of_edist_le_of_tsum_ne_top {α : Type u_1} {f : → α} (d : ennreal) :
(∀ (n : ), edist (f n) (f n.succ) d n)tsum d

theorem emetric.is_closed_ball {α : Type u_1} {a : α} {r : ennreal} :

theorem edist_le_tsum_of_edist_le_of_tendsto {α : Type u_1} {f : → α} (d : ennreal) (hf : ∀ (n : ), edist (f n) (f n.succ) d n) {a : α} (ha : (𝓝 a)) (n : ) :
edist (f n) a ∑' (m : ), d (n + m)

If edist (f n) (f (n+1)) is bounded above by a function d : ℕ → ennreal, then the distance from f n to the limit is bounded by ∑'_{k=n}^∞ d k.

theorem edist_le_tsum_of_edist_le_of_tendsto₀ {α : Type u_1} {f : → α} (d : ennreal) (hf : ∀ (n : ), edist (f n) (f n.succ) d n) {a : α} :
(𝓝 a)(edist (f 0) a ∑' (m : ), d m)

If edist (f n) (f (n+1)) is bounded above by a function d : ℕ → ennreal, then the distance from f 0 to the limit is bounded by ∑'_{k=0}^∞ d k.