theorem
tendsto_iff_norm_div_tendsto_zero
{α : Type u_2}
{E : Type u_5}
[SeminormedGroup E]
{f : α → E}
{a : Filter α}
{b : E}
:
theorem
tendsto_iff_norm_sub_tendsto_zero
{α : Type u_2}
{E : Type u_5}
[SeminormedAddGroup E]
{f : α → E}
{a : Filter α}
{b : E}
:
theorem
tendsto_one_iff_norm_tendsto_zero
{α : Type u_2}
{E : Type u_5}
[SeminormedGroup E]
{f : α → E}
{a : Filter α}
:
theorem
tendsto_zero_iff_norm_tendsto_zero
{α : Type u_2}
{E : Type u_5}
[SeminormedAddGroup E]
{f : α → E}
{a : Filter α}
:
theorem
squeeze_one_norm'
{α : Type u_2}
{E : Type u_5}
[SeminormedGroup E]
{f : α → E}
{a : α → ℝ}
{t₀ : Filter α}
(h : ∀ᶠ (n : α) in t₀, ‖f n‖ ≤ a n)
(h' : Filter.Tendsto a t₀ (nhds 0))
:
Filter.Tendsto f t₀ (nhds 1)
Special case of the sandwich theorem: if the norm of f is eventually bounded by a real
function a which tends to 0, then f tends to 1 (neutral element of SeminormedGroup).
In this pair of lemmas (squeeze_one_norm' and squeeze_one_norm), following a convention of
similar lemmas in Topology.MetricSpace.Basic and Topology.Algebra.Order, the ' version is
phrased using "eventually" and the non-' version is phrased absolutely.
theorem
squeeze_zero_norm'
{α : Type u_2}
{E : Type u_5}
[SeminormedAddGroup E]
{f : α → E}
{a : α → ℝ}
{t₀ : Filter α}
(h : ∀ᶠ (n : α) in t₀, ‖f n‖ ≤ a n)
(h' : Filter.Tendsto a t₀ (nhds 0))
:
Filter.Tendsto f t₀ (nhds 0)
Special case of the sandwich theorem: if the norm of f is eventually bounded by a
real function a which tends to 0, then f tends to 0. In this pair of lemmas
(squeeze_zero_norm' and squeeze_zero_norm), following a convention of similar lemmas in
Topology.MetricSpace.Pseudo.Defs and Topology.Algebra.Order, the ' version is phrased using
"eventually" and the non-' version is phrased absolutely.
theorem
squeeze_one_norm
{α : Type u_2}
{E : Type u_5}
[SeminormedGroup E]
{f : α → E}
{a : α → ℝ}
{t₀ : Filter α}
(h : ∀ (n : α), ‖f n‖ ≤ a n)
:
Filter.Tendsto a t₀ (nhds 0) → Filter.Tendsto f t₀ (nhds 1)
Special case of the sandwich theorem: if the norm of f is bounded by a real function a which
tends to 0, then f tends to 1.
theorem
squeeze_zero_norm
{α : Type u_2}
{E : Type u_5}
[SeminormedAddGroup E]
{f : α → E}
{a : α → ℝ}
{t₀ : Filter α}
(h : ∀ (n : α), ‖f n‖ ≤ a n)
:
Filter.Tendsto a t₀ (nhds 0) → Filter.Tendsto f t₀ (nhds 0)
Special case of the sandwich theorem: if the norm of f is bounded by a real
function a which tends to 0, then f tends to 0.
theorem
tendsto_norm_div_self_nhdsGE
{E : Type u_5}
[SeminormedGroup E]
(x : E)
:
Filter.Tendsto (fun (a : E) => ‖a / x‖) (nhds x) (nhdsWithin 0 (Set.Ici 0))
theorem
tendsto_norm_sub_self_nhdsGE
{E : Type u_5}
[SeminormedAddGroup E]
(x : E)
:
Filter.Tendsto (fun (a : E) => ‖a - x‖) (nhds x) (nhdsWithin 0 (Set.Ici 0))
theorem
tendsto_norm_one
{E : Type u_5}
[SeminormedGroup E]
:
Filter.Tendsto (fun (a : E) => ‖a‖) (nhds 1) (nhds 0)
See tendsto_norm_one for a version with pointed neighborhoods.
theorem
tendsto_norm_zero
{E : Type u_5}
[SeminormedAddGroup E]
:
Filter.Tendsto (fun (a : E) => ‖a‖) (nhds 0) (nhds 0)
See tendsto_norm_zero for a version with pointed neighborhoods.
theorem
Inseparable.norm_eq_norm'
{E : Type u_5}
[SeminormedGroup E]
{u v : E}
(h : Inseparable u v)
:
theorem
Inseparable.norm_eq_norm
{E : Type u_5}
[SeminormedAddGroup E]
{u v : E}
(h : Inseparable u v)
:
theorem
Inseparable.nnnorm_eq_nnnorm'
{E : Type u_5}
[SeminormedGroup E]
{u v : E}
(h : Inseparable u v)
:
theorem
Inseparable.nnnorm_eq_nnnorm
{E : Type u_5}
[SeminormedAddGroup E]
{u v : E}
(h : Inseparable u v)
:
theorem
Continuous.norm'
{α : Type u_2}
{E : Type u_5}
[SeminormedGroup E]
[TopologicalSpace α]
{f : α → E}
:
Continuous f → Continuous fun (x : α) => ‖f x‖
theorem
Continuous.norm
{α : Type u_2}
{E : Type u_5}
[SeminormedAddGroup E]
[TopologicalSpace α]
{f : α → E}
:
Continuous f → Continuous fun (x : α) => ‖f x‖
theorem
Continuous.nnnorm'
{α : Type u_2}
{E : Type u_5}
[SeminormedGroup E]
[TopologicalSpace α]
{f : α → E}
:
Continuous f → Continuous fun (x : α) => ‖f x‖₊
theorem
Continuous.nnnorm
{α : Type u_2}
{E : Type u_5}
[SeminormedAddGroup E]
[TopologicalSpace α]
{f : α → E}
:
Continuous f → Continuous fun (x : α) => ‖f x‖₊
theorem
Continuous.enorm'
{α : Type u_2}
{E : Type u_5}
[SeminormedGroup E]
[TopologicalSpace α]
{f : α → E}
:
Continuous f → Continuous fun (x : α) => ‖f x‖ₑ
theorem
Continuous.enorm
{α : Type u_2}
{E : Type u_5}
[SeminormedAddGroup E]
[TopologicalSpace α]
{f : α → E}
:
Continuous f → Continuous fun (x : α) => ‖f x‖ₑ
theorem
ContinuousAt.norm'
{α : Type u_2}
{E : Type u_5}
[SeminormedGroup E]
[TopologicalSpace α]
{f : α → E}
{a : α}
(h : ContinuousAt f a)
:
ContinuousAt (fun (x : α) => ‖f x‖) a
theorem
ContinuousAt.norm
{α : Type u_2}
{E : Type u_5}
[SeminormedAddGroup E]
[TopologicalSpace α]
{f : α → E}
{a : α}
(h : ContinuousAt f a)
:
ContinuousAt (fun (x : α) => ‖f x‖) a
theorem
ContinuousAt.nnnorm'
{α : Type u_2}
{E : Type u_5}
[SeminormedGroup E]
[TopologicalSpace α]
{f : α → E}
{a : α}
(h : ContinuousAt f a)
:
ContinuousAt (fun (x : α) => ‖f x‖₊) a
theorem
ContinuousAt.nnnorm
{α : Type u_2}
{E : Type u_5}
[SeminormedAddGroup E]
[TopologicalSpace α]
{f : α → E}
{a : α}
(h : ContinuousAt f a)
:
ContinuousAt (fun (x : α) => ‖f x‖₊) a
theorem
ContinuousAt.enorm'
{α : Type u_2}
{E : Type u_5}
[SeminormedGroup E]
[TopologicalSpace α]
{f : α → E}
{a : α}
(h : ContinuousAt f a)
:
ContinuousAt (fun (x : α) => ‖f x‖ₑ) a
theorem
ContinuousAt.enorm
{α : Type u_2}
{E : Type u_5}
[SeminormedAddGroup E]
[TopologicalSpace α]
{f : α → E}
{a : α}
(h : ContinuousAt f a)
:
ContinuousAt (fun (x : α) => ‖f x‖ₑ) a
theorem
ContinuousWithinAt.norm'
{α : Type u_2}
{E : Type u_5}
[SeminormedGroup E]
[TopologicalSpace α]
{f : α → E}
{s : Set α}
{a : α}
(h : ContinuousWithinAt f s a)
:
ContinuousWithinAt (fun (x : α) => ‖f x‖) s a
theorem
ContinuousWithinAt.norm
{α : Type u_2}
{E : Type u_5}
[SeminormedAddGroup E]
[TopologicalSpace α]
{f : α → E}
{s : Set α}
{a : α}
(h : ContinuousWithinAt f s a)
:
ContinuousWithinAt (fun (x : α) => ‖f x‖) s a
theorem
ContinuousWithinAt.nnnorm'
{α : Type u_2}
{E : Type u_5}
[SeminormedGroup E]
[TopologicalSpace α]
{f : α → E}
{s : Set α}
{a : α}
(h : ContinuousWithinAt f s a)
:
ContinuousWithinAt (fun (x : α) => ‖f x‖₊) s a
theorem
ContinuousWithinAt.nnnorm
{α : Type u_2}
{E : Type u_5}
[SeminormedAddGroup E]
[TopologicalSpace α]
{f : α → E}
{s : Set α}
{a : α}
(h : ContinuousWithinAt f s a)
:
ContinuousWithinAt (fun (x : α) => ‖f x‖₊) s a
theorem
ContinuousWithinAt.enorm'
{α : Type u_2}
{E : Type u_5}
[SeminormedGroup E]
[TopologicalSpace α]
{f : α → E}
{s : Set α}
{a : α}
(h : ContinuousWithinAt f s a)
:
ContinuousWithinAt (fun (x : α) => ‖f x‖ₑ) s a
theorem
ContinuousWithinAt.enorm
{α : Type u_2}
{E : Type u_5}
[SeminormedAddGroup E]
[TopologicalSpace α]
{f : α → E}
{s : Set α}
{a : α}
(h : ContinuousWithinAt f s a)
:
ContinuousWithinAt (fun (x : α) => ‖f x‖ₑ) s a
theorem
ContinuousOn.norm'
{α : Type u_2}
{E : Type u_5}
[SeminormedGroup E]
[TopologicalSpace α]
{f : α → E}
{s : Set α}
(h : ContinuousOn f s)
:
ContinuousOn (fun (x : α) => ‖f x‖) s
theorem
ContinuousOn.norm
{α : Type u_2}
{E : Type u_5}
[SeminormedAddGroup E]
[TopologicalSpace α]
{f : α → E}
{s : Set α}
(h : ContinuousOn f s)
:
ContinuousOn (fun (x : α) => ‖f x‖) s
theorem
ContinuousOn.nnnorm'
{α : Type u_2}
{E : Type u_5}
[SeminormedGroup E]
[TopologicalSpace α]
{f : α → E}
{s : Set α}
(h : ContinuousOn f s)
:
ContinuousOn (fun (x : α) => ‖f x‖₊) s
theorem
ContinuousOn.nnnorm
{α : Type u_2}
{E : Type u_5}
[SeminormedAddGroup E]
[TopologicalSpace α]
{f : α → E}
{s : Set α}
(h : ContinuousOn f s)
:
ContinuousOn (fun (x : α) => ‖f x‖₊) s
theorem
ContinuousOn.enorm'
{α : Type u_2}
{E : Type u_5}
[SeminormedGroup E]
[TopologicalSpace α]
{f : α → E}
{s : Set α}
(h : ContinuousOn f s)
:
ContinuousOn (fun (x : α) => ‖f x‖ₑ) s
theorem
ContinuousOn.enorm
{α : Type u_2}
{E : Type u_5}
[SeminormedAddGroup E]
[TopologicalSpace α]
{f : α → E}
{s : Set α}
(h : ContinuousOn f s)
:
ContinuousOn (fun (x : α) => ‖f x‖ₑ) s
theorem
eventually_ne_of_tendsto_norm_atTop'
{α : Type u_2}
{E : Type u_5}
[SeminormedGroup E]
{l : Filter α}
{f : α → E}
(h : Filter.Tendsto (fun (y : α) => ‖f y‖) l Filter.atTop)
(x : E)
:
If ‖y‖ → ∞, then we can assume y ≠ x for any fixed x.
theorem
eventually_ne_of_tendsto_norm_atTop
{α : Type u_2}
{E : Type u_5}
[SeminormedAddGroup E]
{l : Filter α}
{f : α → E}
(h : Filter.Tendsto (fun (y : α) => ‖f y‖) l Filter.atTop)
(x : E)
:
If ‖y‖→∞, then we can assume y≠x for any
fixed x
theorem
SeminormedGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_one
{ι : Type u_3}
{κ : Type u_4}
{G : Type u_7}
[SeminormedGroup G]
{f : ι → κ → G}
{l : Filter ι}
{l' : Filter κ}
:
UniformCauchySeqOnFilter f l l' ↔ TendstoUniformlyOnFilter (fun (n : ι × ι) (z : κ) => f n.1 z / f n.2 z) 1 (l ×ˢ l) l'
theorem
SeminormedAddGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_zero
{ι : Type u_3}
{κ : Type u_4}
{G : Type u_7}
[SeminormedAddGroup G]
{f : ι → κ → G}
{l : Filter ι}
{l' : Filter κ}
:
UniformCauchySeqOnFilter f l l' ↔ TendstoUniformlyOnFilter (fun (n : ι × ι) (z : κ) => f n.1 z - f n.2 z) 0 (l ×ˢ l) l'
theorem
SeminormedGroup.uniformCauchySeqOn_iff_tendstoUniformlyOn_one
{ι : Type u_3}
{κ : Type u_4}
{G : Type u_7}
[SeminormedGroup G]
{f : ι → κ → G}
{s : Set κ}
{l : Filter ι}
:
UniformCauchySeqOn f l s ↔ TendstoUniformlyOn (fun (n : ι × ι) (z : κ) => f n.1 z / f n.2 z) 1 (l ×ˢ l) s
theorem
SeminormedAddGroup.uniformCauchySeqOn_iff_tendstoUniformlyOn_zero
{ι : Type u_3}
{κ : Type u_4}
{G : Type u_7}
[SeminormedAddGroup G]
{f : ι → κ → G}
{s : Set κ}
{l : Filter ι}
:
UniformCauchySeqOn f l s ↔ TendstoUniformlyOn (fun (n : ι × ι) (z : κ) => f n.1 z - f n.2 z) 0 (l ×ˢ l) s
theorem
controlled_prod_of_mem_closure
{E : Type u_5}
[SeminormedCommGroup E]
{a : E}
{s : Subgroup E}
(hg : a ∈ closure ↑s)
{b : ℕ → ℝ}
(b_pos : ∀ (n : ℕ), 0 < b n)
:
theorem
controlled_sum_of_mem_closure
{E : Type u_5}
[SeminormedAddCommGroup E]
{a : E}
{s : AddSubgroup E}
(hg : a ∈ closure ↑s)
{b : ℕ → ℝ}
(b_pos : ∀ (n : ℕ), 0 < b n)
:
theorem
controlled_prod_of_mem_closure_range
{E : Type u_5}
{F : Type u_6}
[SeminormedCommGroup E]
[SeminormedCommGroup F]
{j : E →* F}
{b : F}
(hb : b ∈ closure ↑j.range)
{f : ℕ → ℝ}
(b_pos : ∀ (n : ℕ), 0 < f n)
:
theorem
controlled_sum_of_mem_closure_range
{E : Type u_5}
{F : Type u_6}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
{j : E →+ F}
{b : F}
(hb : b ∈ closure ↑j.range)
{f : ℕ → ℝ}
(b_pos : ∀ (n : ℕ), 0 < f n)
:
theorem
tendsto_norm_nhdsNE_one
{E : Type u_5}
[NormedGroup E]
:
Filter.Tendsto norm (nhdsWithin 1 {1}ᶜ) (nhdsWithin 0 (Set.Ioi 0))
See tendsto_norm_one for a version with full neighborhoods.
theorem
tendsto_norm_nhdsNE_zero
{E : Type u_5}
[NormedAddGroup E]
:
Filter.Tendsto norm (nhdsWithin 0 {0}ᶜ) (nhdsWithin 0 (Set.Ioi 0))
See tendsto_norm_zero for a version with full neighborhoods.
@[deprecated tendsto_norm_nhdsNE_zero (since := "2024-12-22")]
theorem
tendsto_norm_zero'
{E : Type u_5}
[NormedAddGroup E]
:
Filter.Tendsto norm (nhdsWithin 0 {0}ᶜ) (nhdsWithin 0 (Set.Ioi 0))
Alias of tendsto_norm_nhdsNE_zero.
See tendsto_norm_zero for a version with full neighborhoods.
@[deprecated tendsto_norm_nhdsNE_one (since := "2024-12-22")]
theorem
tendsto_norm_one'
{E : Type u_5}
[NormedGroup E]
:
Filter.Tendsto norm (nhdsWithin 1 {1}ᶜ) (nhdsWithin 0 (Set.Ioi 0))
Alias of tendsto_norm_nhdsNE_one.
See tendsto_norm_one for a version with full neighborhoods.
@[deprecated tendsto_norm_nhdsNE_zero (since := "2024-12-22")]
theorem
tendsto_norm_nhdsWithin_zero
{E : Type u_5}
[NormedAddGroup E]
:
Filter.Tendsto norm (nhdsWithin 0 {0}ᶜ) (nhdsWithin 0 (Set.Ioi 0))
Alias of tendsto_norm_nhdsNE_zero.
See tendsto_norm_zero for a version with full neighborhoods.
@[deprecated tendsto_norm_nhdsNE_one (since := "2024-12-22")]
theorem
tendsto_norm_nhdsWithin_one
{E : Type u_5}
[NormedGroup E]
:
Filter.Tendsto norm (nhdsWithin 1 {1}ᶜ) (nhdsWithin 0 (Set.Ioi 0))
Alias of tendsto_norm_nhdsNE_one.
See tendsto_norm_one for a version with full neighborhoods.
theorem
tendsto_norm_div_self_nhdsNE
{E : Type u_5}
[NormedGroup E]
(a : E)
:
Filter.Tendsto (fun (x : E) => ‖x / a‖) (nhdsWithin a {a}ᶜ) (nhdsWithin 0 (Set.Ioi 0))
theorem
tendsto_norm_sub_self_nhdsNE
{E : Type u_5}
[NormedAddGroup E]
(a : E)
:
Filter.Tendsto (fun (x : E) => ‖x - a‖) (nhdsWithin a {a}ᶜ) (nhdsWithin 0 (Set.Ioi 0))
@[deprecated tendsto_norm_sub_self_nhdsNE (since := "2024-12-22")]
theorem
tendsto_norm_sub_self_punctured_nhds
{E : Type u_5}
[NormedAddGroup E]
(a : E)
:
Filter.Tendsto (fun (x : E) => ‖x - a‖) (nhdsWithin a {a}ᶜ) (nhdsWithin 0 (Set.Ioi 0))
Alias of tendsto_norm_sub_self_nhdsNE.
@[deprecated tendsto_norm_div_self_nhdsNE (since := "2024-12-22")]
theorem
tendsto_norm_div_self_punctured_nhds
{E : Type u_5}
[NormedGroup E]
(a : E)
:
Filter.Tendsto (fun (x : E) => ‖x / a‖) (nhdsWithin a {a}ᶜ) (nhdsWithin 0 (Set.Ioi 0))
Alias of tendsto_norm_div_self_nhdsNE.
A version of comap_norm_nhdsGT_zero for a multiplicative normed group.
@[deprecated comap_norm_nhdsGT_zero (since := "2024-12-22")]
Alias of comap_norm_nhdsGT_zero.
@[deprecated comap_norm_nhdsGT_zero' (since := "2024-12-22")]
Alias of comap_norm_nhdsGT_zero'.
A version of comap_norm_nhdsGT_zero for a multiplicative normed group.