Extended non-negative reals
@[instance]
Topology on ennreal.
Note: this is different from the emetric_space topology. The emetric_space topology has
is_open {⊤}, while this topology doesn't have singleton elements.
Equations
theorem
ennreal.tendsto_coe
{α : Type u_1}
{f : filter α}
{m : α → ℝ≥0}
{a : ℝ≥0} :
filter.tendsto (λ (a : α), ↑(m a)) f (𝓝 ↑a) ↔ filter.tendsto m f (𝓝 a)
theorem
ennreal.continuous_coe_iff
{α : Type u_1}
[topological_space α]
{f : α → ℝ≥0} :
continuous (λ (a : α), ↑(f a)) ↔ continuous f
theorem
ennreal.tendsto_of_real
{α : Type u_1}
{f : filter α}
{m : α → ℝ}
{a : ℝ}
(h : filter.tendsto m f (𝓝 a)) :
filter.tendsto (λ (a : α), ennreal.of_real (m a)) f (𝓝 (ennreal.of_real 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 (𝓝 ⊤)
The set of finite ennreal numbers is homeomorphic to nnreal.
Equations
- ennreal.ne_top_homeomorph_nnreal = {to_equiv := {to_fun := λ (x : ↥{a : ennreal | a ≠ ⊤}), ↑x.to_nnreal, inv_fun := λ (x : ℝ≥0), ⟨↑x, _⟩, 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}
The set of finite ennreal numbers is homeomorphic to nnreal.
Equations
- ennreal.lt_top_homeomorph_nnreal = (homeomorph.set_congr ennreal.lt_top_homeomorph_nnreal._proof_1).trans ennreal.ne_top_homeomorph_nnreal
theorem
ennreal.tendsto_nhds
{α : Type u_1}
{f : filter α}
{u : α → ennreal}
{a : ennreal}
(ha : a ≠ ⊤) :
Characterization of neighborhoods for ennreal numbers. See also tendsto_order
for a version with strict inequalities.
theorem
ennreal.tendsto_at_top
{β : Type u_2}
[nonempty β]
[semilattice_sup β]
{f : β → ennreal}
{a : ennreal}
(ha : a ≠ ⊤) :
theorem
ennreal.tendsto_coe_nnreal_nhds_top
{α : Type u_1}
{l : filter α}
{f : α → ℝ≥0}
(h : filter.tendsto f l filter.at_top) :
filter.tendsto (λ (a : α), ↑(f a)) l (𝓝 ⊤)
theorem
ennreal.tendsto.const_mul
{α : Type u_1}
{f : filter α}
{m : α → ennreal}
{a b : ennreal}
(hm : filter.tendsto m f (𝓝 b))
(hb : b ≠ 0 ∨ a ≠ ⊤) :
filter.tendsto (λ (b : α), a * m b) f (𝓝 (a * b))
theorem
ennreal.tendsto.mul_const
{α : Type u_1}
{f : filter α}
{m : α → ennreal}
{a b : ennreal}
(hm : filter.tendsto m f (𝓝 a))
(ha : a ≠ 0 ∨ b ≠ ⊤) :
filter.tendsto (λ (x : α), (m x) * b) f (𝓝 (a * b))
theorem
ennreal.continuous_at_const_mul
{a b : ennreal}
(h : a ≠ ⊤ ∨ b ≠ 0) :
continuous_at (has_mul.mul a) b
theorem
ennreal.continuous_at_mul_const
{a b : ennreal}
(h : a ≠ ⊤ ∨ b ≠ 0) :
continuous_at (λ (x : ennreal), x * a) b
theorem
ennreal.continuous_mul_const
{a : ennreal}
(ha : a ≠ ⊤) :
continuous (λ (x : ennreal), x * a)
@[simp]
theorem
ennreal.tendsto_inv_iff
{α : Type u_1}
{f : filter α}
{m : α → ennreal}
{a : ennreal} :
filter.tendsto (λ (x : α), (m x)⁻¹) f (𝓝 a⁻¹) ↔ filter.tendsto m f (𝓝 a)
theorem
ennreal.tendsto.div_const
{α : Type u_1}
{f : filter α}
{m : α → ennreal}
{a b : ennreal}
(hm : filter.tendsto m f (𝓝 a))
(ha : a ≠ 0 ∨ b ≠ 0) :
filter.tendsto (λ (x : α), m x / b) f (𝓝 (a / b))
theorem
ennreal.finset_sum_supr_nat
{α : Type u_1}
{ι : Type u_2}
[semilattice_sup ι]
{s : finset α}
{f : α → ι → ennreal}
(hf : ∀ (a : α), monotone (f a)) :
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_le_tsum
{α : Type u_1}
{f 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 α) :
∑ (x : α) in s, f x ≤ ∑' (x : α), f x
theorem
ennreal.tsum_eq_supr_nat
{f : ℕ → ennreal} :
(∑' (i : ℕ), f i) = ⨆ (i : ℕ), ∑ (a : ℕ) in finset.range i, f a
@[simp]
theorem
ennreal.has_sum_iff_tendsto_nat
{f : ℕ → ennreal}
(r : ennreal) :
has_sum f r ↔ filter.tendsto (λ (n : ℕ), ∑ (i : ℕ) in finset.range n, f i) filter.at_top (𝓝 r)
theorem
ennreal.to_nnreal_apply_of_tsum_ne_top
{α : Type u_1}
{f : α → ennreal}
(hf : (∑' (i : α), f i) ≠ ⊤)
(x : α) :
↑((ennreal.to_nnreal ∘ f) x) = f x
theorem
ennreal.summable_to_nnreal_of_tsum_ne_top
{α : Type u_1}
{f : α → ennreal}
(hf : (∑' (i : α), f i) ≠ ⊤) :
theorem
ennreal.tsum_apply
{ι : Type u_1}
{α : Type u_2}
{f : ι → α → ennreal}
{x : α} :
(∑' (i : ι), f i) x = ∑' (i : ι), f i x
theorem
nnreal.has_sum_iff_tendsto_nat
{f : ℕ → ℝ≥0}
(r : ℝ≥0) :
has_sum f r ↔ filter.tendsto (λ (n : ℕ), ∑ (i : ℕ) in finset.range n, f i) filter.at_top (𝓝 r)
theorem
nnreal.tsum_comp_le_tsum_of_inj
{α : Type u_1}
{β : Type u_2}
{f : α → ℝ≥0}
(hf : summable f)
{i : β → α}
(hi : function.injective i) :
theorem
nnreal.tendsto_sum_nat_add
(f : ℕ → ℝ≥0)
(hf : summable f) :
filter.tendsto (λ (i : ℕ), ∑' (k : ℕ), f (k + i)) filter.at_top (𝓝 0)
If f : ℕ → ℝ≥0 and ∑' f exists, then ∑' k, f (k + i) tends to zero.
theorem
ennreal.tendsto_sum_nat_add
(f : ℕ → ennreal)
(hf : (∑' (i : ℕ), f i) ≠ ⊤) :
filter.tendsto (λ (i : ℕ), ∑' (k : ℕ), f (k + i)) filter.at_top (𝓝 0)
theorem
tsum_comp_le_tsum_of_inj
{α : Type u_1}
{β : Type u_2}
{f : α → ℝ}
(hf : summable f)
(hn : ∀ (a : α), 0 ≤ f a)
{i : β → α}
(hi : function.injective i) :
theorem
has_sum_iff_tendsto_nat_of_nonneg
{f : ℕ → ℝ}
(hf : ∀ (i : ℕ), 0 ≤ f i)
(r : ℝ) :
has_sum f r ↔ filter.tendsto (λ (n : ℕ), ∑ (i : ℕ) in finset.range n, f i) filter.at_top (𝓝 r)
theorem
edist_ne_top_of_mem_ball
{β : Type u_2}
[emetric_space β]
{a : β}
{r : ennreal}
(x y : ↥(emetric.ball a r)) :
In an emetric ball, the distance between points is everywhere finite
def
metric_space_emetric_ball
{β : Type u_2}
[emetric_space β]
(a : β)
(r : ennreal) :
metric_space ↥(emetric.ball a r)
Each ball in an extended metric space gives us a metric space, as the edist is everywhere finite.
theorem
nhds_eq_nhds_emetric_ball
{β : Type u_2}
[emetric_space β]
(a x : β)
(r : ennreal)
(h : x ∈ emetric.ball a r) :
theorem
tendsto_iff_edist_tendsto_0
{α : Type u_1}
{β : Type u_2}
[emetric_space α]
{l : filter β}
{f : β → α}
{y : α} :
filter.tendsto f l (𝓝 y) ↔ filter.tendsto (λ (x : β), edist (f x) y) l (𝓝 0)
theorem
emetric.cauchy_seq_iff_le_tendsto_0
{α : Type u_1}
{β : Type u_2}
[emetric_space α]
[nonempty β]
[semilattice_sup β]
{s : β → α} :
cauchy_seq s ↔ ∃ (b : β → ennreal), (∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N) ∧ filter.tendsto b filter.at_top (𝓝 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}
[emetric_space α]
{f : α → ennreal}
(C : ennreal)
(hC : C ≠ ⊤)
(h : ∀ (x y : α), f x ≤ f y + C * edist x y) :
theorem
continuous_edist
{α : Type u_1}
[emetric_space α] :
continuous (λ (p : α × α), edist p.fst p.snd)
theorem
continuous.edist
{α : Type u_1}
{β : Type u_2}
[emetric_space α]
[topological_space β]
{f g : β → α}
(hf : continuous f)
(hg : continuous g) :
continuous (λ (b : β), edist (f b) (g b))
theorem
filter.tendsto.edist
{α : Type u_1}
{β : Type u_2}
[emetric_space α]
{f g : β → α}
{x : filter β}
{a b : α}
(hf : filter.tendsto f x (𝓝 a))
(hg : filter.tendsto g x (𝓝 b)) :
filter.tendsto (λ (x : β), edist (f x) (g x)) x (𝓝 (edist a b))
theorem
emetric.is_closed_ball
{α : Type u_1}
[emetric_space α]
{a : α}
{r : ennreal} :
is_closed (emetric.closed_ball a r)
theorem
edist_le_tsum_of_edist_le_of_tendsto
{α : Type u_1}
[emetric_space α]
{f : ℕ → α}
(d : ℕ → ennreal)
(hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n)
{a : α}
(ha : filter.tendsto f filter.at_top (𝓝 a))
(n : ℕ) :
If edist (f n) (f (n+1)) is bounded above by a function d : ℕ → ennreal,
then the distance from f n to the limit is bounded by ∑'_{k=n}^∞ d k.
theorem
edist_le_tsum_of_edist_le_of_tendsto₀
{α : Type u_1}
[emetric_space α]
{f : ℕ → α}
(d : ℕ → ennreal)
(hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n)
{a : α}
(ha : filter.tendsto f filter.at_top (𝓝 a)) :
If edist (f n) (f (n+1)) is bounded above by a function d : ℕ → ennreal,
then the distance from f 0 to the limit is bounded by ∑'_{k=0}^∞ d k.