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
@[instance]
Equations
theorem
ennreal.tendsto_coe
{α : Type u_1}
{f : filter α}
{m : α → nnreal}
{a : nnreal} :
filter.tendsto (λ (a : α), ↑(m a)) f (nhds ↑a) ↔ filter.tendsto m f (nhds a)
theorem
ennreal.continuous_coe
{α : Type u_1}
[topological_space α]
{f : α → nnreal} :
continuous (λ (a : α), ↑(f a)) ↔ continuous f
theorem
ennreal.tendsto_of_real
{α : Type u_1}
{f : filter α}
{m : α → ℝ}
{a : ℝ} :
filter.tendsto m f (nhds a) → filter.tendsto (λ (a : α), ennreal.of_real (m a)) f (nhds (ennreal.of_real a))
theorem
ennreal.tendsto_to_nnreal
{a : ennreal} :
a ≠ ⊤ → filter.tendsto ennreal.to_nnreal (nhds a) (nhds a.to_nnreal)
theorem
ennreal.tendsto_to_real
{a : ennreal} :
a ≠ ⊤ → filter.tendsto ennreal.to_real (nhds a) (nhds a.to_real)
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 : nnreal), ⟨↑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
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} :
theorem
ennreal.tendsto_coe_nnreal_nhds_top
{α : Type u_1}
{l : filter α}
{f : α → nnreal} :
filter.tendsto f l filter.at_top → filter.tendsto (λ (a : α), ↑(f a)) l (nhds ⊤)
@[instance]
Equations
- ennreal.has_continuous_add = _
- _ = _
- _ = _
theorem
ennreal.tendsto.const_mul
{α : Type u_1}
{f : filter α}
{m : α → ennreal}
{a b : ennreal} :
filter.tendsto m f (nhds b) → b ≠ 0 ∨ a ≠ ⊤ → filter.tendsto (λ (b : α), a * m b) f (nhds (a * b))
theorem
ennreal.tendsto.mul_const
{α : Type u_1}
{f : filter α}
{m : α → ennreal}
{a b : ennreal} :
filter.tendsto m f (nhds a) → a ≠ 0 ∨ b ≠ ⊤ → filter.tendsto (λ (x : α), m x * b) f (nhds (a * b))
theorem
ennreal.continuous_at_const_mul
{a b : ennreal} :
a ≠ ⊤ ∨ b ≠ 0 → continuous_at (has_mul.mul a) b
@[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)
theorem
ennreal.tendsto.div_const
{α : Type u_1}
{f : filter α}
{m : α → ennreal}
{a b : ennreal} :
filter.tendsto m f (nhds a) → a ≠ 0 ∨ b ≠ 0 → filter.tendsto (λ (x : α), m x / b) f (nhds (a / b))
theorem
ennreal.tendsto_inv_nat_nhds_zero
:
filter.tendsto (λ (n : ℕ), (↑n)⁻¹) filter.at_top (nhds 0)
theorem
ennreal.finset_sum_supr_nat
{α : Type u_1}
{ι : Type u_2}
[semilattice_sup ι]
{s : finset α}
{f : α → ι → ennreal} :
theorem
ennreal.tsum_comm
{α : Type u_1}
{β : Type u_2}
{f : α → β → ennreal} :
(∑' (a : α) (b : β), f a b) = ∑' (b : β) (a : α), f a b
@[simp]
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)
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)
theorem
nnreal.tsum_comp_le_tsum_of_inj
{α : Type u_1}
{β : Type u_2}
{f : α → nnreal}
(hf : summable f)
{i : β → α} :
function.injective i → tsum (f ∘ i) ≤ tsum f
theorem
tsum_comp_le_tsum_of_inj
{α : Type u_1}
{β : Type u_2}
{f : α → ℝ}
(hf : summable f)
(hn : ∀ (a : α), 0 ≤ f a)
{i : β → α} :
function.injective i → tsum (f ∘ i) ≤ tsum f
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)
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
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 (nhds y) ↔ filter.tendsto (λ (x : β), has_edist.edist (f x) y) l (nhds 0)
theorem
emetric.cauchy_seq_iff_le_tendsto_0
{α : Type u_1}
{β : Type u_2}
[emetric_space α]
[nonempty β]
[semilattice_sup β]
{s : β → α} :
cauchy_seq s ↔ ∃ (b : β → ennreal), (∀ (n m N : β), N ≤ n → N ≤ m → has_edist.edist (s n) (s m) ≤ b N) ∧ filter.tendsto b filter.at_top (nhds 0)
Yet another metric characterization of Cauchy sequences on integers. This one is often the most efficient.
theorem
continuous_of_le_add_edist
{α : Type u_1}
[emetric_space α]
{f : α → ennreal}
(C : ennreal) :
C ≠ ⊤ → (∀ (x y : α), f x ≤ f y + C * has_edist.edist x y) → continuous f
theorem
continuous_edist
{α : Type u_1}
[emetric_space α] :
continuous (λ (p : α × α), has_edist.edist p.fst p.snd)
theorem
continuous.edist
{α : Type u_1}
{β : Type u_2}
[emetric_space α]
[topological_space β]
{f g : β → α} :
continuous f → continuous g → continuous (λ (b : β), has_edist.edist (f b) (g b))
theorem
filter.tendsto.edist
{α : Type u_1}
{β : Type u_2}
[emetric_space α]
{f g : β → α}
{x : filter β}
{a b : α} :
filter.tendsto f x (nhds a) → filter.tendsto g x (nhds b) → filter.tendsto (λ (x : β), has_edist.edist (f x) (g x)) x (nhds (has_edist.edist a b))
theorem
cauchy_seq_of_edist_le_of_tsum_ne_top
{α : Type u_1}
[emetric_space α]
{f : ℕ → α}
(d : ℕ → ennreal) :
(∀ (n : ℕ), has_edist.edist (f n) (f n.succ) ≤ d n) → tsum d ≠ ⊤ → cauchy_seq f
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 : ℕ), 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 : ℕ → 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 : ℕ), has_edist.edist (f n) (f n.succ) ≤ d n)
{a : α} :
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 : ℕ → ennreal,
then the distance from f 0 to the limit is bounded by ∑'_{k=0}^∞ d k.