topology.instances.ennreal

@[protected, instance]

noncomputable def ennreal.topological_space :

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

ennreal.topological_space = preorder.topology ennreal

source

@[protected, instance]

def ennreal.order_topology :

order_topology ennreal

source

@[protected, instance]

def ennreal.t2_space :

t2_space ennreal

source

@[protected, instance]

def ennreal.normal_space :

normal_space ennreal

source

@[protected, instance]

def ennreal.topological_space.second_countable_topology :

topological_space.second_countable_topology ennreal

source

theorem ennreal.embedding_coe :

embedding coe

source

theorem ennreal.is_open_ne_top :

is_open {a : ennreal | a ≠ ⊤}

source

theorem ennreal.is_open_Ico_zero {b : ennreal} :

is_open (set.Ico 0 b)

source

theorem ennreal.open_embedding_coe :

open_embedding coe

source

theorem ennreal.coe_range_mem_nhds {r : nnreal} :

set.range coe ∈ nhds ↑r

source

@[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)

source

theorem ennreal.continuous_coe :

continuous coe

source

theorem ennreal.continuous_coe_iff {α : Type u_1} [topological_space α] {f : α → nnreal} :

continuous (λ (a : α), ↑(f a)) ↔ continuous f

source

theorem ennreal.nhds_coe {r : nnreal} :

nhds ↑r = filter.map coe (nhds r)

source

theorem ennreal.tendsto_nhds_coe_iff {α : Type u_1} {l : filter α} {x : nnreal} {f : ennreal → α} :

filter.tendsto f (nhds ↑x) l ↔ filter.tendsto (f ∘ coe) (nhds x) l

source

theorem ennreal.continuous_at_coe_iff {α : Type u_1} [topological_space α] {x : nnreal} {f : ennreal → α} :

continuous_at f ↑x ↔ continuous_at (f ∘ coe) x

source

theorem ennreal.nhds_coe_coe {r p : nnreal} :

nhds (↑r, ↑p) = filter.map (λ (p : nnreal × nnreal), (↑(p.fst), ↑(p.snd))) (nhds (r, p))

source

theorem ennreal.continuous_of_real :

continuous ennreal.of_real

source

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

source

theorem ennreal.tendsto_to_nnreal {a : ennreal} (ha : a ≠ ⊤) :

filter.tendsto ennreal.to_nnreal (nhds a) (nhds a.to_nnreal)

source

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

source

theorem ennreal.continuous_on_to_nnreal :

continuous_on ennreal.to_nnreal {a : ennreal | a ≠ ⊤}

source

theorem ennreal.tendsto_to_real {a : ennreal} (ha : a ≠ ⊤) :

filter.tendsto ennreal.to_real (nhds a) (nhds a.to_real)

source

def ennreal.ne_top_homeomorph_nnreal :

↥{a : ennreal | a ≠ ⊤} ≃ₜ nnreal

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

Equations

ennreal.ne_top_homeomorph_nnreal = {to_equiv := {to_fun := ennreal.ne_top_equiv_nnreal.to_fun, inv_fun := ennreal.ne_top_equiv_nnreal.inv_fun, left_inv := ennreal.ne_top_homeomorph_nnreal._proof_1, right_inv := ennreal.ne_top_homeomorph_nnreal._proof_2}, continuous_to_fun := ennreal.ne_top_homeomorph_nnreal._proof_3, continuous_inv_fun := ennreal.ne_top_homeomorph_nnreal._proof_4}

source

noncomputable def ennreal.lt_top_homeomorph_nnreal :

↥{a : ennreal | a < ⊤} ≃ₜ nnreal

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

Equations

ennreal.lt_top_homeomorph_nnreal = (homeomorph.set_congr ennreal.lt_top_homeomorph_nnreal._proof_1).trans ennreal.ne_top_homeomorph_nnreal

source

theorem ennreal.nhds_top :

nhds ⊤ = ⨅ (a : ennreal) (H : a ≠ ⊤), filter.principal (set.Ioi a)

source

theorem ennreal.nhds_top' :

nhds ⊤ = ⨅ (r : nnreal), filter.principal (set.Ioi ↑r)

source

theorem ennreal.nhds_top_basis :

(nhds ⊤).has_basis (λ (a : ennreal), a < ⊤) (λ (a : ennreal), set.Ioi a)

source

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

source

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

source

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

filter.tendsto m f (nhds ⊤)

source

theorem ennreal.tendsto_nat_nhds_top :

filter.tendsto (λ (n : ℕ), ↑n) filter.at_top (nhds ⊤)

source

@[simp, norm_cast]

theorem ennreal.tendsto_coe_nhds_top {α : Type u_1} {f : α → nnreal} {l : filter α} :

filter.tendsto (λ (x : α), ↑(f x)) l (nhds ⊤) ↔ filter.tendsto f l filter.at_top

source

theorem ennreal.tendsto_of_real_at_top :

filter.tendsto ennreal.of_real filter.at_top (nhds ⊤)

source

theorem ennreal.nhds_zero :

nhds 0 = ⨅ (a : ennreal) (H : a ≠ 0), filter.principal (set.Iio a)

source

theorem ennreal.nhds_zero_basis :

(nhds 0).has_basis (λ (a : ennreal), 0 < a) (λ (a : ennreal), set.Iio a)

source

theorem ennreal.nhds_zero_basis_Iic :

(nhds 0).has_basis (λ (a : ennreal), 0 < a) set.Iic

source

@[instance]

theorem ennreal.nhds_within_Ioi_coe_ne_bot {r : nnreal} :

(nhds_within ↑r (set.Ioi ↑r)).ne_bot

source

@[instance]

theorem ennreal.nhds_within_Ioi_zero_ne_bot :

(nhds_within 0 (set.Ioi 0)).ne_bot

source

theorem ennreal.Icc_mem_nhds {x ε : ennreal} (xt : x ≠ ⊤) (ε0 : ε ≠ 0) :

set.Icc (x - ε) (x + ε) ∈ nhds x

source

theorem ennreal.nhds_of_ne_top {x : ennreal} (xt : x ≠ ⊤) :

nhds x = ⨅ (ε : ennreal) (H : ε > 0), filter.principal (set.Icc (x - ε) (x + ε))

source

@[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.

source

@[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 ≤ ε)

source

@[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 + ε))

source

@[protected, instance]

def ennreal.has_continuous_add :

has_continuous_add ennreal

source

@[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 ≤ ε)

source

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

source

@[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))

source

@[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))

source

@[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))

source

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

source

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)

source

@[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))

source

@[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))

source

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

source

@[protected]

theorem ennreal.continuous_at_const_mul {a b : ennreal} (h : a ≠ ⊤ ∨ b ≠ 0) :

continuous_at (has_mul.mul a) b

source

@[protected]

theorem ennreal.continuous_at_mul_const {a b : ennreal} (h : a ≠ ⊤ ∨ b ≠ 0) :

continuous_at (λ (x : ennreal), x * a) b

source

@[protected]

theorem ennreal.continuous_const_mul {a : ennreal} (ha : a ≠ ⊤) :

continuous (has_mul.mul a)

source

@[protected]

theorem ennreal.continuous_mul_const {a : ennreal} (ha : a ≠ ⊤) :

continuous (λ (x : ennreal), x * a)

source

@[protected]

theorem ennreal.continuous_div_const (c : ennreal) (c_ne_zero : c ≠ 0) :

continuous (λ (x : ennreal), x / c)

source

@[continuity]

theorem ennreal.continuous_pow (n : ℕ) :

continuous (λ (a : ennreal), a ^ n)

source

theorem ennreal.continuous_on_sub :

continuous_on (λ (p : ennreal × ennreal), p.fst - p.snd) {p : ennreal × ennreal | p ≠ (⊤, ⊤)}

source

theorem ennreal.continuous_sub_left {a : ennreal} (a_ne_top : a ≠ ⊤) :

continuous (λ (x : ennreal), a - x)

source

theorem ennreal.continuous_nnreal_sub {a : nnreal} :

continuous (λ (x : ennreal), ↑a - x)

source

theorem ennreal.continuous_on_sub_left (a : ennreal) :

continuous_on (λ (x : ennreal), a - x) {x : ennreal | x ≠ ⊤}

source

theorem ennreal.continuous_sub_right (a : ennreal) :

continuous (λ (x : ennreal), x - a)

source

@[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))

source

theorem ennreal.le_of_forall_lt_one_mul_le {x y : ennreal} (h : ∀ (a : ennreal), a < 1 → a * x ≤ y) :

x ≤ y

source

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

source

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

source

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

source

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

source

theorem ennreal.inv_map_infi {ι : Sort u_1} {x : ι → ennreal} :

(infi x)⁻¹ = ⨆ (i : ι), (x i)⁻¹

source

theorem ennreal.inv_map_supr {ι : Sort u_1} {x : ι → ennreal} :

(supr x)⁻¹ = ⨅ (i : ι), (x i)⁻¹

source

theorem ennreal.inv_limsup {ι : Type u_1} {x : ι → ennreal} {l : filter ι} :

(filter.limsup x l)⁻¹ = filter.liminf (λ (i : ι), (x i)⁻¹) l

source

theorem ennreal.inv_liminf {ι : Type u_1} {x : ι → ennreal} {l : filter ι} :

(filter.liminf x l)⁻¹ = filter.limsup (λ (i : ι), (x i)⁻¹) l

source

@[protected, instance]

def ennreal.has_continuous_inv :

has_continuous_inv ennreal

source

@[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)

source

@[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))

source

@[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))

source

@[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))

source

@[protected]

theorem ennreal.tendsto_inv_nat_nhds_zero :

filter.tendsto (λ (n : ℕ), (↑n)⁻¹) filter.at_top (nhds 0)

source

theorem ennreal.supr_add {a : ennreal} {ι : Sort u_1} {s : ι → ennreal} [h : nonempty ι] :

supr s + a = ⨆ (b : ι), s b + a

source

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

source

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

source

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

source

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

source

theorem ennreal.Sup_add {a : ennreal} {s : set ennreal} (hs : s.nonempty) :

has_Sup.Sup s + a = ⨆ (b : ennreal) (H : b ∈ s), b + a

source

theorem ennreal.add_supr {a : ennreal} {ι : Sort u_1} {s : ι → ennreal} [nonempty ι] :

a + supr s = ⨆ (b : ι), a + s b

source

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

source

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

source

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

source

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

source

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

source

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)

source

theorem ennreal.mul_supr {ι : Sort u_1} {f : ι → ennreal} {a : ennreal} :

a * supr f = ⨆ (i : ι), a * f i

source

theorem ennreal.mul_Sup {s : set ennreal} {a : ennreal} :

a * has_Sup.Sup s = ⨆ (i : ennreal) (H : i ∈ s), a * i

source

theorem ennreal.supr_mul {ι : Sort u_1} {f : ι → ennreal} {a : ennreal} :

supr f * a = ⨆ (i : ι), f i * a

source

theorem ennreal.smul_supr {ι : Sort u_1} {R : Type u_2} [has_smul R ennreal] [is_scalar_tower R ennreal ennreal] (f : ι → ennreal) (c : R) :

(c • ⨆ (i : ι), f i) = ⨆ (i : ι), c • f i

source

theorem ennreal.smul_Sup {R : Type u_1} [has_smul R ennreal] [is_scalar_tower R ennreal ennreal] (s : set ennreal) (c : R) :

c • has_Sup.Sup s = ⨆ (i : ennreal) (H : i ∈ s), c • i

source

theorem ennreal.supr_div {ι : Sort u_1} {f : ι → ennreal} {a : ennreal} :

supr f / a = ⨆ (i : ι), f i / a

source

@[protected]

theorem ennreal.tendsto_coe_sub {r : nnreal} {b : ennreal} :

filter.tendsto (λ (b : ennreal), ↑r - b) (nhds b) (nhds (↑r - b))

source

theorem ennreal.sub_supr {a : ennreal} {ι : Sort u_1} [nonempty ι] {b : ι → ennreal} (hr : a < ⊤) :

(a - ⨆ (i : ι), b i) = ⨅ (i : ι), a - b i

source

theorem ennreal.exists_countable_dense_no_zero_top :

∃ (s : set ennreal), s.countable ∧ dense s ∧ 0 ∉ s ∧ ⊤ ∉ s

source

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'

source

theorem ennreal.exists_frequently_lt_of_liminf_ne_top {ι : Type u_1} {l : filter ι} {x : ι → ℝ} (hx : filter.liminf (λ (n : ι), ↑(⇑real.nnabs (x n))) l ≠ ⊤) :

∃ (R : ℝ), ∃ᶠ (n : ι) in l, x n < R

source

theorem ennreal.exists_frequently_lt_of_liminf_ne_top' {ι : Type u_1} {l : filter ι} {x : ι → ℝ} (hx : filter.liminf (λ (n : ι), ↑(⇑real.nnabs (x n))) l ≠ ⊤) :

∃ (R : ℝ), ∃ᶠ (n : ι) in l, R < x n

source

theorem ennreal.exists_upcrossings_of_not_bounded_under {ι : Type u_1} {l : filter ι} {x : ι → ℝ} (hf : filter.liminf (λ (i : ι), ↑(⇑real.nnabs (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

source

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

source

@[protected]

theorem ennreal.tsum_coe_eq {α : Type u_1} {r : nnreal} {f : α → nnreal} (h : has_sum f r) :

∑' (a : α), ↑(f a) = ↑r

source

@[protected]

theorem ennreal.coe_tsum {α : Type u_1} {f : α → nnreal} :

summable f → ↑(tsum f) = ∑' (a : α), ↑(f a)

source

@[protected]

theorem ennreal.has_sum {α : Type u_1} {f : α → ennreal} :

has_sum f (⨆ (s : finset α), s.sum (λ (a : α), f a))

source

@[protected, simp]

theorem ennreal.summable {α : Type u_1} {f : α → ennreal} :

summable f

source

theorem ennreal.tsum_coe_ne_top_iff_summable {β : Type u_2} {f : β → nnreal} :

∑' (b : β), ↑(f b) ≠ ⊤ ↔ summable f

source

@[protected]

theorem ennreal.tsum_eq_supr_sum {α : Type u_1} {f : α → ennreal} :

∑' (a : α), f a = ⨆ (s : finset α), s.sum (λ (a : α), f a)

source

@[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)

source

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

source

@[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⟩

source

@[protected]

theorem ennreal.tsum_prod {α : Type u_1} {β : Type u_2} {f : α → β → ennreal} :

∑' (p : α × β), f p.fst p.snd = ∑' (a : α) (b : β), f a b

source

@[protected]

theorem ennreal.tsum_prod' {α : Type u_1} {β : Type u_2} {f : α × β → ennreal} :

∑' (p : α × β), f p = ∑' (a : α) (b : β), f (a, b)

source

@[protected]

theorem ennreal.tsum_comm {α : Type u_1} {β : Type u_2} {f : α → β → ennreal} :

∑' (a : α) (b : β), f a b = ∑' (b : β) (a : α), f a b

source

@[protected]

theorem ennreal.tsum_add {α : Type u_1} {f g : α → ennreal} :

∑' (a : α), (f a + g a) = ∑' (a : α), f a + ∑' (a : α), g a

source

@[protected]

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

∑' (a : α), f a ≤ ∑' (a : α), g a

source

@[protected]

theorem ennreal.sum_le_tsum {α : Type u_1} {f : α → ennreal} (s : finset α) :

s.sum (λ (x : α), f x) ≤ ∑' (x : α), f x

source

@[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)

source

@[protected]

theorem ennreal.tsum_eq_supr_nat {f : ℕ → ennreal} :

∑' (i : ℕ), f i = ⨆ (i : ℕ), (finset.range i).sum (λ (a : ℕ), f a)

source

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

source

@[protected]

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

f a ≤ ∑' (a : α), f a

source

@[protected, simp]

theorem ennreal.tsum_eq_zero {α : Type u_1} {f : α → ennreal} :

∑' (i : α), f i = 0 ↔ ∀ (i : α), f i = 0

source

@[protected]

theorem ennreal.tsum_eq_top_of_eq_top {α : Type u_1} {f : α → ennreal} :

(∃ (a : α), f a = ⊤) → ∑' (a : α), f a = ⊤

source

@[protected]

theorem ennreal.lt_top_of_tsum_ne_top {α : Type u_1} {a : α → ennreal} (tsum_ne_top : ∑' (i : α), a i ≠ ⊤) (j : α) :

a j < ⊤

source

@[protected, simp]

theorem ennreal.tsum_top {α : Type u_1} [nonempty α] :

∑' (a : α), ⊤ = ⊤

source

theorem ennreal.tsum_const_eq_top_of_ne_zero {α : Type u_1} [infinite α] {c : ennreal} (hc : c ≠ 0) :

∑' (a : α), c = ⊤

source

@[protected]

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

f a ≠ ⊤

source

@[protected]

theorem ennreal.tsum_mul_left {α : Type u_1} {a : ennreal} {f : α → ennreal} :

∑' (i : α), a * f i = a * ∑' (i : α), f i

source

@[protected]

theorem ennreal.tsum_mul_right {α : Type u_1} {a : ennreal} {f : α → ennreal} :

∑' (i : α), f i * a = (∑' (i : α), f i) * a

source

@[protected]

theorem ennreal.tsum_const_smul {α : Type u_1} {f : α → ennreal} {R : Type u_2} [has_smul R ennreal] [is_scalar_tower R ennreal ennreal] (a : R) :

∑' (i : α), a • f i = a • ∑' (i : α), f i

source

@[simp]

theorem ennreal.tsum_supr_eq {α : Type u_1} (a : α) {f : α → ennreal} :

(∑' (b : α), ⨆ (h : a = b), f b) = f a

source

theorem ennreal.has_sum_iff_tendsto_nat {f : ℕ → ennreal} (r : ennreal) :

has_sum f r ↔ filter.tendsto (λ (n : ℕ), (finset.range n).sum (λ (i : ℕ), f i)) filter.at_top (nhds r)

source

theorem ennreal.tendsto_nat_tsum (f : ℕ → ennreal) :

filter.tendsto (λ (n : ℕ), (finset.range n).sum (λ (i : ℕ), f i)) filter.at_top (nhds (∑' (n : ℕ), f n))

source

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

↑((ennreal.to_nnreal ∘ f) x) = f x

source

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

summable (ennreal.to_nnreal ∘ f)

source

theorem ennreal.tendsto_cofinite_zero_of_tsum_ne_top {α : Type u_1} {f : α → ennreal} (hf : ∑' (x : α), f x ≠ ⊤) :

filter.tendsto f filter.cofinite (nhds 0)

source

theorem ennreal.tendsto_at_top_zero_of_tsum_ne_top {f : ℕ → ennreal} (hf : ∑' (x : ℕ), f x ≠ ⊤) :

filter.tendsto f filter.at_top (nhds 0)

source

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.

source

@[protected]

theorem ennreal.tsum_apply {ι : Type u_1} {α : Type u_2} {f : ι → α → ennreal} {x : α} :

(∑' (i : ι), f i) x = ∑' (i : ι), f i x

source

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

source

theorem ennreal.tsum_mono_subtype {α : Type u_1} (f : α → ennreal) {s t : set α} (h : s ⊆ t) :

∑' (x : ↥s), f ↑x ≤ ∑' (x : ↥t), f ↑x

source

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

source

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)

source

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)

source

theorem ennreal.tsum_eq_add_tsum_ite {β : Type u_2} {f : β → ennreal} (b : β) :

∑' (x : β), f x = f b + ∑' (x : β), ite (x = b) 0 (f x)

source

theorem ennreal.tsum_add_one_eq_top {f : ℕ → ennreal} (hf : ∑' (n : ℕ), f n = ⊤) (hf0 : f 0 ≠ ⊤) :

∑' (n : ℕ), f (n + 1) = ⊤

source

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.

source

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

source

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)

source

theorem ennreal.tsum_coe_ne_top_iff_summable_coe {α : Type u_1} {f : α → nnreal} :

∑' (a : α), ↑(f a) ≠ ⊤ ↔ summable (λ (a : α), ↑(f a))

source

theorem ennreal.tsum_coe_eq_top_iff_not_summable_coe {α : Type u_1} {f : α → nnreal} :

∑' (a : α), ↑(f a) = ⊤ ↔ ¬summable (λ (a : α), ↑(f a))

source

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)

source

theorem ennreal.summable_to_real {α : Type u_1} {f : α → ennreal} (hsum : ∑' (x : α), f x ≠ ⊤) :

summable (λ (x : α), (f x).to_real)

source

theorem nnreal.tsum_eq_to_nnreal_tsum {β : Type u_2} {f : β → nnreal} :

∑' (b : β), f b = (∑' (b : β), ↑(f b)).to_nnreal

source

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.

source

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

summable f → summable g

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

source

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.

source

theorem nnreal.not_summable_iff_tendsto_nat_at_top {f : ℕ → nnreal} :

¬summable f ↔ filter.tendsto (λ (n : ℕ), (finset.range n).sum (λ (i : ℕ), f i)) filter.at_top filter.at_top

source

theorem nnreal.summable_iff_not_tendsto_nat_at_top {f : ℕ → nnreal} :

summable f ↔ ¬filter.tendsto (λ (n : ℕ), (finset.range n).sum (λ (i : ℕ), f i)) filter.at_top filter.at_top

source

theorem nnreal.summable_of_sum_range_le {f : ℕ → nnreal} {c : nnreal} (h : ∀ (n : ℕ), (finset.range n).sum (λ (i : ℕ), f i) ≤ c) :

summable f

source

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

source

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

source

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

source

theorem nnreal.indicator_summable {α : Type u_1} {f : α → nnreal} (hf : summable f) (s : set α) :

summable (s.indicator f)

source

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

source

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.

source

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

source

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

source

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

source

theorem nnreal.tsum_strict_mono {α : Type u_1} {f g : α → nnreal} (hg : summable g) (h : f < g) :

∑' (n : α), f n < ∑' (n : α), g n

source

theorem nnreal.tsum_pos {α : Type u_1} {g : α → nnreal} (hg : summable g) (i : α) (hi : 0 < g i) :

0 < ∑' (b : α), g b

source

theorem nnreal.tsum_eq_add_tsum_ite {α : Type u_1} {f : α → nnreal} (hf : summable f) (i : α) :

∑' (x : α), f x = f i + ∑' (x : α), ite (x = i) 0 (f x)

source

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

source

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

source

theorem ennreal.tendsto_sum_nat_add (f : ℕ → ennreal) (hf : ∑' (i : ℕ), f i ≠ ⊤) :

filter.tendsto (λ (i : ℕ), ∑' (k : ℕ), f (k + i)) filter.at_top (nhds 0)

source

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

source

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

source

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

source

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

source

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

summable g

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

source

theorem summable.to_nnreal {α : Type u_1} {f : α → ℝ} (hf : summable f) :

summable (λ (n : α), (f n).to_nnreal)

source

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.

source

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)

source

theorem not_summable_iff_tendsto_nat_at_top_of_nonneg {f : ℕ → ℝ} (hf : ∀ (n : ℕ), 0 ≤ f n) :

¬summable f ↔ filter.tendsto (λ (n : ℕ), (finset.range n).sum (λ (i : ℕ), f i)) filter.at_top filter.at_top

source

theorem summable_iff_not_tendsto_nat_at_top_of_nonneg {f : ℕ → ℝ} (hf : ∀ (n : ℕ), 0 ≤ f n) :

summable f ↔ ¬filter.tendsto (λ (n : ℕ), (finset.range n).sum (λ (i : ℕ), f i)) filter.at_top filter.at_top

source

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

source

theorem summable_of_sum_le {ι : Type u_1} {f : ι → ℝ} {c : ℝ} (hf : 0 ≤ f) (h : ∀ (u : finset ι), u.sum (λ (x : ι), f x) ≤ c) :

summable f

source

theorem summable_of_sum_range_le {f : ℕ → ℝ} {c : ℝ} (hf : ∀ (n : ℕ), 0 ≤ f n) (h : ∀ (n : ℕ), (finset.range n).sum (λ (i : ℕ), f i) ≤ c) :

summable f

source

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

source

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.

source

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

has_edist.edist x.val y.val ≠ ⊤

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

source

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

metric_space ↥(emetric.ball a r)

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

Equations

metric_space_emetric_ball a r = emetric_space.to_metric_space edist_ne_top_of_mem_ball

source

theorem nhds_eq_nhds_emetric_ball {β : Type u_2} [emetric_space β] (a x : β) (r : ennreal) (h : x ∈ emetric.ball a r) :

nhds x = filter.map coe (nhds ⟨x, h⟩)

source

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)

source

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.

source

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

continuous f

source

theorem continuous_edist {α : Type u_1} [pseudo_emetric_space α] :

continuous (λ (p : α × α), has_edist.edist p.fst p.snd)

source

@[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))

source

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

source

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

cauchy_seq f

source

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

is_closed (emetric.closed_ball a r)

source

@[simp]

theorem emetric.diam_closure {α : Type u_1} [pseudo_emetric_space α] (s : set α) :

emetric.diam (closure s) = emetric.diam s

source

@[simp]

theorem metric.diam_closure {α : Type u_1} [pseudo_metric_space α] (s : set α) :

metric.diam (closure s) = metric.diam s

source

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}

source

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}

source

theorem real.ediam_eq {s : set ℝ} (h : metric.bounded s) :

emetric.diam s = ennreal.of_real (has_Sup.Sup s - has_Inf.Inf s)

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

source

theorem real.diam_eq {s : set ℝ} (h : metric.bounded s) :

metric.diam s = has_Sup.Sup s - has_Inf.Inf s

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

source

@[simp]

theorem real.ediam_Ioo (a b : ℝ) :

emetric.diam (set.Ioo a b) = ennreal.of_real (b - a)

source

@[simp]

theorem real.ediam_Icc (a b : ℝ) :

emetric.diam (set.Icc a b) = ennreal.of_real (b - a)

source

@[simp]

theorem real.ediam_Ico (a b : ℝ) :

emetric.diam (set.Ico a b) = ennreal.of_real (b - a)

source

@[simp]

theorem real.ediam_Ioc (a b : ℝ) :

emetric.diam (set.Ioc a b) = ennreal.of_real (b - a)

source

theorem real.diam_Icc {a b : ℝ} (h : a ≤ b) :

metric.diam (set.Icc a b) = b - a

source

theorem real.diam_Ico {a b : ℝ} (h : a ≤ b) :

metric.diam (set.Ico a b) = b - a

source

theorem real.diam_Ioc {a b : ℝ} (h : a ≤ b) :

metric.diam (set.Ioc a b) = b - a

source

theorem real.diam_Ioo {a b : ℝ} (h : a ≤ b) :

metric.diam (set.Ioo a b) = b - a

source

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.

source

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.

mathlib3 documentation

Extended non-negative reals #