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 α}
:
@[simp]
@[simp]
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.
Equations
- SeminormedGroup.toContinuousENorm = { toENorm := NNNorm.toENorm, continuous_enorm := ⋯ }
Equations
- SeminormedAddGroup.toContinuousENorm = { toENorm := NNNorm.toENorm, continuous_enorm := ⋯ }
Equations
- NormedGroup.toENormedMonoid = { toContinuousENorm := SeminormedGroup.toContinuousENorm, toMonoid := inst✝.toMonoid, enorm_zero := ⋯, enorm_mul_le := ⋯, enorm_eq_zero := ⋯ }
Equations
- NormedAddGroup.toENormedAddMonoid = { toContinuousENorm := SeminormedAddGroup.toContinuousENorm, toAddMonoid := inst✝.toAddMonoid, enorm_zero := ⋯, enorm_add_le := ⋯, enorm_eq_zero := ⋯ }
Equations
- NormedCommGroup.toENormedCommMonoid = { toESeminormedMonoid := NormedGroup.toENormedMonoid.toESeminormedMonoid, mul_comm := ⋯, enorm_eq_zero := ⋯ }
Equations
- NormedAddCommGroup.toENormedAddCommMonoid = { toESeminormedAddMonoid := NormedAddGroup.toENormedAddMonoid.toESeminormedAddMonoid, add_comm := ⋯, enorm_eq_zero := ⋯ }
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
Inseparable.enorm_eq_enorm'
{E : Type u_8}
[TopologicalSpace E]
[ContinuousENorm E]
{u v : E}
(h : Inseparable u v)
:
theorem
Inseparable.enorm_eq_enorm
{E : Type u_8}
[TopologicalSpace E]
[ContinuousENorm 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
Filter.Tendsto.enorm'
{α : Type u_2}
{E : Type u_5}
[TopologicalSpace E]
[ContinuousENorm E]
{a : E}
{l : Filter α}
{f : α → E}
(h : Tendsto f l (nhds a))
:
theorem
Filter.Tendsto.enorm
{α : Type u_2}
{E : Type u_5}
[TopologicalSpace E]
[ContinuousENorm E]
{a : E}
{l : Filter α}
{f : α → E}
(h : Tendsto f l (nhds a))
:
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
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
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
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.
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))
A version of comap_norm_nhdsGT_zero for a multiplicative normed group.