Extended non-negative reals #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[protected, instance]
Topology on ℝ≥0∞.
Note: this is different from the emetric_space topology. The emetric_space topology has
is_open {⊤}, while this topology doesn't have singleton elements.
Equations
@[protected, instance]
@[norm_cast]
theorem
ennreal.tendsto_coe
{α : Type u_1}
{f : filter α}
{m : α → nnreal}
{a : nnreal} :
filter.tendsto (λ (a : α), ↑(m a)) f (nhds ↑a) ↔ filter.tendsto m f (nhds a)
theorem
ennreal.continuous_coe_iff
{α : Type u_1}
[topological_space α]
{f : α → nnreal} :
continuous (λ (a : α), ↑(f a)) ↔ continuous f
theorem
ennreal.tendsto_nhds_coe_iff
{α : Type u_1}
{l : filter α}
{x : nnreal}
{f : ennreal → α} :
filter.tendsto f (nhds ↑x) l ↔ filter.tendsto (f ∘ coe) (nhds x) l
theorem
ennreal.continuous_at_coe_iff
{α : Type u_1}
[topological_space α]
{x : nnreal}
{f : ennreal → α} :
continuous_at f ↑x ↔ continuous_at (f ∘ coe) x
theorem
ennreal.tendsto_of_real
{α : Type u_1}
{f : filter α}
{m : α → ℝ}
{a : ℝ}
(h : filter.tendsto m f (nhds a)) :
filter.tendsto (λ (a : α), ennreal.of_real (m a)) f (nhds (ennreal.of_real a))
theorem
ennreal.tendsto_to_nnreal
{a : ennreal}
(ha : a ≠ ⊤) :
filter.tendsto ennreal.to_nnreal (nhds a) (nhds a.to_nnreal)
theorem
ennreal.tendsto_to_real
{a : ennreal}
(ha : a ≠ ⊤) :
filter.tendsto ennreal.to_real (nhds a) (nhds a.to_real)
The set of finite ℝ≥0∞ numbers is homeomorphic to ℝ≥0.
Equations
- ennreal.ne_top_homeomorph_nnreal = {to_equiv := {to_fun := ennreal.ne_top_equiv_nnreal.to_fun, inv_fun := ennreal.ne_top_equiv_nnreal.inv_fun, left_inv := ennreal.ne_top_homeomorph_nnreal._proof_1, right_inv := ennreal.ne_top_homeomorph_nnreal._proof_2}, continuous_to_fun := ennreal.ne_top_homeomorph_nnreal._proof_3, continuous_inv_fun := ennreal.ne_top_homeomorph_nnreal._proof_4}
The set of finite ℝ≥0∞ numbers is homeomorphic to ℝ≥0.
Equations
- ennreal.lt_top_homeomorph_nnreal = (homeomorph.set_congr ennreal.lt_top_homeomorph_nnreal._proof_1).trans ennreal.ne_top_homeomorph_nnreal
@[simp, norm_cast]
theorem
ennreal.tendsto_coe_nhds_top
{α : Type u_1}
{f : α → nnreal}
{l : filter α} :
filter.tendsto (λ (x : α), ↑(f x)) l (nhds ⊤) ↔ filter.tendsto f l filter.at_top
@[instance]
@[protected]
theorem
ennreal.tendsto_nhds
{α : Type u_1}
{f : filter α}
{u : α → ennreal}
{a : ennreal}
(ha : a ≠ ⊤) :
Characterization of neighborhoods for ℝ≥0∞ numbers. See also tendsto_order
for a version with strict inequalities.
@[protected]
theorem
ennreal.tendsto.sub
{α : Type u_1}
{f : filter α}
{ma mb : α → ennreal}
{a b : ennreal}
(hma : filter.tendsto ma f (nhds a))
(hmb : filter.tendsto mb f (nhds b))
(h : a ≠ ⊤ ∨ b ≠ ⊤) :
filter.tendsto (λ (a : α), ma a - mb a) f (nhds (a - b))
theorem
continuous_on.ennreal_mul
{α : Type u_1}
[topological_space α]
{f g : α → ennreal}
{s : set α}
(hf : continuous_on f s)
(hg : continuous_on g s)
(h₁ : ∀ (x : α), x ∈ s → f x ≠ 0 ∨ g x ≠ ⊤)
(h₂ : ∀ (x : α), x ∈ s → g x ≠ 0 ∨ f x ≠ ⊤) :
continuous_on (λ (x : α), f x * g x) s
theorem
continuous.ennreal_mul
{α : Type u_1}
[topological_space α]
{f g : α → ennreal}
(hf : continuous f)
(hg : continuous g)
(h₁ : ∀ (x : α), f x ≠ 0 ∨ g x ≠ ⊤)
(h₂ : ∀ (x : α), g x ≠ 0 ∨ f x ≠ ⊤) :
continuous (λ (x : α), f x * g x)
theorem
ennreal.tendsto_finset_prod_of_ne_top
{α : Type u_1}
{ι : Type u_2}
{f : ι → α → ennreal}
{x : filter α}
{a : ι → ennreal}
(s : finset ι)
(h : ∀ (i : ι), i ∈ s → filter.tendsto (f i) x (nhds (a i)))
(h' : ∀ (i : ι), i ∈ s → a i ≠ ⊤) :
filter.tendsto (λ (b : α), s.prod (λ (c : ι), f c b)) x (nhds (s.prod (λ (c : ι), a c)))
@[protected]
theorem
ennreal.continuous_at_const_mul
{a b : ennreal}
(h : a ≠ ⊤ ∨ b ≠ 0) :
continuous_at (has_mul.mul a) b
@[protected]
theorem
ennreal.continuous_at_mul_const
{a b : ennreal}
(h : a ≠ ⊤ ∨ b ≠ 0) :
continuous_at (λ (x : ennreal), x * a) b
@[protected]
@[protected]
theorem
ennreal.continuous_mul_const
{a : ennreal}
(ha : a ≠ ⊤) :
continuous (λ (x : ennreal), x * a)
@[protected]
theorem
ennreal.continuous_div_const
(c : ennreal)
(c_ne_zero : c ≠ 0) :
continuous (λ (x : ennreal), x / c)
theorem
ennreal.continuous_sub_left
{a : ennreal}
(a_ne_top : a ≠ ⊤) :
continuous (λ (x : ennreal), a - x)
@[protected]
theorem
ennreal.tendsto.pow
{α : Type u_1}
{f : filter α}
{m : α → ennreal}
{a : ennreal}
{n : ℕ}
(hm : filter.tendsto m f (nhds a)) :
filter.tendsto (λ (x : α), m x ^ n) f (nhds (a ^ n))
theorem
ennreal.inv_limsup
{ι : Type u_1}
{x : ι → ennreal}
{l : filter ι} :
(filter.limsup x l)⁻¹ = filter.liminf (λ (i : ι), (x i)⁻¹) l
theorem
ennreal.inv_liminf
{ι : Type u_1}
{x : ι → ennreal}
{l : filter ι} :
(filter.liminf x l)⁻¹ = filter.limsup (λ (i : ι), (x i)⁻¹) l
@[protected, simp]
theorem
ennreal.tendsto_inv_iff
{α : Type u_1}
{f : filter α}
{m : α → ennreal}
{a : ennreal} :
filter.tendsto (λ (x : α), (m x)⁻¹) f (nhds a⁻¹) ↔ filter.tendsto m f (nhds a)
@[protected]
theorem
ennreal.tendsto_inv_nat_nhds_zero
:
filter.tendsto (λ (n : ℕ), (↑n)⁻¹) filter.at_top (nhds 0)
theorem
ennreal.exists_upcrossings_of_not_bounded_under
{ι : Type u_1}
{l : filter ι}
{x : ι → ℝ}
(hf : filter.liminf (λ (i : ι), ↑(⇑real.nnabs (x i))) l ≠ ⊤)
(hbdd : ¬filter.is_bounded_under has_le.le l (λ (i : ι), |x i|)) :
@[protected]
theorem
ennreal.tsum_eq_supr_nat'
{f : ℕ → ennreal}
{N : ℕ → ℕ}
(hN : filter.tendsto N filter.at_top filter.at_top) :
@[protected]
theorem
ennreal.tsum_eq_liminf_sum_nat
{f : ℕ → ennreal} :
∑' (i : ℕ), f i = filter.liminf (λ (n : ℕ), (finset.range n).sum (λ (i : ℕ), f i)) filter.at_top
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
ennreal.tendsto_nat_tsum
(f : ℕ → ennreal) :
filter.tendsto (λ (n : ℕ), (finset.range n).sum (λ (i : ℕ), f i)) filter.at_top (nhds (∑' (n : ℕ), f n))
theorem
ennreal.tendsto_at_top_zero_of_tsum_ne_top
{f : ℕ → ennreal}
(hf : ∑' (x : ℕ), f x ≠ ⊤) :
filter.tendsto f filter.at_top (nhds 0)
theorem
ennreal.tendsto_tsum_compl_at_top_zero
{α : Type u_1}
{f : α → ennreal}
(hf : ∑' (x : α), f x ≠ ⊤) :
filter.tendsto (λ (s : finset α), ∑' (b : {x // x ∉ s}), f ↑b) filter.at_top (nhds 0)
The sum over the complement of a finset tends to 0 when the finset grows to cover the whole
space. This does not need a summability assumption, as otherwise all sums are zero.
theorem
nnreal.has_sum_iff_tendsto_nat
{f : ℕ → nnreal}
{r : nnreal} :
has_sum f r ↔ filter.tendsto (λ (n : ℕ), (finset.range n).sum (λ (i : ℕ), f i)) filter.at_top (nhds r)
A series of non-negative real numbers converges to r in the sense of has_sum if and only if
the sequence of partial sum converges to r.
theorem
nnreal.not_summable_iff_tendsto_nat_at_top
{f : ℕ → nnreal} :
¬summable f ↔ filter.tendsto (λ (n : ℕ), (finset.range n).sum (λ (i : ℕ), f i)) filter.at_top filter.at_top
theorem
nnreal.summable_iff_not_tendsto_nat_at_top
{f : ℕ → nnreal} :
summable f ↔ ¬filter.tendsto (λ (n : ℕ), (finset.range n).sum (λ (i : ℕ), f i)) filter.at_top filter.at_top
theorem
nnreal.tendsto_sum_nat_add
(f : ℕ → nnreal) :
filter.tendsto (λ (i : ℕ), ∑' (k : ℕ), f (k + i)) filter.at_top (nhds 0)
For f : ℕ → ℝ≥0, then ∑' k, f (k + i) tends to zero. This does not require a summability
assumption on f, as otherwise all sums are zero.
theorem
has_sum_iff_tendsto_nat_of_nonneg
{f : ℕ → ℝ}
(hf : ∀ (i : ℕ), 0 ≤ f i)
(r : ℝ) :
has_sum f r ↔ filter.tendsto (λ (n : ℕ), (finset.range n).sum (λ (i : ℕ), f i)) filter.at_top (nhds r)
A series of non-negative real numbers converges to r in the sense of has_sum if and only if
the sequence of partial sum converges to r.
theorem
ennreal.of_real_tsum_of_nonneg
{α : Type u_1}
{f : α → ℝ}
(hf_nonneg : ∀ (n : α), 0 ≤ f n)
(hf : summable f) :
ennreal.of_real (∑' (n : α), f n) = ∑' (n : α), ennreal.of_real (f n)
theorem
not_summable_iff_tendsto_nat_at_top_of_nonneg
{f : ℕ → ℝ}
(hf : ∀ (n : ℕ), 0 ≤ f n) :
¬summable f ↔ filter.tendsto (λ (n : ℕ), (finset.range n).sum (λ (i : ℕ), f i)) filter.at_top filter.at_top
theorem
summable_iff_not_tendsto_nat_at_top_of_nonneg
{f : ℕ → ℝ}
(hf : ∀ (n : ℕ), 0 ≤ f n) :
summable f ↔ ¬filter.tendsto (λ (n : ℕ), (finset.range n).sum (λ (i : ℕ), f i)) filter.at_top filter.at_top
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) :
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}
[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}
[pseudo_emetric_space α]
{l : filter β}
{f : β → α}
{y : α} :
filter.tendsto f l (nhds y) ↔ filter.tendsto (λ (x : β), has_edist.edist (f x) y) l (nhds 0)
theorem
emetric.cauchy_seq_iff_le_tendsto_0
{α : Type u_1}
{β : Type u_2}
[pseudo_emetric_space α]
[nonempty β]
[semilattice_sup β]
{s : β → α} :
cauchy_seq s ↔ ∃ (b : β → ennreal), (∀ (n m N : β), N ≤ n → N ≤ m → has_edist.edist (s n) (s m) ≤ b N) ∧ filter.tendsto b filter.at_top (nhds 0)
Yet another metric characterization of Cauchy sequences on integers. This one is often the most efficient.
theorem
continuous_of_le_add_edist
{α : Type u_1}
[pseudo_emetric_space α]
{f : α → ennreal}
(C : ennreal)
(hC : C ≠ ⊤)
(h : ∀ (x y : α), f x ≤ f y + C * has_edist.edist x y) :
theorem
continuous_edist
{α : Type u_1}
[pseudo_emetric_space α] :
continuous (λ (p : α × α), has_edist.edist p.fst p.snd)
@[continuity]
theorem
continuous.edist
{α : Type u_1}
{β : Type u_2}
[pseudo_emetric_space α]
[topological_space β]
{f g : β → α}
(hf : continuous f)
(hg : continuous g) :
continuous (λ (b : β), has_edist.edist (f b) (g b))
theorem
filter.tendsto.edist
{α : Type u_1}
{β : Type u_2}
[pseudo_emetric_space α]
{f g : β → α}
{x : filter β}
{a b : α}
(hf : filter.tendsto f x (nhds a))
(hg : filter.tendsto g x (nhds b)) :
filter.tendsto (λ (x : β), has_edist.edist (f x) (g x)) x (nhds (has_edist.edist a b))
theorem
emetric.is_closed_ball
{α : Type u_1}
[pseudo_emetric_space α]
{a : α}
{r : ennreal} :
is_closed (emetric.closed_ball a r)
@[simp]
theorem
emetric.diam_closure
{α : Type u_1}
[pseudo_emetric_space α]
(s : set α) :
emetric.diam (closure s) = emetric.diam s
@[simp]
theorem
metric.diam_closure
{α : Type u_1}
[pseudo_metric_space α]
(s : set α) :
metric.diam (closure s) = metric.diam s
theorem
is_closed_set_of_lipschitz_on_with
{α : Type u_1}
{β : Type u_2}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(K : nnreal)
(s : set α) :
is_closed {f : α → β | lipschitz_on_with K f s}
theorem
is_closed_set_of_lipschitz_with
{α : Type u_1}
{β : Type u_2}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(K : nnreal) :
is_closed {f : α → β | lipschitz_with K f}
theorem
real.ediam_eq
{s : set ℝ}
(h : metric.bounded s) :
emetric.diam s = ennreal.of_real (has_Sup.Sup s - has_Inf.Inf s)
For a bounded set s : set ℝ, its emetric.diam is equal to Sup s - Inf s reinterpreted as
ℝ≥0∞.
theorem
real.diam_eq
{s : set ℝ}
(h : metric.bounded s) :
metric.diam s = has_Sup.Sup s - has_Inf.Inf s
For a bounded set s : set ℝ, its metric.diam is equal to Sup s - Inf s.
@[simp]
@[simp]
@[simp]
@[simp]
theorem
edist_le_tsum_of_edist_le_of_tendsto
{α : Type u_1}
[pseudo_emetric_space α]
{f : ℕ → α}
(d : ℕ → ennreal)
(hf : ∀ (n : ℕ), has_edist.edist (f n) (f n.succ) ≤ d n)
{a : α}
(ha : filter.tendsto f filter.at_top (nhds a))
(n : ℕ) :
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}
[pseudo_emetric_space α]
{f : ℕ → α}
(d : ℕ → ennreal)
(hf : ∀ (n : ℕ), has_edist.edist (f n) (f n.succ) ≤ d n)
{a : α}
(ha : filter.tendsto f filter.at_top (nhds a)) :
has_edist.edist (f 0) a ≤ ∑' (m : ℕ), d m
If edist (f n) (f (n+1)) is bounded above by a function d : ℕ → ℝ≥0∞,
then the distance from f 0 to the limit is bounded by ∑'_{k=0}^∞ d k.