mathlib documentation

topology.instances.ennreal

Extended non-negative reals #

@[protected, instance]

Topology on ℝ≥0∞.

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
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[norm_cast]
theorem ennreal.tendsto_coe {α : Type u_1} {f : filter α} {m : α nnreal} {a : nnreal} :
filter.tendsto (λ (a : α), (m a)) f (nhds a) filter.tendsto m f (nhds a)
theorem ennreal.continuous_coe_iff {α : Type u_1} [topological_space α] {f : α nnreal} :
continuous (λ (a : α), (f a)) continuous f
theorem ennreal.tendsto_nhds_coe_iff {α : Type u_1} {l : filter α} {x : nnreal} {f : ennreal α} :
theorem ennreal.nhds_coe_coe {r p : nnreal} :
nhds (r, p) = filter.map (λ (p : nnreal × nnreal), ((p.fst), (p.snd))) (nhds (r, p))
theorem ennreal.tendsto_of_real {α : Type u_1} {f : filter α} {m : α } {a : } (h : filter.tendsto m f (nhds a)) :
filter.tendsto (λ (a : α), ennreal.of_real (m a)) f (nhds (ennreal.of_real a))
theorem ennreal.eventually_eq_of_to_real_eventually_eq {α : Type u_1} {l : filter α} {f g : α ennreal} (hfi : ∀ᶠ (x : α) in l, f x ) (hgi : ∀ᶠ (x : α) in l, g x ) (hfg : (λ (x : α), (f x).to_real) =ᶠ[l] λ (x : α), (g x).to_real) :
f =ᶠ[l] g

The set of finite ℝ≥0∞ numbers is homeomorphic to ℝ≥0.

Equations
noncomputable def ennreal.lt_top_homeomorph_nnreal  :

The set of finite ℝ≥0∞ numbers is homeomorphic to ℝ≥0.

Equations
theorem ennreal.nhds_top_basis  :
(nhds ).has_basis (λ (a : ennreal), a < ) (λ (a : ennreal), set.Ioi a)
theorem ennreal.tendsto_nhds_top_iff_nnreal {α : Type u_1} {m : α ennreal} {f : filter α} :
filter.tendsto m f (nhds ) (x : nnreal), ∀ᶠ (a : α) in f, x < m a
theorem ennreal.tendsto_nhds_top_iff_nat {α : Type u_1} {m : α ennreal} {f : filter α} :
filter.tendsto m f (nhds ) (n : ), ∀ᶠ (a : α) in f, n < m a
theorem ennreal.tendsto_nhds_top {α : Type u_1} {m : α ennreal} {f : filter α} (h : (n : ), ∀ᶠ (a : α) in f, n < m a) :
@[simp, norm_cast]
theorem ennreal.tendsto_coe_nhds_top {α : Type u_1} {f : α nnreal} {l : filter α} :
theorem ennreal.nhds_zero  :
nhds 0 = (a : ennreal) (H : a 0), filter.principal (set.Iio a)
theorem ennreal.nhds_zero_basis  :
(nhds 0).has_basis (λ (a : ennreal), 0 < a) (λ (a : ennreal), set.Iio a)
theorem ennreal.Icc_mem_nhds {x ε : ennreal} (xt : x ) (ε0 : ε 0) :
set.Icc (x - ε) (x + ε) nhds x
theorem ennreal.nhds_of_ne_top {x : ennreal} (xt : x ) :
nhds x = (ε : ennreal) (H : ε > 0), filter.principal (set.Icc (x - ε) (x + ε))
@[protected]
theorem ennreal.tendsto_nhds {α : Type u_1} {f : filter α} {u : α ennreal} {a : ennreal} (ha : a ) :
filter.tendsto u f (nhds a) (ε : ennreal), ε > 0 (∀ᶠ (x : α) in f, u x set.Icc (a - ε) (a + ε))

Characterization of neighborhoods for ℝ≥0∞ numbers. See also tendsto_order for a version with strict inequalities.

@[protected]
theorem ennreal.tendsto_nhds_zero {α : Type u_1} {f : filter α} {u : α ennreal} :
filter.tendsto u f (nhds 0) (ε : ennreal), ε > 0 (∀ᶠ (x : α) in f, u x ε)
@[protected]
theorem ennreal.tendsto_at_top {β : Type u_2} [nonempty β] [semilattice_sup β] {f : β ennreal} {a : ennreal} (ha : a ) :
filter.tendsto f filter.at_top (nhds a) (ε : ennreal), ε > 0 ( (N : β), (n : β), n N f n set.Icc (a - ε) (a + ε))
@[protected]
theorem ennreal.tendsto_at_top_zero {β : Type u_2} [hβ : nonempty β] [semilattice_sup β] {f : β ennreal} :
filter.tendsto f filter.at_top (nhds 0) (ε : ennreal), ε > 0 ( (N : β), (n : β), n N f n ε)
theorem ennreal.tendsto_sub {a b : ennreal} (h : a b ) :
filter.tendsto (λ (p : ennreal × ennreal), p.fst - p.snd) (nhds (a, b)) (nhds (a - b))
@[protected]
theorem ennreal.tendsto.sub {α : Type u_1} {f : filter α} {ma mb : α ennreal} {a b : ennreal} (hma : filter.tendsto ma f (nhds a)) (hmb : filter.tendsto mb f (nhds b)) (h : a b ) :
filter.tendsto (λ (a : α), ma a - mb a) f (nhds (a - b))
@[protected]
theorem ennreal.tendsto_mul {a b : ennreal} (ha : a 0 b ) (hb : b 0 a ) :
filter.tendsto (λ (p : ennreal × ennreal), p.fst * p.snd) (nhds (a, b)) (nhds (a * b))
@[protected]
theorem ennreal.tendsto.mul {α : Type u_1} {f : filter α} {ma mb : α ennreal} {a b : ennreal} (hma : filter.tendsto ma f (nhds a)) (ha : a 0 b ) (hmb : filter.tendsto mb f (nhds b)) (hb : b 0 a ) :
filter.tendsto (λ (a : α), ma a * mb a) f (nhds (a * b))
theorem continuous_on.ennreal_mul {α : Type u_1} [topological_space α] {f g : α ennreal} {s : set α} (hf : continuous_on f s) (hg : continuous_on g s) (h₁ : (x : α), x s f x 0 g x ) (h₂ : (x : α), x s g x 0 f x ) :
continuous_on (λ (x : α), f x * g x) s
theorem continuous.ennreal_mul {α : Type u_1} [topological_space α] {f g : α ennreal} (hf : continuous f) (hg : continuous g) (h₁ : (x : α), f x 0 g x ) (h₂ : (x : α), g x 0 f x ) :
continuous (λ (x : α), f x * g x)
@[protected]
theorem ennreal.tendsto.const_mul {α : Type u_1} {f : filter α} {m : α ennreal} {a b : ennreal} (hm : filter.tendsto m f (nhds b)) (hb : b 0 a ) :
filter.tendsto (λ (b : α), a * m b) f (nhds (a * b))
@[protected]
theorem ennreal.tendsto.mul_const {α : Type u_1} {f : filter α} {m : α ennreal} {a b : ennreal} (hm : filter.tendsto m f (nhds a)) (ha : a 0 b ) :
filter.tendsto (λ (x : α), m x * b) f (nhds (a * b))
theorem ennreal.tendsto_finset_prod_of_ne_top {α : Type u_1} {ι : Type u_2} {f : ι α ennreal} {x : filter α} {a : ι ennreal} (s : finset ι) (h : (i : ι), i s filter.tendsto (f i) x (nhds (a i))) (h' : (i : ι), i s a i ) :
filter.tendsto (λ (b : α), s.prod (λ (c : ι), f c b)) x (nhds (s.prod (λ (c : ι), a c)))
@[protected]
@[protected]
theorem ennreal.continuous_at_mul_const {a b : ennreal} (h : a b 0) :
continuous_at (λ (x : ennreal), x * a) b
@[protected]
@[protected]
theorem ennreal.continuous_mul_const {a : ennreal} (ha : a ) :
continuous (λ (x : ennreal), x * a)
@[protected]
theorem ennreal.continuous_div_const (c : ennreal) (c_ne_zero : c 0) :
continuous (λ (x : ennreal), x / c)
@[continuity]
theorem ennreal.continuous_pow (n : ) :
continuous (λ (a : ennreal), a ^ n)
theorem ennreal.continuous_sub_left {a : ennreal} (a_ne_top : a ) :
continuous (λ (x : ennreal), a - x)
theorem ennreal.continuous_on_sub_left (a : ennreal) :
continuous_on (λ (x : ennreal), a - x) {x : ennreal | x }
theorem ennreal.continuous_sub_right (a : ennreal) :
continuous (λ (x : ennreal), x - a)
@[protected]
theorem ennreal.tendsto.pow {α : Type u_1} {f : filter α} {m : α ennreal} {a : ennreal} {n : } (hm : filter.tendsto m f (nhds a)) :
filter.tendsto (λ (x : α), m x ^ n) f (nhds (a ^ n))
theorem ennreal.le_of_forall_lt_one_mul_le {x y : ennreal} (h : (a : ennreal), a < 1 a * x y) :
x y
theorem ennreal.infi_mul_left' {ι : Sort u_1} {f : ι ennreal} {a : ennreal} (h : a = ( (i : ι), f i) = 0 ( (i : ι), f i = 0)) (h0 : a = 0 nonempty ι) :
( (i : ι), a * f i) = a * (i : ι), f i
theorem ennreal.infi_mul_left {ι : Sort u_1} [nonempty ι] {f : ι ennreal} {a : ennreal} (h : 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} {f : ι ennreal} {a : ennreal} (h : a = ( (i : ι), f i) = 0 ( (i : ι), f i = 0)) (h0 : a = 0 nonempty ι) :
( (i : ι), f i * a) = ( (i : ι), f i) * a
theorem ennreal.infi_mul_right {ι : Sort u_1} [nonempty ι] {f : ι ennreal} {a : ennreal} (h : a = ( (i : ι), f i) = 0 ( (i : ι), f i = 0)) :
( (i : ι), f i * a) = ( (i : ι), f i) * a
theorem ennreal.inv_map_infi {ι : Sort u_1} {x : ι ennreal} :
(infi x)⁻¹ = (i : ι), (x i)⁻¹
theorem ennreal.inv_map_supr {ι : Sort u_1} {x : ι ennreal} :
(supr x)⁻¹ = (i : ι), (x i)⁻¹
theorem ennreal.inv_limsup {ι : Type u_1} {x : ι ennreal} {l : filter ι} :
(filter.limsup x l)⁻¹ = filter.liminf (λ (i : ι), (x i)⁻¹) l
theorem ennreal.inv_liminf {ι : Type u_1} {x : ι ennreal} {l : filter ι} :
(filter.liminf x l)⁻¹ = filter.limsup (λ (i : ι), (x i)⁻¹) l
@[protected, simp]
theorem ennreal.tendsto_inv_iff {α : Type u_1} {f : filter α} {m : α ennreal} {a : ennreal} :
filter.tendsto (λ (x : α), (m x)⁻¹) f (nhds a⁻¹) filter.tendsto m f (nhds a)
@[protected]
theorem ennreal.tendsto.div {α : Type u_1} {f : filter α} {ma mb : α ennreal} {a b : ennreal} (hma : filter.tendsto ma f (nhds a)) (ha : a 0 b 0) (hmb : filter.tendsto mb f (nhds b)) (hb : b a ) :
filter.tendsto (λ (a : α), ma a / mb a) f (nhds (a / b))
@[protected]
theorem ennreal.tendsto.const_div {α : Type u_1} {f : filter α} {m : α ennreal} {a b : ennreal} (hm : filter.tendsto m f (nhds b)) (hb : b a ) :
filter.tendsto (λ (b : α), a / m b) f (nhds (a / b))
@[protected]
theorem ennreal.tendsto.div_const {α : Type u_1} {f : filter α} {m : α ennreal} {a b : ennreal} (hm : filter.tendsto m f (nhds a)) (ha : a 0 b 0) :
filter.tendsto (λ (x : α), m x / b) f (nhds (a / b))
theorem ennreal.supr_add {a : ennreal} {ι : Sort u_1} {s : ι ennreal} [h : nonempty ι] :
supr s + a = (b : ι), s b + a
theorem ennreal.bsupr_add' {a : ennreal} {ι : Sort u_1} {p : ι Prop} (h : (i : ι), p i) {f : ι ennreal} :
( (i : ι) (hi : p i), f i) + a = (i : ι) (hi : p i), f i + a
theorem ennreal.add_bsupr' {a : ennreal} {ι : Sort u_1} {p : ι Prop} (h : (i : ι), p i) {f : ι ennreal} :
(a + (i : ι) (hi : p i), f i) = (i : ι) (hi : p i), a + f i
theorem ennreal.bsupr_add {a : ennreal} {ι : Type u_1} {s : set ι} (hs : s.nonempty) {f : ι ennreal} :
( (i : ι) (H : i s), f i) + a = (i : ι) (H : i s), f i + a
theorem ennreal.add_bsupr {a : ennreal} {ι : Type u_1} {s : set ι} (hs : s.nonempty) {f : ι ennreal} :
(a + (i : ι) (H : i s), f i) = (i : ι) (H : i s), a + f i
theorem ennreal.Sup_add {a : ennreal} {s : set ennreal} (hs : s.nonempty) :
has_Sup.Sup s + a = (b : ennreal) (H : b s), b + a
theorem ennreal.add_supr {a : ennreal} {ι : Sort u_1} {s : ι ennreal} [nonempty ι] :
a + supr s = (b : ι), a + s b
theorem ennreal.supr_add_supr_le {ι : Sort u_1} {ι' : Sort u_2} [nonempty ι] [nonempty ι'] {f : ι ennreal} {g : ι' ennreal} {a : ennreal} (h : (i : ι) (j : ι'), f i + g j a) :
supr f + supr g a
theorem ennreal.bsupr_add_bsupr_le' {ι : Sort u_1} {ι' : Sort u_2} {p : ι Prop} {q : ι' Prop} (hp : (i : ι), p i) (hq : (j : ι'), q j) {f : ι ennreal} {g : ι' ennreal} {a : ennreal} (h : (i : ι), p i (j : ι'), q j f i + g j a) :
(( (i : ι) (hi : p i), f i) + (j : ι') (hj : q j), g j) a
theorem ennreal.bsupr_add_bsupr_le {ι : Type u_1} {ι' : Type u_2} {s : set ι} {t : set ι'} (hs : s.nonempty) (ht : t.nonempty) {f : ι ennreal} {g : ι' ennreal} {a : ennreal} (h : (i : ι), i s (j : ι'), j t f i + g j a) :
(( (i : ι) (H : i s), f i) + (j : ι') (H : j t), g j) a
theorem ennreal.supr_add_supr {ι : Sort u_1} {f g : ι ennreal} (h : (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} [semilattice_sup ι] {f g : ι ennreal} (hf : monotone f) (hg : monotone g) :
supr f + supr g = (a : ι), f a + g a
theorem ennreal.finset_sum_supr_nat {α : Type u_1} {ι : Type u_2} [semilattice_sup ι] {s : finset α} {f : α ι ennreal} (hf : (a : α), monotone (f a)) :
s.sum (λ (a : α), supr (f a)) = (n : ι), s.sum (λ (a : α), f a n)
theorem ennreal.mul_supr {ι : Sort u_1} {f : ι ennreal} {a : ennreal} :
a * supr f = (i : ι), a * f i
theorem ennreal.mul_Sup {s : set ennreal} {a : ennreal} :
a * has_Sup.Sup s = (i : ennreal) (H : i s), a * i
theorem ennreal.supr_mul {ι : Sort u_1} {f : ι ennreal} {a : ennreal} :
supr f * a = (i : ι), f i * a
theorem ennreal.supr_div {ι : Sort u_1} {f : ι ennreal} {a : ennreal} :
supr f / a = (i : ι), f i / a
@[protected]
theorem ennreal.tendsto_coe_sub {r : nnreal} {b : ennreal} :
filter.tendsto (λ (b : ennreal), r - b) (nhds b) (nhds (r - b))
theorem ennreal.sub_supr {a : ennreal} {ι : Sort u_1} [nonempty ι] {b : ι ennreal} (hr : a < ) :
(a - (i : ι), b i) = (i : ι), a - b i
theorem ennreal.exists_lt_add_of_lt_add {x y z : ennreal} (h : x < y + z) (hy : y 0) (hz : z 0) :
(y' z' : ennreal), y' < y z' < z x < y' + z'
theorem ennreal.exists_frequently_lt_of_liminf_ne_top {ι : Type u_1} {l : filter ι} {x : ι } (hx : filter.liminf (λ (n : ι), x n‖₊) l ) :
(R : ), ∃ᶠ (n : ι) in l, x n < R
theorem ennreal.exists_frequently_lt_of_liminf_ne_top' {ι : Type u_1} {l : filter ι} {x : ι } (hx : filter.liminf (λ (n : ι), x n‖₊) l ) :
(R : ), ∃ᶠ (n : ι) in l, R < x n
theorem ennreal.exists_upcrossings_of_not_bounded_under {ι : Type u_1} {l : filter ι} {x : ι } (hf : filter.liminf (λ (i : ι), x i‖₊) l ) (hbdd : ¬filter.is_bounded_under has_le.le l (λ (i : ι), |x i|)) :
(a b : ), a < b (∃ᶠ (i : ι) in l, x i < a) ∃ᶠ (i : ι) in l, b < x i
@[protected, norm_cast]
theorem ennreal.has_sum_coe {α : Type u_1} {f : α nnreal} {r : nnreal} :
has_sum (λ (a : α), (f a)) r has_sum f r
@[protected]
theorem ennreal.tsum_coe_eq {α : Type u_1} {r : nnreal} {f : α nnreal} (h : has_sum f r) :
∑' (a : α), (f a) = r
@[protected]
theorem ennreal.coe_tsum {α : Type u_1} {f : α nnreal} :
summable f (tsum f) = ∑' (a : α), (f a)
@[protected]
theorem ennreal.has_sum {α : Type u_1} {f : α ennreal} :
has_sum f ( (s : finset α), s.sum (λ (a : α), f a))
@[protected, simp]
theorem ennreal.summable {α : Type u_1} {f : α ennreal} :
theorem ennreal.tsum_coe_ne_top_iff_summable {β : Type u_2} {f : β nnreal} :
∑' (b : β), (f b) summable f
@[protected]
theorem ennreal.tsum_eq_supr_sum {α : Type u_1} {f : α ennreal} :
∑' (a : α), f a = (s : finset α), s.sum (λ (a : α), f a)
@[protected]
theorem ennreal.tsum_eq_supr_sum' {α : Type u_1} {f : α ennreal} {ι : Type u_2} (s : ι finset α) (hs : (t : finset α), (i : ι), t s i) :
∑' (a : α), f a = (i : ι), (s i).sum (λ (a : α), f a)
@[protected]
theorem ennreal.tsum_sigma {α : Type u_1} {β : α Type u_2} (f : Π (a : α), β a ennreal) :
∑' (p : Σ (a : α), β a), f p.fst p.snd = ∑' (a : α) (b : β a), f a b
@[protected]
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⟩
@[protected]
theorem ennreal.tsum_prod {α : Type u_1} {β : Type u_2} {f : α β ennreal} :
∑' (p : α × β), f p.fst p.snd = ∑' (a : α) (b : β), f a b
@[protected]
theorem ennreal.tsum_comm {α : Type u_1} {β : Type u_2} {f : α β ennreal} :
∑' (a : α) (b : β), f a b = ∑' (b : β) (a : α), f a b
@[protected]
theorem ennreal.tsum_add {α : Type u_1} {f g : α ennreal} :
∑' (a : α), (f a + g a) = ∑' (a : α), f a + ∑' (a : α), g a
@[protected]
theorem ennreal.tsum_le_tsum {α : Type u_1} {f g : α ennreal} (h : (a : α), f a g a) :
∑' (a : α), f a ∑' (a : α), g a
@[protected]
theorem ennreal.sum_le_tsum {α : Type u_1} {f : α ennreal} (s : finset α) :
s.sum (λ (x : α), f x) ∑' (x : α), f x
@[protected]
theorem ennreal.tsum_eq_supr_nat' {f : ennreal} {N : } (hN : filter.tendsto N filter.at_top filter.at_top) :
∑' (i : ), f i = (i : ), (finset.range (N i)).sum (λ (a : ), f a)
@[protected]
theorem ennreal.tsum_eq_supr_nat {f : ennreal} :
∑' (i : ), f i = (i : ), (finset.range i).sum (λ (a : ), f a)
@[protected]
theorem ennreal.tsum_eq_liminf_sum_nat {f : ennreal} :
∑' (i : ), f i = filter.liminf (λ (n : ), (finset.range n).sum (λ (i : ), f i)) filter.at_top
@[protected]
theorem ennreal.le_tsum {α : Type u_1} {f : α ennreal} (a : α) :
f a ∑' (a : α), f a
@[protected, simp]
theorem ennreal.tsum_eq_zero {α : Type u_1} {f : α ennreal} :
∑' (i : α), f i = 0 (i : α), f i = 0
@[protected]
theorem ennreal.tsum_eq_top_of_eq_top {α : Type u_1} {f : α ennreal} :
( (a : α), f a = ) ∑' (a : α), f a =
@[protected]
theorem ennreal.lt_top_of_tsum_ne_top {α : Type u_1} {a : α ennreal} (tsum_ne_top : ∑' (i : α), a i ) (j : α) :
a j <
@[protected, simp]
theorem ennreal.tsum_top {α : Type u_1} [nonempty α] :
∑' (a : α), =
theorem ennreal.tsum_const_eq_top_of_ne_zero {α : Type u_1} [infinite α] {c : ennreal} (hc : c 0) :
∑' (a : α), c =
@[protected]
theorem ennreal.ne_top_of_tsum_ne_top {α : Type u_1} {f : α ennreal} (h : ∑' (a : α), f a ) (a : α) :
f a
@[protected]
theorem ennreal.tsum_mul_left {α : Type u_1} {a : ennreal} {f : α ennreal} :
∑' (i : α), a * f i = a * ∑' (i : α), f i
@[protected]
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.tendsto_nat_tsum (f : ennreal) :
filter.tendsto (λ (n : ), (finset.range n).sum (λ (i : ), f i)) filter.at_top (nhds (∑' (n : ), f n))
theorem ennreal.to_nnreal_apply_of_tsum_ne_top {α : Type u_1} {f : α ennreal} (hf : ∑' (i : α), f i ) (x : α) :
theorem ennreal.summable_to_nnreal_of_tsum_ne_top {α : Type u_1} {f : α ennreal} (hf : ∑' (i : α), f i ) :
theorem ennreal.tendsto_tsum_compl_at_top_zero {α : Type u_1} {f : α ennreal} (hf : ∑' (x : α), f x ) :
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.

@[protected]
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} (h₁ : ∑' (i : ), g i ) (h₂ : g f) :
∑' (i : ), (f i - g i) = ∑' (i : ), f i - ∑' (i : ), g i
theorem ennreal.tsum_mono_subtype {α : Type u_1} (f : α ennreal) {s t : set α} (h : s t) :
∑' (x : s), f x ∑' (x : t), f x
theorem ennreal.tsum_union_le {α : Type u_1} (f : α ennreal) (s t : set α) :
∑' (x : (s t)), f x ∑' (x : s), f x + ∑' (x : t), f x
theorem ennreal.tsum_bUnion_le {α : Type u_1} {ι : Type u_2} (f : α ennreal) (s : finset ι) (t : ι set α) :
∑' (x : (i : ι) (H : i s), t i), f x s.sum (λ (i : ι), ∑' (x : (t i)), f x)
theorem ennreal.tsum_Union_le {α : Type u_1} {ι : Type u_2} [fintype ι] (f : α ennreal) (t : ι set α) :
∑' (x : (i : ι), t i), f x finset.univ.sum (λ (i : ι), ∑' (x : (t i)), f x)
theorem ennreal.tsum_add_one_eq_top {f : ennreal} (hf : ∑' (n : ), f n = ) (hf0 : f 0 ) :
∑' (n : ), f (n + 1) =
theorem ennreal.finite_const_le_of_tsum_ne_top {ι : Type u_1} {a : ι ennreal} (tsum_ne_top : ∑' (i : ι), a i ) {ε : ennreal} (ε_ne_zero : ε 0) :
{i : ι | ε a i}.finite

A sum of extended nonnegative reals which is finite can have only finitely many terms above any positive threshold.

theorem ennreal.finset_card_const_le_le_of_tsum_le {ι : Type u_1} {a : ι ennreal} {c : ennreal} (c_ne_top : c ) (tsum_le_c : ∑' (i : ι), a i c) {ε : ennreal} (ε_ne_zero : ε 0) :
(hf : {i : ι | ε a i}.finite), (hf.to_finset.card) c / ε

Markov's inequality for finset.card and tsum in ℝ≥0∞.

theorem ennreal.tendsto_to_real_iff {ι : Type u_1} {fi : filter ι} {f : ι ennreal} (hf : (i : ι), f i ) {x : ennreal} (hx : x ) :
filter.tendsto (λ (n : ι), (f n).to_real) fi (nhds x.to_real) filter.tendsto f fi (nhds x)
theorem ennreal.tsum_coe_ne_top_iff_summable_coe {α : Type u_1} {f : α nnreal} :
∑' (a : α), (f a) summable (λ (a : α), (f a))
theorem ennreal.tsum_coe_eq_top_iff_not_summable_coe {α : Type u_1} {f : α nnreal} :
∑' (a : α), (f a) = ¬summable (λ (a : α), (f a))
theorem ennreal.has_sum_to_real {α : Type u_1} {f : α ennreal} (hsum : ∑' (x : α), f x ) :
has_sum (λ (x : α), (f x).to_real) (∑' (x : α), (f x).to_real)
theorem ennreal.summable_to_real {α : Type u_1} {f : α ennreal} (hsum : ∑' (x : α), f x ) :
summable (λ (x : α), (f x).to_real)
theorem nnreal.tsum_eq_to_nnreal_tsum {β : Type u_2} {f : β nnreal} :
∑' (b : β), f b = (∑' (b : β), (f b)).to_nnreal
theorem nnreal.exists_le_has_sum_of_le {β : Type u_2} {f g : β nnreal} {r : nnreal} (hgf : (b : β), g b f b) (hfr : has_sum f r) :
(p : nnreal) (H : p r), has_sum g p

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

theorem nnreal.summable_of_le {β : Type u_2} {f g : β nnreal} (hgf : (b : β), g b f b) :

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

theorem nnreal.has_sum_iff_tendsto_nat {f : nnreal} {r : nnreal} :
has_sum f r filter.tendsto (λ (n : ), (finset.range n).sum (λ (i : ), f i)) filter.at_top (nhds 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.summable_of_sum_range_le {f : nnreal} {c : nnreal} (h : (n : ), (finset.range n).sum (λ (i : ), f i) c) :
theorem nnreal.tsum_le_of_sum_range_le {f : nnreal} {c : nnreal} (h : (n : ), (finset.range n).sum (λ (i : ), f i) c) :
∑' (n : ), f n c
theorem nnreal.tsum_comp_le_tsum_of_inj {α : Type u_1} {β : Type u_2} {f : α nnreal} (hf : summable f) {i : β α} (hi : function.injective i) :
∑' (x : β), f (i x) ∑' (x : α), f x
theorem nnreal.summable_sigma {α : Type u_1} {β : α Type u_2} {f : (Σ (x : α), β x) nnreal} :
summable f ( (x : α), summable (λ (y : β x), f x, y⟩)) summable (λ (x : α), ∑' (y : β x), f x, y⟩)
theorem nnreal.indicator_summable {α : Type u_1} {f : α nnreal} (hf : summable f) (s : set α) :
theorem nnreal.tsum_indicator_ne_zero {α : Type u_1} {f : α nnreal} (hf : summable f) {s : set α} (h : (a : α) (H : a s), f a 0) :
∑' (x : α), s.indicator f x 0
theorem nnreal.tendsto_sum_nat_add (f : nnreal) :
filter.tendsto (λ (i : ), ∑' (k : ), f (k + i)) filter.at_top (nhds 0)

For f : ℕ → ℝ≥0, then ∑' k, f (k + i) tends to zero. This does not require a summability assumption on f, as otherwise all sums are zero.

theorem nnreal.has_sum_lt {α : Type u_1} {f g : α nnreal} {sf sg : nnreal} {i : α} (h : (a : α), f a g a) (hi : f i < g i) (hf : has_sum f sf) (hg : has_sum g sg) :
sf < sg
theorem nnreal.has_sum_strict_mono {α : Type u_1} {f g : α nnreal} {sf sg : nnreal} (hf : has_sum f sf) (hg : has_sum g sg) (h : f < g) :
sf < sg
theorem nnreal.tsum_lt_tsum {α : Type u_1} {f g : α nnreal} {i : α} (h : (a : α), f a g a) (hi : f i < g i) (hg : summable g) :
∑' (n : α), f n < ∑' (n : α), g n
theorem nnreal.tsum_strict_mono {α : Type u_1} {f g : α nnreal} (hg : summable g) (h : f < g) :
∑' (n : α), f n < ∑' (n : α), g n
theorem nnreal.tsum_pos {α : Type u_1} {g : α nnreal} (hg : summable g) (i : α) (hi : 0 < g i) :
0 < ∑' (b : α), g b
theorem ennreal.tsum_to_nnreal_eq {α : Type u_1} {f : α ennreal} (hf : (a : α), f a ) :
(∑' (a : α), f a).to_nnreal = ∑' (a : α), (f a).to_nnreal
theorem ennreal.tsum_to_real_eq {α : Type u_1} {f : α ennreal} (hf : (a : α), f a ) :
(∑' (a : α), f a).to_real = ∑' (a : α), (f a).to_real
theorem ennreal.tendsto_sum_nat_add (f : ennreal) (hf : ∑' (i : ), f i ) :
filter.tendsto (λ (i : ), ∑' (k : ), f (k + i)) filter.at_top (nhds 0)
theorem ennreal.tsum_le_of_sum_range_le {f : ennreal} {c : ennreal} (h : (n : ), (finset.range n).sum (λ (i : ), f i) c) :
∑' (n : ), f n c
theorem ennreal.has_sum_lt {α : Type u_1} {f g : α ennreal} {sf sg : ennreal} {i : α} (h : (a : α), f a g a) (hi : f i < g i) (hsf : sf ) (hf : has_sum f sf) (hg : has_sum g sg) :
sf < sg
theorem ennreal.tsum_lt_tsum {α : Type u_1} {f g : α ennreal} {i : α} (hfi : tsum f ) (h : (a : α), f a g a) (hi : f i < g i) :
∑' (x : α), f x < ∑' (x : α), g x
theorem tsum_comp_le_tsum_of_inj {α : Type u_1} {β : Type u_2} {f : α } (hf : summable f) (hn : (a : α), 0 f a) {i : β α} (hi : function.injective i) :
tsum (f i) tsum f
theorem summable_of_nonneg_of_le {β : Type u_2} {f g : β } (hg : (b : β), 0 g b) (hgf : (b : β), g b f b) (hf : summable f) :

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

theorem summable.to_nnreal {α : Type u_1} {f : α } (hf : summable f) :
summable (λ (n : α), (f n).to_nnreal)
theorem has_sum_iff_tendsto_nat_of_nonneg {f : } (hf : (i : ), 0 f i) (r : ) :
has_sum f r filter.tendsto (λ (n : ), (finset.range n).sum (λ (i : ), f i)) filter.at_top (nhds 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 ennreal.of_real_tsum_of_nonneg {α : Type u_1} {f : α } (hf_nonneg : (n : α), 0 f n) (hf : summable f) :
ennreal.of_real (∑' (n : α), f n) = ∑' (n : α), ennreal.of_real (f n)
theorem summable_sigma_of_nonneg {α : Type u_1} {β : α Type u_2} {f : (Σ (x : α), β x) } (hf : (x : Σ (x : α), β x), 0 f x) :
summable f ( (x : α), summable (λ (y : β x), f x, y⟩)) summable (λ (x : α), ∑' (y : β x), f x, y⟩)
theorem summable_of_sum_le {ι : Type u_1} {f : ι } {c : } (hf : 0 f) (h : (u : finset ι), u.sum (λ (x : ι), f x) c) :
theorem summable_of_sum_range_le {f : } {c : } (hf : (n : ), 0 f n) (h : (n : ), (finset.range n).sum (λ (i : ), f i) c) :
theorem real.tsum_le_of_sum_range_le {f : } {c : } (hf : (n : ), 0 f n) (h : (n : ), (finset.range n).sum (λ (i : ), f i) c) :
∑' (n : ), f n c
theorem tsum_lt_tsum_of_nonneg {i : } {f g : } (h0 : (b : ), 0 f b) (h : (b : ), f b g b) (hi : f i < g i) (hg : summable g) :
∑' (n : ), f n < ∑' (n : ), g n

If a sequence f with non-negative terms is dominated by a sequence g with summable series and at least one term of f is strictly smaller than the corresponding term in g, then the series of f is strictly smaller than the series of g.

theorem edist_ne_top_of_mem_ball {β : Type u_2} [emetric_space β] {a : β} {r : ennreal} (x y : (emetric.ball a r)) :

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

def metric_space_emetric_ball {β : Type u_2} [emetric_space β] (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} [emetric_space β] (a x : β) (r : ennreal) (h : x emetric.ball a r) :
theorem tendsto_iff_edist_tendsto_0 {α : Type u_1} {β : Type u_2} [pseudo_emetric_space α] {l : filter β} {f : β α} {y : α} :
filter.tendsto f l (nhds y) filter.tendsto (λ (x : β), has_edist.edist (f x) y) l (nhds 0)
theorem emetric.cauchy_seq_iff_le_tendsto_0 {α : Type u_1} {β : Type u_2} [pseudo_emetric_space α] [nonempty β] [semilattice_sup β] {s : β α} :
cauchy_seq s (b : β ennreal), ( (n m N : β), N n N m has_edist.edist (s n) (s m) b N) filter.tendsto b filter.at_top (nhds 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} [pseudo_emetric_space α] {f : α ennreal} (C : ennreal) (hC : C ) (h : (x y : α), f x f y + C * has_edist.edist x y) :
theorem continuous_edist {α : Type u_1} [pseudo_emetric_space α] :
continuous (λ (p : α × α), has_edist.edist p.fst p.snd)
@[continuity]
theorem continuous.edist {α : Type u_1} {β : Type u_2} [pseudo_emetric_space α] [topological_space β] {f g : β α} (hf : continuous f) (hg : continuous g) :
continuous (λ (b : β), has_edist.edist (f b) (g b))
theorem filter.tendsto.edist {α : Type u_1} {β : Type u_2} [pseudo_emetric_space α] {f g : β α} {x : filter β} {a b : α} (hf : filter.tendsto f x (nhds a)) (hg : filter.tendsto g x (nhds b)) :
filter.tendsto (λ (x : β), has_edist.edist (f x) (g x)) x (nhds (has_edist.edist a b))
theorem cauchy_seq_of_edist_le_of_tsum_ne_top {α : Type u_1} [pseudo_emetric_space α] {f : α} (d : ennreal) (hf : (n : ), has_edist.edist (f n) (f n.succ) d n) (hd : tsum d ) :
@[simp]
@[simp]
theorem metric.diam_closure {α : Type u_1} [pseudo_metric_space α] (s : set α) :
theorem is_closed_set_of_lipschitz_on_with {α : Type u_1} {β : Type u_2} [pseudo_emetric_space α] [pseudo_emetric_space β] (K : nnreal) (s : set α) :
is_closed {f : α β | lipschitz_on_with K f s}
theorem is_closed_set_of_lipschitz_with {α : Type u_1} {β : Type u_2} [pseudo_emetric_space α] [pseudo_emetric_space β] (K : nnreal) :
is_closed {f : α β | lipschitz_with K f}

For a bounded set s : set, its emetric.diam is equal to Sup s - Inf s reinterpreted as ℝ≥0∞.

For a bounded set s : set, its metric.diam is equal to Sup s - Inf s.

@[simp]
theorem real.ediam_Ioo (a b : ) :
@[simp]
theorem real.ediam_Icc (a b : ) :
@[simp]
theorem real.ediam_Ico (a b : ) :
@[simp]
theorem real.ediam_Ioc (a b : ) :
theorem real.diam_Icc {a b : } (h : a b) :
theorem real.diam_Ico {a b : } (h : a b) :
theorem real.diam_Ioc {a b : } (h : a b) :
theorem real.diam_Ioo {a b : } (h : a b) :
theorem edist_le_tsum_of_edist_le_of_tendsto {α : Type u_1} [pseudo_emetric_space α] {f : α} (d : ennreal) (hf : (n : ), has_edist.edist (f n) (f n.succ) d n) {a : α} (ha : filter.tendsto f filter.at_top (nhds a)) (n : ) :
has_edist.edist (f n) a ∑' (m : ), d (n + m)

If edist (f n) (f (n+1)) is bounded above by a function d : ℕ → ℝ≥0∞, 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} [pseudo_emetric_space α] {f : α} (d : ennreal) (hf : (n : ), has_edist.edist (f n) (f n.succ) d n) {a : α} (ha : filter.tendsto f filter.at_top (nhds a)) :
has_edist.edist (f 0) a ∑' (m : ), d m

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