Topology on extended non-negative reals

instance ENNReal.instTopologicalSpace : TopologicalSpace ENNReal

Topology on ℝ≥0∞.

Note: this is different from the EMetricSpace topology. The EMetricSpace topology has IsOpen {∞}, while this topology doesn't have singleton elements.

Equations

• ENNReal.instTopologicalSpace = Preorder.topology ENNReal

instance ENNReal.instOrderTopology : OrderTopology ENNReal

Equations

• ENNReal.instOrderTopology = ⋯

instance ENNReal.instT2Space : T2Space ENNReal

Equations

• ENNReal.instT2Space = ⋯

instance ENNReal.instT5Space : T5Space ENNReal

Equations

• ENNReal.instT5Space = ⋯

instance ENNReal.instT4Space : T4Space ENNReal

Equations

• ENNReal.instT4Space = ⋯

instance ENNReal.instSecondCountableTopology : SecondCountableTopology ENNReal

Equations

• ENNReal.instSecondCountableTopology = ⋯

instance ENNReal.instMetrizableSpace : TopologicalSpace.MetrizableSpace ENNReal

Equations

• ENNReal.instMetrizableSpace = ⋯

theorem ENNReal.embedding_coe : Embedding ENNReal.ofNNReal

theorem ENNReal.isOpen_ne_top : IsOpen {a : ENNReal | a ≠ ⊤}

theorem ENNReal.isOpen_Ico_zero {b : ENNReal} : IsOpen (Set.Ico 0 b)

theorem ENNReal.openEmbedding_coe : OpenEmbedding ENNReal.ofNNReal

theorem ENNReal.coe_range_mem_nhds {r : NNReal} : Set.range ENNReal.ofNNReal ∈ nhds ↑r

theorem ENNReal.tendsto_coe {α : Type u_1} {f : Filter α} {m : α → NNReal} {a : NNReal} : Filter.Tendsto (fun (a : α) => ↑(m a)) f (nhds ↑a) ↔ Filter.Tendsto m f (nhds a)

theorem ENNReal.continuous_coe : Continuous ENNReal.ofNNReal

theorem ENNReal.continuous_coe_iff {α : Type u_4} [TopologicalSpace α] {f : α → NNReal} : (Continuous fun (a : α) => ↑(f a)) ↔ Continuous f

theorem ENNReal.nhds_coe {r : NNReal} : nhds ↑r = Filter.map ENNReal.ofNNReal (nhds r)

theorem ENNReal.tendsto_nhds_coe_iff {α : Type u_4} {l : Filter α} {x : NNReal} {f : ENNReal → α} : Filter.Tendsto f (nhds ↑x) l ↔ Filter.Tendsto (f ∘ ENNReal.ofNNReal) (nhds x) l

theorem ENNReal.continuousAt_coe_iff {α : Type u_4} [TopologicalSpace α] {x : NNReal} {f : ENNReal → α} : ContinuousAt f ↑x ↔ ContinuousAt (f ∘ ENNReal.ofNNReal) x

theorem ENNReal.nhds_coe_coe {r : NNReal} {p : NNReal} : nhds (↑r, ↑p) = Filter.map (fun (p : NNReal × NNReal) => (↑p.1, ↑p.2)) (nhds (r, p))

theorem ENNReal.continuous_ofReal : Continuous ENNReal.ofReal

theorem ENNReal.tendsto_ofReal {α : Type u_1} {f : Filter α} {m : α → ℝ} {a : ℝ} (h : Filter.Tendsto m f (nhds a)) : Filter.Tendsto (fun (a : α) => ENNReal.ofReal (m a)) f (nhds (ENNReal.ofReal a))

theorem ENNReal.tendsto_toNNReal {a : ENNReal} (ha : a ≠ ⊤) : Filter.Tendsto ENNReal.toNNReal (nhds a) (nhds a.toNNReal)

theorem ENNReal.eventuallyEq_of_toReal_eventuallyEq {α : Type u_1} {l : Filter α} {f : α → ENNReal} {g : α → ENNReal} (hfi : ∀ᶠ (x : α) in l, f x ≠ ⊤) (hgi : ∀ᶠ (x : α) in l, g x ≠ ⊤) (hfg : (fun (x : α) => (f x).toReal) =ᶠ[l] fun (x : α) => (g x).toReal) : f =ᶠ[l] g

theorem ENNReal.continuousOn_toNNReal : ContinuousOn ENNReal.toNNReal {a : ENNReal | a ≠ ⊤}

theorem ENNReal.tendsto_toReal {a : ENNReal} (ha : a ≠ ⊤) : Filter.Tendsto ENNReal.toReal (nhds a) (nhds a.toReal)

theorem ENNReal.continuousOn_toReal : ContinuousOn ENNReal.toReal {a : ENNReal | a ≠ ⊤}

theorem ENNReal.continuousAt_toReal {x : ENNReal} (hx : x ≠ ⊤) : ContinuousAt ENNReal.toReal x

def ENNReal.neTopHomeomorphNNReal : ↑{a : ENNReal | a ≠ ⊤} ≃ₜ NNReal

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

Equations

• ENNReal.neTopHomeomorphNNReal = { toEquiv := ENNReal.neTopEquivNNReal, continuous_toFun := ENNReal.neTopHomeomorphNNReal.proof_1, continuous_invFun := ENNReal.neTopHomeomorphNNReal.proof_2 }

def ENNReal.ltTopHomeomorphNNReal : ↑{a : ENNReal | a < ⊤} ≃ₜ NNReal

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

Equations

• ENNReal.ltTopHomeomorphNNReal = (Homeomorph.setCongr ENNReal.ltTopHomeomorphNNReal.proof_1).trans ENNReal.neTopHomeomorphNNReal

theorem ENNReal.nhds_top : nhds ⊤ = ⨅ (a : ENNReal), ⨅ (_ : a ≠ ⊤), Filter.principal (Set.Ioi a)

theorem ENNReal.nhds_top' : nhds ⊤ = ⨅ (r : NNReal), Filter.principal (Set.Ioi ↑r)

theorem ENNReal.nhds_top_basis : (nhds ⊤).HasBasis (fun (a : ENNReal) => a < ⊤) fun (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) : Filter.Tendsto m f (nhds ⊤)

theorem ENNReal.tendsto_nat_nhds_top : Filter.Tendsto (fun (n : ℕ) => ↑n) Filter.atTop (nhds ⊤)

@[simp]

theorem ENNReal.tendsto_coe_nhds_top {α : Type u_1} {f : α → NNReal} {l : Filter α} : Filter.Tendsto (fun (x : α) => ↑(f x)) l (nhds ⊤) ↔ Filter.Tendsto f l Filter.atTop

theorem ENNReal.tendsto_ofReal_atTop : Filter.Tendsto ENNReal.ofReal Filter.atTop (nhds ⊤)

theorem ENNReal.nhds_zero : nhds 0 = ⨅ (a : ENNReal), ⨅ (_ : a ≠ 0), Filter.principal (Set.Iio a)

theorem ENNReal.nhds_zero_basis : (nhds 0).HasBasis (fun (a : ENNReal) => 0 < a) fun (a : ENNReal) => Set.Iio a

theorem ENNReal.nhds_zero_basis_Iic : (nhds 0).HasBasis (fun (a : ENNReal) => 0 < a) Set.Iic

theorem ENNReal.nhdsWithin_Ioi_coe_neBot {r : NNReal} : (nhdsWithin (↑r) (Set.Ioi ↑r)).NeBot

theorem ENNReal.nhdsWithin_Ioi_zero_neBot : (nhdsWithin 0 (Set.Ioi 0)).NeBot

theorem ENNReal.nhdsWithin_Ioi_one_neBot : (nhdsWithin 1 (Set.Ioi 1)).NeBot

theorem ENNReal.nhdsWithin_Ioi_nat_neBot (n : ℕ) : (nhdsWithin (↑n) (Set.Ioi ↑n)).NeBot

theorem ENNReal.nhdsWithin_Ioi_ofNat_nebot (n : ℕ) [n.AtLeastTwo] : (nhdsWithin (OfNat.ofNat n) (Set.Ioi (OfNat.ofNat n))).NeBot

theorem ENNReal.nhdsWithin_Iio_neBot {x : ENNReal} [NeZero x] : (nhdsWithin x (Set.Iio x)).NeBot

theorem ENNReal.hasBasis_nhds_of_ne_top' {x : ENNReal} (xt : x ≠ ⊤) : (nhds x).HasBasis (fun (x : ENNReal) => x ≠ 0) fun (ε : ENNReal) => Set.Icc (x - ε) (x + ε)

Closed intervals Set.Icc (x - ε) (x + ε), ε ≠ 0, form a basis of neighborhoods of an extended nonnegative real number x ≠ ∞. We use Set.Icc instead of Set.Ioo because this way the statement works for x = 0.

theorem ENNReal.hasBasis_nhds_of_ne_top {x : ENNReal} (xt : x ≠ ⊤) : (nhds x).HasBasis (fun (x : ENNReal) => 0 < x) fun (ε : ENNReal) => Set.Icc (x - ε) (x + ε)

theorem ENNReal.Icc_mem_nhds {x : ENNReal} {ε : ENNReal} (xt : x ≠ ⊤) (ε0 : ε ≠ 0) : Set.Icc (x - ε) (x + ε) ∈ nhds x

theorem ENNReal.nhds_of_ne_top {x : ENNReal} (xt : x ≠ ⊤) : nhds x = ⨅ (ε : ENNReal), ⨅ (_ : ε > 0), Filter.principal (Set.Icc (x - ε) (x + ε))

theorem ENNReal.biInf_le_nhds (x : ENNReal) : ⨅ (ε : ENNReal), ⨅ (_ : ε > 0), Filter.principal (Set.Icc (x - ε) (x + ε)) ≤ nhds x

theorem ENNReal.tendsto_nhds_of_Icc {α : Type u_1} {f : Filter α} {u : α → ENNReal} {a : ENNReal} (h : ∀ ε > 0, ∀ᶠ (x : α) in f, u x ∈ Set.Icc (a - ε) (a + ε)) : Filter.Tendsto u f (nhds a)

theorem ENNReal.tendsto_nhds {α : Type u_1} {f : Filter α} {u : α → ENNReal} {a : ENNReal} (ha : a ≠ ⊤) : Filter.Tendsto u f (nhds a) ↔ ∀ ε > 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.

theorem ENNReal.tendsto_nhds_zero {α : Type u_1} {f : Filter α} {u : α → ENNReal} : Filter.Tendsto u f (nhds 0) ↔ ∀ ε > 0, ∀ᶠ (x : α) in f, u x ≤ ε

theorem ENNReal.tendsto_atTop {β : Type u_2} [Nonempty β] [SemilatticeSup β] {f : β → ENNReal} {a : ENNReal} (ha : a ≠ ⊤) : Filter.Tendsto f Filter.atTop (nhds a) ↔ ∀ ε > 0, ∃ (N : β), ∀ n ≥ N, f n ∈ Set.Icc (a - ε) (a + ε)

instance ENNReal.instContinuousAdd : ContinuousAdd ENNReal

Equations

• ENNReal.instContinuousAdd = ⋯

theorem ENNReal.tendsto_atTop_zero {β : Type u_2} [Nonempty β] [SemilatticeSup β] {f : β → ENNReal} : Filter.Tendsto f Filter.atTop (nhds 0) ↔ ∀ ε > 0, ∃ (N : β), ∀ n ≥ N, f n ≤ ε

theorem ENNReal.tendsto_sub {a : ENNReal} {b : ENNReal} : a ≠ ⊤ ∨ b ≠ ⊤ → Filter.Tendsto (fun (p : ENNReal × ENNReal) => p.1 - p.2) (nhds (a, b)) (nhds (a - b))

theorem ENNReal.Tendsto.sub {α : Type u_1} {f : Filter α} {ma : α → ENNReal} {mb : α → ENNReal} {a : ENNReal} {b : ENNReal} (hma : Filter.Tendsto ma f (nhds a)) (hmb : Filter.Tendsto mb f (nhds b)) (h : a ≠ ⊤ ∨ b ≠ ⊤) : Filter.Tendsto (fun (a : α) => ma a - mb a) f (nhds (a - b))

theorem ENNReal.tendsto_mul {a : ENNReal} {b : ENNReal} (ha : a ≠ 0 ∨ b ≠ ⊤) (hb : b ≠ 0 ∨ a ≠ ⊤) : Filter.Tendsto (fun (p : ENNReal × ENNReal) => p.1 * p.2) (nhds (a, b)) (nhds (a * b))

theorem ENNReal.Tendsto.mul {α : Type u_1} {f : Filter α} {ma : α → ENNReal} {mb : α → ENNReal} {a : ENNReal} {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 (fun (a : α) => ma a * mb a) f (nhds (a * b))

theorem ContinuousOn.ennreal_mul {α : Type u_1} [TopologicalSpace α] {f : α → ENNReal} {g : α → ENNReal} {s : Set α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) (h₁ : ∀ x ∈ s, f x ≠ 0 ∨ g x ≠ ⊤) (h₂ : ∀ x ∈ s, g x ≠ 0 ∨ f x ≠ ⊤) : ContinuousOn (fun (x : α) => f x * g x) s

theorem Continuous.ennreal_mul {α : Type u_1} [TopologicalSpace α] {f : α → ENNReal} {g : α → ENNReal} (hf : Continuous f) (hg : Continuous g) (h₁ : ∀ (x : α), f x ≠ 0 ∨ g x ≠ ⊤) (h₂ : ∀ (x : α), g x ≠ 0 ∨ f x ≠ ⊤) : Continuous fun (x : α) => f x * g x

theorem ENNReal.Tendsto.const_mul {α : Type u_1} {f : Filter α} {m : α → ENNReal} {a : ENNReal} {b : ENNReal} (hm : Filter.Tendsto m f (nhds b)) (hb : b ≠ 0 ∨ a ≠ ⊤) : Filter.Tendsto (fun (b : α) => a * m b) f (nhds (a * b))

theorem ENNReal.Tendsto.mul_const {α : Type u_1} {f : Filter α} {m : α → ENNReal} {a : ENNReal} {b : ENNReal} (hm : Filter.Tendsto m f (nhds a)) (ha : a ≠ 0 ∨ b ≠ ⊤) : Filter.Tendsto (fun (x : α) => m x * b) f (nhds (a * b))

theorem ENNReal.tendsto_finset_prod_of_ne_top {α : Type u_1} {ι : Type u_4} {f : ι → α → ENNReal} {x : Filter α} {a : ι → ENNReal} (s : Finset ι) (h : ∀ i ∈ s, Filter.Tendsto (f i) x (nhds (a i))) (h' : ∀ i ∈ s, a i ≠ ⊤) : Filter.Tendsto (fun (b : α) => s.prod fun (c : ι) => f c b) x (nhds (s.prod fun (c : ι) => a c))

theorem ENNReal.continuousAt_const_mul {a : ENNReal} {b : ENNReal} (h : a ≠ ⊤ ∨ b ≠ 0) : ContinuousAt (fun (x : ENNReal) => a * x) b

theorem ENNReal.continuousAt_mul_const {a : ENNReal} {b : ENNReal} (h : a ≠ ⊤ ∨ b ≠ 0) : ContinuousAt (fun (x : ENNReal) => x * a) b

theorem ENNReal.continuous_const_mul {a : ENNReal} (ha : a ≠ ⊤) : Continuous fun (x : ENNReal) => a * x

theorem ENNReal.continuous_mul_const {a : ENNReal} (ha : a ≠ ⊤) : Continuous fun (x : ENNReal) => x * a

theorem ENNReal.continuous_div_const (c : ENNReal) (c_ne_zero : c ≠ 0) : Continuous fun (x : ENNReal) => x / c

theorem ENNReal.continuous_pow (n : ℕ) : Continuous fun (a : ENNReal) => a ^ n

theorem ENNReal.continuousOn_sub : ContinuousOn (fun (p : ENNReal × ENNReal) => p.1 - p.2) {p : ENNReal × ENNReal | p ≠ (⊤, ⊤)}

theorem ENNReal.continuous_sub_left {a : ENNReal} (a_ne_top : a ≠ ⊤) : Continuous fun (x : ENNReal) => a - x

theorem ENNReal.continuous_nnreal_sub {a : NNReal} : Continuous fun (x : ENNReal) => ↑a - x

theorem ENNReal.continuousOn_sub_left (a : ENNReal) : ContinuousOn (fun (x : ENNReal) => a - x) {x : ENNReal | x ≠ ⊤}

theorem ENNReal.continuous_sub_right (a : ENNReal) : Continuous fun (x : ENNReal) => x - a

theorem ENNReal.Tendsto.pow {α : Type u_1} {f : Filter α} {m : α → ENNReal} {a : ENNReal} {n : ℕ} (hm : Filter.Tendsto m f (nhds a)) : Filter.Tendsto (fun (x : α) => m x ^ n) f (nhds (a ^ n))

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

theorem ENNReal.iInf_mul_left' {ι : Sort u_4} {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.iInf_mul_left {ι : Sort u_4} [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.iInf_mul_right' {ι : Sort u_4} {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.iInf_mul_right {ι : Sort u_4} [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_iInf {ι : Sort u_4} {x : ι → ENNReal} : (iInf x)⁻¹ = ⨆ (i : ι), (x i)⁻¹

theorem ENNReal.inv_map_iSup {ι : Sort u_4} {x : ι → ENNReal} : (iSup x)⁻¹ = ⨅ (i : ι), (x i)⁻¹

theorem ENNReal.inv_limsup {ι : Type u_4} {x : ι → ENNReal} {l : Filter ι} : (Filter.limsup x l)⁻¹ = Filter.liminf (fun (i : ι) => (x i)⁻¹) l

theorem ENNReal.inv_liminf {ι : Type u_4} {x : ι → ENNReal} {l : Filter ι} : (Filter.liminf x l)⁻¹ = Filter.limsup (fun (i : ι) => (x i)⁻¹) l

instance ENNReal.instContinuousInv : ContinuousInv ENNReal

Equations

• ENNReal.instContinuousInv = ⋯

@[simp]

theorem ENNReal.tendsto_inv_iff {α : Type u_1} {f : Filter α} {m : α → ENNReal} {a : ENNReal} : Filter.Tendsto (fun (x : α) => (m x)⁻¹) f (nhds a⁻¹) ↔ Filter.Tendsto m f (nhds a)

theorem ENNReal.Tendsto.div {α : Type u_1} {f : Filter α} {ma : α → ENNReal} {mb : α → ENNReal} {a : ENNReal} {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 (fun (a : α) => ma a / mb a) f (nhds (a / b))

theorem ENNReal.Tendsto.const_div {α : Type u_1} {f : Filter α} {m : α → ENNReal} {a : ENNReal} {b : ENNReal} (hm : Filter.Tendsto m f (nhds b)) (hb : b ≠ ⊤ ∨ a ≠ ⊤) : Filter.Tendsto (fun (b : α) => a / m b) f (nhds (a / b))

theorem ENNReal.Tendsto.div_const {α : Type u_1} {f : Filter α} {m : α → ENNReal} {a : ENNReal} {b : ENNReal} (hm : Filter.Tendsto m f (nhds a)) (ha : a ≠ 0 ∨ b ≠ 0) : Filter.Tendsto (fun (x : α) => m x / b) f (nhds (a / b))

theorem ENNReal.tendsto_inv_nat_nhds_zero : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹) Filter.atTop (nhds 0)

theorem ENNReal.iSup_add {a : ENNReal} {ι : Sort u_4} {s : ι → ENNReal} [Nonempty ι] : iSup s + a = ⨆ (b : ι), s b + a

theorem ENNReal.biSup_add' {a : ENNReal} {ι : Sort u_4} {p : ι → Prop} (h : ∃ (i : ι), p i) {f : ι → ENNReal} : (⨆ (i : ι), ⨆ (_ : p i), f i) + a = ⨆ (i : ι), ⨆ (_ : p i), f i + a

theorem ENNReal.add_biSup' {a : ENNReal} {ι : Sort u_4} {p : ι → Prop} (h : ∃ (i : ι), p i) {f : ι → ENNReal} : a + ⨆ (i : ι), ⨆ (_ : p i), f i = ⨆ (i : ι), ⨆ (_ : p i), a + f i

theorem ENNReal.biSup_add {a : ENNReal} {ι : Type u_4} {s : Set ι} (hs : s.Nonempty) {f : ι → ENNReal} : (⨆ i ∈ s, f i) + a = ⨆ i ∈ s, f i + a

theorem ENNReal.add_biSup {a : ENNReal} {ι : Type u_4} {s : Set ι} (hs : s.Nonempty) {f : ι → ENNReal} : a + ⨆ i ∈ s, f i = ⨆ i ∈ s, a + f i

theorem ENNReal.sSup_add {a : ENNReal} {s : Set ENNReal} (hs : s.Nonempty) : sSup s + a = ⨆ b ∈ s, b + a

theorem ENNReal.add_iSup {a : ENNReal} {ι : Sort u_4} {s : ι → ENNReal} [Nonempty ι] : a + iSup s = ⨆ (b : ι), a + s b

theorem ENNReal.iSup_add_iSup_le {ι : Sort u_4} {ι' : Sort u_5} [Nonempty ι] [Nonempty ι'] {f : ι → ENNReal} {g : ι' → ENNReal} {a : ENNReal} (h : ∀ (i : ι) (j : ι'), f i + g j ≤ a) : iSup f + iSup g ≤ a

theorem ENNReal.biSup_add_biSup_le' {ι : Sort u_4} {ι' : Sort u_5} {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 : ι), ⨆ (_ : p i), f i) + ⨆ (j : ι'), ⨆ (_ : q j), g j ≤ a

theorem ENNReal.biSup_add_biSup_le {ι : Type u_4} {ι' : Type u_5} {s : Set ι} {t : Set ι'} (hs : s.Nonempty) (ht : t.Nonempty) {f : ι → ENNReal} {g : ι' → ENNReal} {a : ENNReal} (h : ∀ i ∈ s, ∀ j ∈ t, f i + g j ≤ a) : (⨆ i ∈ s, f i) + ⨆ j ∈ t, g j ≤ a

theorem ENNReal.iSup_add_iSup {ι : Sort u_4} {f : ι → ENNReal} {g : ι → ENNReal} (h : ∀ (i j : ι), ∃ (k : ι), f i + g j ≤ f k + g k) : iSup f + iSup g = ⨆ (a : ι), f a + g a

theorem ENNReal.iSup_add_iSup_of_monotone {ι : Type u_4} [SemilatticeSup ι] {f : ι → ENNReal} {g : ι → ENNReal} (hf : Monotone f) (hg : Monotone g) : iSup f + iSup g = ⨆ (a : ι), f a + g a

theorem ENNReal.finset_sum_iSup_nat {α : Type u_4} {ι : Type u_5} [SemilatticeSup ι] {s : Finset α} {f : α → ι → ENNReal} (hf : ∀ (a : α), Monotone (f a)) : (s.sum fun (a : α) => iSup (f a)) = ⨆ (n : ι), s.sum fun (a : α) => f a n

theorem ENNReal.mul_iSup {ι : Sort u_4} {f : ι → ENNReal} {a : ENNReal} : a * iSup f = ⨆ (i : ι), a * f i

theorem ENNReal.mul_sSup {s : Set ENNReal} {a : ENNReal} : a * sSup s = ⨆ i ∈ s, a * i

theorem ENNReal.iSup_mul {ι : Sort u_4} {f : ι → ENNReal} {a : ENNReal} : iSup f * a = ⨆ (i : ι), f i * a

theorem ENNReal.smul_iSup {ι : Sort u_4} {R : Type u_5} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] (f : ι → ENNReal) (c : R) : c • ⨆ (i : ι), f i = ⨆ (i : ι), c • f i

theorem ENNReal.smul_sSup {R : Type u_4} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] (s : Set ENNReal) (c : R) : c • sSup s = ⨆ i ∈ s, c • i

theorem ENNReal.iSup_div {ι : Sort u_4} {f : ι → ENNReal} {a : ENNReal} : iSup f / a = ⨆ (i : ι), f i / a

theorem ENNReal.tendsto_coe_sub {r : NNReal} {b : ENNReal} : Filter.Tendsto (fun (b : ENNReal) => ↑r - b) (nhds b) (nhds (↑r - b))

theorem ENNReal.sub_iSup {a : ENNReal} {ι : Sort u_4} [Nonempty ι] {b : ι → ENNReal} (hr : a < ⊤) : a - ⨆ (i : ι), b i = ⨅ (i : ι), a - b i

theorem ENNReal.exists_countable_dense_no_zero_top : ∃ (s : Set ENNReal), s.Countable ∧ Dense s ∧ 0 ∉ s ∧ ⊤ ∉ s

theorem ENNReal.exists_lt_add_of_lt_add {x : ENNReal} {y : ENNReal} {z : ENNReal} (h : x < y + z) (hy : y ≠ 0) (hz : z ≠ 0) : ∃ (y' : ENNReal) (z' : ENNReal), y' < y ∧ z' < z ∧ x < y' + z'

theorem ENNReal.ofReal_cinfi {α : Type u_1} (f : α → ℝ) [Nonempty α] : ENNReal.ofReal (⨅ (i : α), f i) = ⨅ (i : α), ENNReal.ofReal (f i)

theorem ENNReal.exists_frequently_lt_of_liminf_ne_top {ι : Type u_4} {l : Filter ι} {x : ι → ℝ} (hx : Filter.liminf (fun (n : ι) => ↑(Real.nnabs (x n))) l ≠ ⊤) : ∃ (R : ℝ), ∃ᶠ (n : ι) in l, x n < R

theorem ENNReal.exists_frequently_lt_of_liminf_ne_top' {ι : Type u_4} {l : Filter ι} {x : ι → ℝ} (hx : Filter.liminf (fun (n : ι) => ↑(Real.nnabs (x n))) l ≠ ⊤) : ∃ (R : ℝ), ∃ᶠ (n : ι) in l, R < x n

theorem ENNReal.exists_upcrossings_of_not_bounded_under {ι : Type u_4} {l : Filter ι} {x : ι → ℝ} (hf : Filter.liminf (fun (i : ι) => ↑(Real.nnabs (x i))) l ≠ ⊤) (hbdd : ¬Filter.IsBoundedUnder (fun (x x_1 : ℝ) => x ≤ x_1) l fun (i : ι) => |x i|) : ∃ (a : ℚ) (b : ℚ), a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i

theorem ENNReal.hasSum_coe {α : Type u_1} {f : α → NNReal} {r : NNReal} : HasSum (fun (a : α) => ↑(f a)) ↑r ↔ HasSum f r

theorem ENNReal.tsum_coe_eq {α : Type u_1} {r : NNReal} {f : α → NNReal} (h : HasSum f r) : ∑' (a : α), ↑(f a) = ↑r

theorem ENNReal.coe_tsum {α : Type u_1} {f : α → NNReal} : Summable f → ↑(tsum f) = ∑' (a : α), ↑(f a)

theorem ENNReal.hasSum {α : Type u_1} {f : α → ENNReal} : HasSum f (⨆ (s : Finset α), s.sum fun (a : α) => f a)

@[simp]

theorem ENNReal.summable {α : Type u_1} {f : α → ENNReal} : Summable f

theorem ENNReal.tsum_coe_ne_top_iff_summable {β : Type u_2} {f : β → NNReal} : ∑' (b : β), ↑(f b) ≠ ⊤ ↔ Summable f

theorem ENNReal.tsum_eq_iSup_sum {α : Type u_1} {f : α → ENNReal} : ∑' (a : α), f a = ⨆ (s : Finset α), s.sum fun (a : α) => f a

theorem ENNReal.tsum_eq_iSup_sum' {α : Type u_1} {f : α → ENNReal} {ι : Type u_4} (s : ι → Finset α) (hs : ∀ (t : Finset α), ∃ (i : ι), t ⊆ s i) : ∑' (a : α), f a = ⨆ (i : ι), (s i).sum fun (a : α) => f a

theorem ENNReal.tsum_sigma {α : Type u_1} {β : α → Type u_4} (f : (a : α) → β a → ENNReal) : ∑' (p : (a : α) × β a), f p.fst p.snd = ∑' (a : α) (b : β a), f a b

theorem ENNReal.tsum_sigma' {α : Type u_1} {β : α → Type u_4} (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.1 p.2 = ∑' (a : α) (b : β), f a b

theorem ENNReal.tsum_prod' {α : Type u_1} {β : Type u_2} {f : α × β → ENNReal} : ∑' (p : α × β), f p = ∑' (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 : α → ENNReal} {g : α → ENNReal} : ∑' (a : α), (f a + g a) = ∑' (a : α), f a + ∑' (a : α), g a

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

theorem GCongr.ennreal_tsum_le_tsum {α : Type u_1} {f : α → ENNReal} {g : α → ENNReal} (h : ∀ (a : α), f a ≤ g a) : tsum f ≤ tsum g

theorem ENNReal.sum_le_tsum {α : Type u_1} {f : α → ENNReal} (s : Finset α) : (s.sum fun (x : α) => f x) ≤ ∑' (x : α), f x

theorem ENNReal.tsum_eq_iSup_nat' {f : ℕ → ENNReal} {N : ℕ → ℕ} (hN : Filter.Tendsto N Filter.atTop Filter.atTop) : ∑' (i : ℕ), f i = ⨆ (i : ℕ), (Finset.range (N i)).sum fun (a : ℕ) => f a

theorem ENNReal.tsum_eq_iSup_nat {f : ℕ → ENNReal} : ∑' (i : ℕ), f i = ⨆ (i : ℕ), (Finset.range i).sum fun (a : ℕ) => f a

theorem ENNReal.tsum_eq_liminf_sum_nat {f : ℕ → ENNReal} : ∑' (i : ℕ), f i = Filter.liminf (fun (n : ℕ) => (Finset.range n).sum fun (i : ℕ) => f i) Filter.atTop

theorem ENNReal.tsum_eq_limsup_sum_nat {f : ℕ → ENNReal} : ∑' (i : ℕ), f i = Filter.limsup (fun (n : ℕ) => (Finset.range n).sum fun (i : ℕ) => f i) Filter.atTop

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

@[simp]

theorem ENNReal.tsum_eq_zero {α : Type u_1} {f : α → ENNReal} : ∑' (i : α), f i = 0 ↔ ∀ (i : α), f i = 0

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

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

@[simp]

theorem ENNReal.tsum_top {α : Type u_1} [Nonempty α] : ∑' (x : α), ⊤ = ⊤

theorem ENNReal.tsum_const_eq_top_of_ne_zero {α : Type u_4} [Infinite α] {c : ENNReal} (hc : c ≠ 0) : ∑' (x : α), c = ⊤

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

theorem ENNReal.tsum_const_smul {α : Type u_1} {f : α → ENNReal} {R : Type u_4} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] (a : R) : ∑' (i : α), a • f i = a • ∑' (i : α), f i

@[simp]

theorem ENNReal.tsum_iSup_eq {α : Type u_4} (a : α) {f : α → ENNReal} : ∑' (b : α), ⨆ (_ : a = b), f b = f a

theorem ENNReal.hasSum_iff_tendsto_nat {f : ℕ → ENNReal} (r : ENNReal) : HasSum f r ↔ Filter.Tendsto (fun (n : ℕ) => (Finset.range n).sum fun (i : ℕ) => f i) Filter.atTop (nhds r)

theorem ENNReal.tendsto_nat_tsum (f : ℕ → ENNReal) : Filter.Tendsto (fun (n : ℕ) => (Finset.range n).sum fun (i : ℕ) => f i) Filter.atTop (nhds (∑' (n : ℕ), f n))

theorem ENNReal.toNNReal_apply_of_tsum_ne_top {α : Type u_4} {f : α → ENNReal} (hf : ∑' (i : α), f i ≠ ⊤) (x : α) : ↑((ENNReal.toNNReal ∘ f) x) = f x

theorem ENNReal.summable_toNNReal_of_tsum_ne_top {α : Type u_4} {f : α → ENNReal} (hf : ∑' (i : α), f i ≠ ⊤) : Summable (ENNReal.toNNReal ∘ f)

theorem ENNReal.tendsto_cofinite_zero_of_tsum_ne_top {α : Type u_4} {f : α → ENNReal} (hf : ∑' (x : α), f x ≠ ⊤) : Filter.Tendsto f Filter.cofinite (nhds 0)

theorem ENNReal.tendsto_atTop_zero_of_tsum_ne_top {f : ℕ → ENNReal} (hf : ∑' (x : ℕ), f x ≠ ⊤) : Filter.Tendsto f Filter.atTop (nhds 0)

theorem ENNReal.tendsto_tsum_compl_atTop_zero {α : Type u_4} {f : α → ENNReal} (hf : ∑' (x : α), f x ≠ ⊤) : 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.

theorem ENNReal.tsum_apply {ι : Type u_4} {α : Type u_5} {f : ι → α → ENNReal} {x : α} : tsum (fun (i : ι) => f i) x = ∑' (i : ι), f i x

theorem ENNReal.tsum_sub {f : ℕ → ENNReal} {g : ℕ → ENNReal} (h₁ : ∑' (i : ℕ), g i ≠ ⊤) (h₂ : g ≤ f) : ∑' (i : ℕ), (f i - g i) = ∑' (i : ℕ), f i - ∑' (i : ℕ), g i

theorem ENNReal.tsum_comp_le_tsum_of_injective {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Injective f) (g : β → ENNReal) : ∑' (x : α), g (f x) ≤ ∑' (y : β), g y

theorem ENNReal.tsum_le_tsum_comp_of_surjective {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Surjective f) (g : β → ENNReal) : ∑' (y : β), g y ≤ ∑' (x : α), g (f x)

theorem ENNReal.tsum_mono_subtype {α : Type u_1} (f : α → ENNReal) {s : Set α} {t : Set α} (h : s ⊆ t) : ∑' (x : ↑s), f ↑x ≤ ∑' (x : ↑t), f ↑x

theorem ENNReal.tsum_iUnion_le_tsum {α : Type u_1} {ι : Type u_4} (f : α → ENNReal) (t : ι → Set α) : ∑' (x : ↑(⋃ (i : ι), t i)), f ↑x ≤ ∑' (i : ι) (x : ↑(t i)), f ↑x

theorem ENNReal.tsum_biUnion_le_tsum {α : Type u_1} {ι : Type u_4} (f : α → ENNReal) (s : Set ι) (t : ι → Set α) : ∑' (x : ↑(⋃ i ∈ s, t i)), f ↑x ≤ ∑' (i : ↑s) (x : ↑(t ↑i)), f ↑x

theorem ENNReal.tsum_biUnion_le {α : Type u_1} {ι : Type u_4} (f : α → ENNReal) (s : Finset ι) (t : ι → Set α) : ∑' (x : ↑(⋃ i ∈ s, t i)), f ↑x ≤ s.sum fun (i : ι) => ∑' (x : ↑(t i)), f ↑x

theorem ENNReal.tsum_iUnion_le {α : Type u_1} {ι : Type u_4} [Fintype ι] (f : α → ENNReal) (t : ι → Set α) : ∑' (x : ↑(⋃ (i : ι), t i)), f ↑x ≤ Finset.univ.sum fun (i : ι) => ∑' (x : ↑(t i)), f ↑x

theorem ENNReal.tsum_union_le {α : Type u_1} (f : α → ENNReal) (s : Set α) (t : Set α) : ∑' (x : ↑(s ∪ t)), f ↑x ≤ ∑' (x : ↑s), f ↑x + ∑' (x : ↑t), f ↑x

theorem ENNReal.tsum_eq_add_tsum_ite {β : Type u_2} {f : β → ENNReal} (b : β) : ∑' (x : β), f x = f b + ∑' (x : β), if x = b then 0 else 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_4} {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_4} {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.toFinset.card ≤ c / ε

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

theorem ENNReal.tendsto_toReal_iff {ι : Type u_4} {fi : Filter ι} {f : ι → ENNReal} (hf : ∀ (i : ι), f i ≠ ⊤) {x : ENNReal} (hx : x ≠ ⊤) : Filter.Tendsto (fun (n : ι) => (f n).toReal) fi (nhds x.toReal) ↔ Filter.Tendsto f fi (nhds x)

theorem ENNReal.tsum_coe_ne_top_iff_summable_coe {α : Type u_1} {f : α → NNReal} : ∑' (a : α), ↑(f a) ≠ ⊤ ↔ Summable fun (a : α) => ↑(f a)

theorem ENNReal.tsum_coe_eq_top_iff_not_summable_coe {α : Type u_1} {f : α → NNReal} : ∑' (a : α), ↑(f a) = ⊤ ↔ ¬Summable fun (a : α) => ↑(f a)

theorem ENNReal.hasSum_toReal {α : Type u_1} {f : α → ENNReal} (hsum : ∑' (x : α), f x ≠ ⊤) : HasSum (fun (x : α) => (f x).toReal) (∑' (x : α), (f x).toReal)

theorem ENNReal.summable_toReal {α : Type u_1} {f : α → ENNReal} (hsum : ∑' (x : α), f x ≠ ⊤) : Summable fun (x : α) => (f x).toReal

theorem NNReal.tsum_eq_toNNReal_tsum {β : Type u_2} {f : β → NNReal} : ∑' (b : β), f b = (∑' (b : β), ↑(f b)).toNNReal

theorem NNReal.exists_le_hasSum_of_le {β : Type u_2} {f : β → NNReal} {g : β → NNReal} {r : NNReal} (hgf : ∀ (b : β), g b ≤ f b) (hfr : HasSum f r) : ∃ p ≤ r, HasSum g p

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

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

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

theorem Summable.countable_support_nnreal {α : Type u_1} (f : α → NNReal) (h : Summable f) : (Function.support f).Countable

Summable non-negative functions have countable support

theorem NNReal.hasSum_iff_tendsto_nat {f : ℕ → NNReal} {r : NNReal} : HasSum f r ↔ Filter.Tendsto (fun (n : ℕ) => (Finset.range n).sum fun (i : ℕ) => f i) Filter.atTop (nhds r)

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

theorem NNReal.not_summable_iff_tendsto_nat_atTop {f : ℕ → NNReal} : ¬Summable f ↔ Filter.Tendsto (fun (n : ℕ) => (Finset.range n).sum fun (i : ℕ) => f i) Filter.atTop Filter.atTop

theorem NNReal.summable_iff_not_tendsto_nat_atTop {f : ℕ → NNReal} : Summable f ↔ ¬Filter.Tendsto (fun (n : ℕ) => (Finset.range n).sum fun (i : ℕ) => f i) Filter.atTop Filter.atTop

theorem NNReal.summable_of_sum_range_le {f : ℕ → NNReal} {c : NNReal} (h : ∀ (n : ℕ), ((Finset.range n).sum fun (i : ℕ) => f i) ≤ c) : Summable f

theorem NNReal.tsum_le_of_sum_range_le {f : ℕ → NNReal} {c : NNReal} (h : ∀ (n : ℕ), ((Finset.range n).sum fun (i : ℕ) => f i) ≤ c) : ∑' (n : ℕ), f n ≤ c

theorem NNReal.tsum_comp_le_tsum_of_inj {α : Type u_1} {β : Type u_4} {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_4} {f : (x : α) × β x → NNReal} : Summable f ↔ (∀ (x : α), Summable fun (y : β x) => f ⟨x, y⟩) ∧ Summable fun (x : α) => ∑' (y : β x), f ⟨x, y⟩

theorem NNReal.indicator_summable {α : Type u_1} {f : α → NNReal} (hf : Summable f) (s : Set α) : Summable (s.indicator f)

theorem NNReal.tsum_indicator_ne_zero {α : Type u_1} {f : α → NNReal} (hf : Summable f) {s : Set α} (h : ∃ a ∈ s, f a ≠ 0) : ∑' (x : α), s.indicator f x ≠ 0

theorem NNReal.tendsto_sum_nat_add (f : ℕ → NNReal) : Filter.Tendsto (fun (i : ℕ) => ∑' (k : ℕ), f (k + i)) Filter.atTop (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.hasSum_lt {α : Type u_1} {f : α → NNReal} {g : α → NNReal} {sf : NNReal} {sg : NNReal} {i : α} (h : ∀ (a : α), f a ≤ g a) (hi : f i < g i) (hf : HasSum f sf) (hg : HasSum g sg) : sf < sg

theorem NNReal.hasSum_strict_mono {α : Type u_1} {f : α → NNReal} {g : α → NNReal} {sf : NNReal} {sg : NNReal} (hf : HasSum f sf) (hg : HasSum g sg) (h : f < g) : sf < sg

theorem NNReal.tsum_lt_tsum {α : Type u_1} {f : α → NNReal} {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 : α → NNReal} {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 NNReal.tsum_eq_add_tsum_ite {α : Type u_1} {f : α → NNReal} (hf : Summable f) (i : α) : ∑' (x : α), f x = f i + ∑' (x : α), if x = i then 0 else f x

theorem ENNReal.tsum_toNNReal_eq {α : Type u_1} {f : α → ENNReal} (hf : ∀ (a : α), f a ≠ ⊤) : (∑' (a : α), f a).toNNReal = ∑' (a : α), (f a).toNNReal

theorem ENNReal.tsum_toReal_eq {α : Type u_1} {f : α → ENNReal} (hf : ∀ (a : α), f a ≠ ⊤) : (∑' (a : α), f a).toReal = ∑' (a : α), (f a).toReal

theorem ENNReal.tendsto_sum_nat_add (f : ℕ → ENNReal) (hf : ∑' (i : ℕ), f i ≠ ⊤) : Filter.Tendsto (fun (i : ℕ) => ∑' (k : ℕ), f (k + i)) Filter.atTop (nhds 0)

theorem ENNReal.tsum_le_of_sum_range_le {f : ℕ → ENNReal} {c : ENNReal} (h : ∀ (n : ℕ), ((Finset.range n).sum fun (i : ℕ) => f i) ≤ c) : ∑' (n : ℕ), f n ≤ c

theorem ENNReal.hasSum_lt {α : Type u_1} {f : α → ENNReal} {g : α → ENNReal} {sf : ENNReal} {sg : ENNReal} {i : α} (h : ∀ (a : α), f a ≤ g a) (hi : f i < g i) (hsf : sf ≠ ⊤) (hf : HasSum f sf) (hg : HasSum g sg) : sf < sg

theorem ENNReal.tsum_lt_tsum {α : Type u_1} {f : α → ENNReal} {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_4} {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) : Summable g

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

theorem Summable.toNNReal {α : Type u_1} {f : α → ℝ} (hf : Summable f) : Summable fun (n : α) => (f n).toNNReal

theorem Summable.countable_support_ennreal {α : Type u_1} {f : α → ENNReal} (h : ∑' (i : α), f i ≠ ⊤) : (Function.support f).Countable

Finitely summable non-negative functions have countable support

theorem hasSum_iff_tendsto_nat_of_nonneg {f : ℕ → ℝ} (hf : ∀ (i : ℕ), 0 ≤ f i) (r : ℝ) : HasSum f r ↔ Filter.Tendsto (fun (n : ℕ) => (Finset.range n).sum fun (i : ℕ) => f i) Filter.atTop (nhds r)

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

theorem ENNReal.ofReal_tsum_of_nonneg {α : Type u_1} {f : α → ℝ} (hf_nonneg : ∀ (n : α), 0 ≤ f n) (hf : Summable f) : ENNReal.ofReal (∑' (n : α), f n) = ∑' (n : α), ENNReal.ofReal (f n)

theorem edist_ne_top_of_mem_ball {β : Type u_2} [EMetricSpace β] {a : β} {r : ENNReal} (x : ↑(EMetric.ball a r)) (y : ↑(EMetric.ball a r)) : edist ↑x ↑y ≠ ⊤

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

def metricSpaceEMetricBall {β : Type u_2} [EMetricSpace β] (a : β) (r : ENNReal) : MetricSpace ↑(EMetric.ball a r)

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

Equations

• metricSpaceEMetricBall a r = EMetricSpace.toMetricSpace ⋯

theorem nhds_eq_nhds_emetric_ball {β : Type u_2} [EMetricSpace β] (a : β) (x : β) (r : ENNReal) (h : x ∈ EMetric.ball a r) : nhds x = Filter.map Subtype.val (nhds ⟨x, h⟩)

theorem tendsto_iff_edist_tendsto_0 {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] {l : Filter β} {f : β → α} {y : α} : Filter.Tendsto f l (nhds y) ↔ Filter.Tendsto (fun (x : β) => edist (f x) y) l (nhds 0)

theorem EMetric.cauchySeq_iff_le_tendsto_0 {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [Nonempty β] [SemilatticeSup β] {s : β → α} : CauchySeq s ↔ ∃ (b : β → ENNReal), (∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N) ∧ Filter.Tendsto b Filter.atTop (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} [PseudoEMetricSpace α] {f : α → ENNReal} (C : ENNReal) (hC : C ≠ ⊤) (h : ∀ (x y : α), f x ≤ f y + C * edist x y) : Continuous f

theorem continuous_edist {α : Type u_1} [PseudoEMetricSpace α] : Continuous fun (p : α × α) => edist p.1 p.2

theorem Continuous.edist {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [TopologicalSpace β] {f : β → α} {g : β → α} (hf : Continuous f) (hg : Continuous g) : Continuous fun (b : β) => edist (f b) (g b)

theorem Filter.Tendsto.edist {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] {f : β → α} {g : β → α} {x : Filter β} {a : α} {b : α} (hf : Filter.Tendsto f x (nhds a)) (hg : Filter.Tendsto g x (nhds b)) : Filter.Tendsto (fun (x : β) => edist (f x) (g x)) x (nhds (edist a b))

theorem cauchySeq_of_edist_le_of_summable {α : Type u_1} [PseudoEMetricSpace α] {f : ℕ → α} (d : ℕ → NNReal) (hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)) (hd : Summable d) : CauchySeq f

If the extended distance between consecutive points of a sequence is estimated by a summable series of NNReals, then the original sequence is a Cauchy sequence.

theorem cauchySeq_of_edist_le_of_tsum_ne_top {α : Type u_1} [PseudoEMetricSpace α] {f : ℕ → α} (d : ℕ → ENNReal) (hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n) (hd : tsum d ≠ ⊤) : CauchySeq f

theorem EMetric.isClosed_ball {α : Type u_1} [PseudoEMetricSpace α] {a : α} {r : ENNReal} : IsClosed (EMetric.closedBall a r)

@[simp]

theorem EMetric.diam_closure {α : Type u_1} [PseudoEMetricSpace α] (s : Set α) : EMetric.diam (closure s) = EMetric.diam s

@[simp]

theorem Metric.diam_closure {α : Type u_4} [PseudoMetricSpace α] (s : Set α) : Metric.diam (closure s) = Metric.diam s

theorem isClosed_setOf_lipschitzOnWith {α : Type u_4} {β : Type u_5} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (K : NNReal) (s : Set α) : IsClosed {f : α → β | LipschitzOnWith K f s}

theorem isClosed_setOf_lipschitzWith {α : Type u_4} {β : Type u_5} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (K : NNReal) : IsClosed {f : α → β | LipschitzWith K f}

theorem Real.ediam_eq {s : Set ℝ} (h : Bornology.IsBounded s) : EMetric.diam s = ENNReal.ofReal (sSup s - sInf s)

For a bounded set s : Set ℝ, its EMetric.diam is equal to sSup s - sInf s reinterpreted as ℝ≥0∞.

theorem Real.diam_eq {s : Set ℝ} (h : Bornology.IsBounded s) : Metric.diam s = sSup s - sInf s

For a bounded set s : Set ℝ, its Metric.diam is equal to sSup s - sInf s.

@[simp]

theorem Real.ediam_Ioo (a : ℝ) (b : ℝ) : EMetric.diam (Set.Ioo a b) = ENNReal.ofReal (b - a)

@[simp]

theorem Real.ediam_Icc (a : ℝ) (b : ℝ) : EMetric.diam (Set.Icc a b) = ENNReal.ofReal (b - a)

@[simp]

theorem Real.ediam_Ico (a : ℝ) (b : ℝ) : EMetric.diam (Set.Ico a b) = ENNReal.ofReal (b - a)

@[simp]

theorem Real.ediam_Ioc (a : ℝ) (b : ℝ) : EMetric.diam (Set.Ioc a b) = ENNReal.ofReal (b - a)

theorem Real.diam_Icc {a : ℝ} {b : ℝ} (h : a ≤ b) : Metric.diam (Set.Icc a b) = b - a

theorem Real.diam_Ico {a : ℝ} {b : ℝ} (h : a ≤ b) : Metric.diam (Set.Ico a b) = b - a

theorem Real.diam_Ioc {a : ℝ} {b : ℝ} (h : a ≤ b) : Metric.diam (Set.Ioc a b) = b - a

theorem Real.diam_Ioo {a : ℝ} {b : ℝ} (h : a ≤ b) : Metric.diam (Set.Ioo a b) = b - a

theorem edist_le_tsum_of_edist_le_of_tendsto {α : Type u_1} [PseudoEMetricSpace α] {f : ℕ → α} (d : ℕ → ENNReal) (hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n) {a : α} (ha : Filter.Tendsto f Filter.atTop (nhds a)) (n : ℕ) : 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} [PseudoEMetricSpace α] {f : ℕ → α} (d : ℕ → ENNReal) (hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n) {a : α} (ha : Filter.Tendsto f Filter.atTop (nhds a)) : 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.

noncomputable def ENNReal.truncateToReal (t : ENNReal) (x : ENNReal) : ℝ

With truncation level t, the truncated cast ℝ≥0∞ → ℝ is given by x ↦ (min t x).toReal. Unlike ENNReal.toReal, this cast is continuous and monotone when t ≠ ∞.

Equations

• t.truncateToReal x = (min t x).toReal

theorem ENNReal.truncateToReal_eq_toReal {t : ENNReal} {x : ENNReal} (t_ne_top : t ≠ ⊤) (x_le : x ≤ t) : t.truncateToReal x = x.toReal

theorem ENNReal.truncateToReal_le {t : ENNReal} (t_ne_top : t ≠ ⊤) {x : ENNReal} : t.truncateToReal x ≤ t.toReal

theorem ENNReal.truncateToReal_nonneg {t : ENNReal} {x : ENNReal} : 0 ≤ t.truncateToReal x

theorem ENNReal.monotone_truncateToReal {t : ENNReal} (t_ne_top : t ≠ ⊤) : Monotone t.truncateToReal

The truncated cast ENNReal.truncateToReal t : ℝ≥0∞ → ℝ is monotone when t ≠ ∞.

theorem ENNReal.continuous_truncateToReal {t : ENNReal} (t_ne_top : t ≠ ⊤) : Continuous t.truncateToReal

The truncated cast ENNReal.truncateToReal t : ℝ≥0∞ → ℝ is continuous when t ≠ ∞.

theorem ENNReal.limsup_sub_const {ι : Type u_4} (F : Filter ι) [F.NeBot] (f : ι → ENNReal) (c : ENNReal) : Filter.limsup (fun (i : ι) => f i - c) F = Filter.limsup f F - c

theorem ENNReal.liminf_sub_const {ι : Type u_4} (F : Filter ι) [F.NeBot] (f : ι → ENNReal) (c : ENNReal) : Filter.liminf (fun (i : ι) => f i - c) F = Filter.liminf f F - c

theorem ENNReal.limsup_const_sub {ι : Type u_4} (F : Filter ι) [F.NeBot] (f : ι → ENNReal) {c : ENNReal} (c_ne_top : c ≠ ⊤) : Filter.limsup (fun (i : ι) => c - f i) F = c - Filter.liminf f F

theorem ENNReal.liminf_const_sub {ι : Type u_4} (F : Filter ι) [F.NeBot] (f : ι → ENNReal) {c : ENNReal} (c_ne_top : c ≠ ⊤) : Filter.liminf (fun (i : ι) => c - f i) F = c - Filter.limsup f F

theorem ENNReal.liminf_toReal_eq {ι : Type u_5} {F : Filter ι} [F.NeBot] {b : ENNReal} (b_ne_top : b ≠ ⊤) {xs : ι → ENNReal} (le_b : ∀ᶠ (i : ι) in F, xs i ≤ b) : Filter.liminf (fun (i : ι) => (xs i).toReal) F = (Filter.liminf xs F).toReal

If xs : ι → ℝ≥0∞ is bounded, then we have liminf (toReal ∘ xs) = toReal (liminf xs).

theorem ENNReal.limsup_toReal_eq {ι : Type u_5} {F : Filter ι} [F.NeBot] {b : ENNReal} (b_ne_top : b ≠ ⊤) {xs : ι → ENNReal} (le_b : ∀ᶠ (i : ι) in F, xs i ≤ b) : Filter.limsup (fun (i : ι) => (xs i).toReal) F = (Filter.limsup xs F).toReal

If xs : ι → ℝ≥0∞ is bounded, then we have liminf (toReal ∘ xs) = toReal (liminf xs).