Documentation

Mathlib.Topology.Instances.ENNReal

Topology on extended non-negative reals #

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
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_iff {α : Type u_4} [TopologicalSpace α] {f : αNNReal} :
(Continuous fun (a : α) => (f a)) Continuous f
theorem ENNReal.tendsto_nhds_coe_iff {α : Type u_4} {l : Filter α} {x : NNReal} {f : ENNRealα} :
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.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.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

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

Equations
Instances For
    theorem ENNReal.nhds_top :
    nhds = ⨅ (a : ENNReal), ⨅ (_ : a ), Filter.principal (Set.Ioi a)
    theorem ENNReal.nhds_top_basis :
    Filter.HasBasis (nhds ) (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) :
    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.nhds_zero :
    nhds 0 = ⨅ (a : ENNReal), ⨅ (_ : a 0), Filter.principal (Set.Iio a)
    theorem ENNReal.nhds_zero_basis :
    Filter.HasBasis (nhds 0) (fun (a : ENNReal) => 0 < a) fun (a : ENNReal) => Set.Iio a
    theorem ENNReal.nhds_zero_basis_Iic :
    Filter.HasBasis (nhds 0) (fun (a : ENNReal) => 0 < a) Set.Iic
    theorem ENNReal.hasBasis_nhds_of_ne_top' {x : ENNReal} (xt : x ) :
    Filter.HasBasis (nhds x) (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 ) :
    Filter.HasBasis (nhds x) (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 + ε)) :
    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 : β), nN, f n Set.Icc (a - ε) (a + ε)
    theorem ENNReal.tendsto_atTop_zero {β : Type u_2} [Nonempty β] [SemilatticeSup β] {f : βENNReal} :
    Filter.Tendsto f Filter.atTop (nhds 0) ε > 0, ∃ (N : β), nN, 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₁ : xs, f x 0 g x ) (h₂ : xs, 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 : is, Filter.Tendsto (f i) x (nhds (a i))) (h' : is, a i ) :
    Filter.Tendsto (fun (b : α) => Finset.prod s fun (c : ι) => f c b) x (nhds (Finset.prod s 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.continuousOn_sub_left (a : ENNReal) :
    ContinuousOn (fun (x : ENNReal) => a - x) {x : ENNReal | x }
    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 = 0Nonempty ι) :
    ⨅ (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 = 0Nonempty ι) :
    ⨅ (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
    @[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 : Set.Nonempty s) {f : ιENNReal} :
    (⨆ i ∈ s, f i) + a = ⨆ i ∈ s, f i + a
    theorem ENNReal.add_biSup {a : ENNReal} {ι : Type u_4} {s : Set ι} (hs : Set.Nonempty s) {f : ιENNReal} :
    a + ⨆ i ∈ s, f i = ⨆ i ∈ s, a + f i
    theorem ENNReal.sSup_add {a : ENNReal} {s : Set ENNReal} (hs : Set.Nonempty s) :
    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 jf 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 : Set.Nonempty s) (ht : Set.Nonempty t) {f : ιENNReal} {g : ι'ENNReal} {a : ENNReal} (h : is, jt, 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)) :
    (Finset.sum s fun (a : α) => iSup (f a)) = ⨆ (n : ι), Finset.sum s 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_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 α), Finset.sum s fun (a : α) => f a)
    @[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
    theorem ENNReal.tsum_eq_iSup_sum {α : Type u_1} {f : αENNReal} :
    ∑' (a : α), f a = ⨆ (s : Finset α), Finset.sum s 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 : ι), Finset.sum (s i) fun (a : α) => f a
    theorem ENNReal.tsum_sigma {α : Type u_1} {β : αType u_4} (f : (a : α) → β aENNReal) :
    ∑' (p : (a : α) × β a), f p.fst p.snd = ∑' (a : α) (b : β a), f a b
    theorem ENNReal.tsum_sigma' {α : Type u_1} {β : αType u_4} (f : (a : α) × β aENNReal) :
    ∑' (p : (a : α) × β a), f p = ∑' (a : α) (b : β a), f { fst := a, snd := 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 ENNReal.sum_le_tsum {α : Type u_1} {f : αENNReal} (s : Finset α) :
    (Finset.sum s 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.sum (Finset.range (N i)) fun (a : ) => f a
    theorem ENNReal.tsum_eq_iSup_nat {f : ENNReal} :
    ∑' (i : ), f i = ⨆ (i : ), Finset.sum (Finset.range i) fun (a : ) => f a
    theorem ENNReal.tsum_eq_liminf_sum_nat {f : ENNReal} :
    ∑' (i : ), f i = Filter.liminf (fun (n : ) => Finset.sum (Finset.range n) fun (i : ) => f i) Filter.atTop
    theorem ENNReal.tsum_eq_limsup_sum_nat {f : ENNReal} :
    ∑' (i : ), f i = Filter.limsup (fun (n : ) => Finset.sum (Finset.range n) 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.sum (Finset.range n) fun (i : ) => f i) Filter.atTop (nhds r)
    theorem ENNReal.tendsto_nat_tsum (f : ENNReal) :
    Filter.Tendsto (fun (n : ) => Finset.sum (Finset.range n) 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 ) :
    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 : α // xs }), 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 Finset.sum s 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.sum Finset.univ 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) :
    Set.Finite {i : ι | ε a i}

    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 : Set.Finite {i : ι | ε a i}), (Set.Finite.toFinset hf).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) :

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

    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.sum (Finset.range n) 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.sum (Finset.range n) 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.sum (Finset.range n) fun (i : ) => f i) Filter.atTop Filter.atTop
    theorem NNReal.summable_of_sum_range_le {f : NNReal} {c : NNReal} (h : ∀ (n : ), (Finset.sum (Finset.range n) fun (i : ) => f i) c) :
    theorem NNReal.tsum_le_of_sum_range_le {f : NNReal} {c : NNReal} (h : ∀ (n : ), (Finset.sum (Finset.range n) 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 : α) × β xNNReal} :
    Summable f (∀ (x : α), Summable fun (y : β x) => f { fst := x, snd := y }) Summable fun (x : α) => ∑' (y : β x), f { fst := x, snd := 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 ∈ s, f a 0) :
    ∑' (x : α), Set.indicator s 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.sum (Finset.range n) 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) :

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

    theorem Summable.toNNReal {α : Type u_1} {f : α} (hf : Summable f) :
    Summable fun (n : α) => Real.toNNReal (f n)
    theorem Summable.countable_support_ennreal {α : Type u_1} {f : αENNReal} (h : ∑' (i : α), f i ) :

    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.sum (Finset.range n) 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 not_summable_iff_tendsto_nat_atTop_of_nonneg {f : } (hf : ∀ (n : ), 0 f n) :
    ¬Summable f Filter.Tendsto (fun (n : ) => Finset.sum (Finset.range n) fun (i : ) => f i) Filter.atTop Filter.atTop
    theorem summable_iff_not_tendsto_nat_atTop_of_nonneg {f : } (hf : ∀ (n : ), 0 f n) :
    Summable f ¬Filter.Tendsto (fun (n : ) => Finset.sum (Finset.range n) fun (i : ) => f i) Filter.atTop Filter.atTop
    theorem summable_sigma_of_nonneg {α : Type u_1} {β : αType u_4} {f : (x : α) × β x} (hf : ∀ (x : (x : α) × β x), 0 f x) :
    Summable f (∀ (x : α), Summable fun (y : β x) => f { fst := x, snd := y }) Summable fun (x : α) => ∑' (y : β x), f { fst := x, snd := y }
    theorem summable_prod_of_nonneg {α : Type u_1} {β : Type u_2} {f : α × β} (hf : 0 f) :
    Summable f (∀ (x : α), Summable fun (y : β) => f (x, y)) Summable fun (x : α) => ∑' (y : β), f (x, y)
    theorem summable_of_sum_le {ι : Type u_4} {f : ι} {c : } (hf : 0 f) (h : ∀ (u : Finset ι), (Finset.sum u fun (x : ι) => f x) c) :
    theorem summable_of_sum_range_le {f : } {c : } (hf : ∀ (n : ), 0 f n) (h : ∀ (n : ), (Finset.sum (Finset.range n) fun (i : ) => f i) c) :
    theorem Real.tsum_le_of_sum_range_le {f : } {c : } (hf : ∀ (n : ), 0 f n) (h : ∀ (n : ), (Finset.sum (Finset.range n) fun (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} [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) :

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

    Equations
    Instances For
      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 { val := x, property := 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 nN medist (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) :
      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_tsum_ne_top {α : Type u_1} [PseudoEMetricSpace α] {f : α} (d : ENNReal) (hf : ∀ (n : ), edist (f n) (f (Nat.succ n)) d n) (hd : tsum d ) :
      @[simp]
      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}

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

      For a bounded set s : Set, its Metric.diam is equal to sSup s - sInf 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} [PseudoEMetricSpace α] {f : α} (d : ENNReal) (hf : ∀ (n : ), edist (f n) (f (Nat.succ n)) 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 (Nat.succ n)) 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
      Instances For
        theorem ENNReal.truncateToReal_eq_toReal {t : ENNReal} {x : ENNReal} (t_ne_top : t ) (x_le : x t) :
        theorem ENNReal.truncateToReal_le {t : ENNReal} (t_ne_top : t ) {x : ENNReal} :

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

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

        theorem ENNReal.limsup_sub_const {ι : Type u_4} (F : Filter ι) [Filter.NeBot F] (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 ι) [Filter.NeBot F] (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 ι) [Filter.NeBot F] (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 ι) [Filter.NeBot F] (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 ι} [Filter.NeBot F] {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 ι} [Filter.NeBot F] {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).