Documentation

theorem ContinuousAt.enorm {E : Type u_7} [TopologicalSpace E] [ContinuousENorm E] {X : Type u_8} [TopologicalSpace X] {f : X → E} {a : X} (h : ContinuousAt f a) :

ContinuousAt (fun (x : X) => ‖f x‖ₑ) a

theorem ContinuousWithinAt.enorm {E : Type u_7} [TopologicalSpace E] [ContinuousENorm E] {X : Type u_8} [TopologicalSpace X] {f : X → E} {s : Set X} {a : X} (h : ContinuousWithinAt f s a) :

ContinuousWithinAt (fun (x : X) => ‖f x‖ₑ) s a

theorem ContinuousOn.enorm {E : Type u_7} [TopologicalSpace E] [ContinuousENorm E] {X : Type u_8} [TopologicalSpace X] {f : X → E} {s : Set X} (h : ContinuousOn f s) :

ContinuousOn (fun (x : X) => ‖f x‖ₑ) s

theorem tendsto_iff_norm_div_tendsto_zero {α : Type u_1} {E : Type u_4} [SeminormedGroup E] {f : α → E} {a : Filter α} {b : E} :

Filter.Tendsto f a (nhds b) ↔ Filter.Tendsto (fun (e : α) => ‖f e / b‖) a (nhds 0)

theorem tendsto_iff_norm_sub_tendsto_zero {α : Type u_1} {E : Type u_4} [SeminormedAddGroup E] {f : α → E} {a : Filter α} {b : E} :

Filter.Tendsto f a (nhds b) ↔ Filter.Tendsto (fun (e : α) => ‖f e - b‖) a (nhds 0)

theorem tendsto_one_iff_norm_tendsto_zero {α : Type u_1} {E : Type u_4} [SeminormedGroup E] {f : α → E} {a : Filter α} :

Filter.Tendsto f a (nhds 1) ↔ Filter.Tendsto (fun (x : α) => ‖f x‖) a (nhds 0)

theorem tendsto_zero_iff_norm_tendsto_zero {α : Type u_1} {E : Type u_4} [SeminormedAddGroup E] {f : α → E} {a : Filter α} :

Filter.Tendsto f a (nhds 0) ↔ Filter.Tendsto (fun (x : α) => ‖f x‖) a (nhds 0)

@[simp]

theorem comap_norm_nhds_one {E : Type u_4} [SeminormedGroup E] :

Filter.comap norm (nhds 0) = nhds 1

@[simp]

theorem comap_norm_nhds_zero {E : Type u_4} [SeminormedAddGroup E] :

Filter.comap norm (nhds 0) = nhds 0

theorem squeeze_one_norm' {α : Type u_1} {E : Type u_4} [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_1} {E : Type u_4} [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_1} {E : Type u_4} [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_1} {E : Type u_4} [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 {E : Type u_4} [SeminormedGroup E] (x : E) :

Filter.Tendsto (fun (a : E) => ‖a / x‖) (nhds x) (nhds 0)

theorem tendsto_norm_sub_self {E : Type u_4} [SeminormedAddGroup E] (x : E) :

Filter.Tendsto (fun (a : E) => ‖a - x‖) (nhds x) (nhds 0)

theorem tendsto_norm_div_self_nhdsGE {E : Type u_4} [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_4} [SeminormedAddGroup E] (x : E) :

Filter.Tendsto (fun (a : E) => ‖a - x‖) (nhds x) (nhdsWithin 0 (Set.Ici 0))

theorem tendsto_norm' {E : Type u_4} [SeminormedGroup E] {x : E} :

Filter.Tendsto (fun (a : E) => ‖a‖) (nhds x) (nhds ‖x‖)

theorem tendsto_norm {E : Type u_4} [SeminormedAddGroup E] {x : E} :

Filter.Tendsto (fun (a : E) => ‖a‖) (nhds x) (nhds ‖x‖)

theorem tendsto_norm_one {E : Type u_4} [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_4} [SeminormedAddGroup E] :

Filter.Tendsto (fun (a : E) => ‖a‖) (nhds 0) (nhds 0)

See tendsto_norm_zero for a version with pointed neighborhoods.

theorem continuous_norm' {E : Type u_4} [SeminormedGroup E] :

Continuous fun (a : E) => ‖a‖

theorem continuous_norm {E : Type u_4} [SeminormedAddGroup E] :

Continuous fun (a : E) => ‖a‖

theorem continuous_nnnorm' {E : Type u_4} [SeminormedGroup E] :

Continuous fun (a : E) => ‖a‖₊

theorem continuous_nnnorm {E : Type u_4} [SeminormedAddGroup E] :

Continuous fun (a : E) => ‖a‖₊

instance SeminormedGroup.toContinuousENorm {E : Type u_4} [SeminormedGroup E] :

ContinuousENorm E

Equations

instance SeminormedAddGroup.toContinuousENorm {E : Type u_4} [SeminormedAddGroup E] :

ContinuousENorm E

Equations

instance NormedGroup.toENormedMonoid {F : Type u_7} [NormedGroup F] :

ENormedMonoid F

Equations

instance NormedAddGroup.toENormedAddMonoid {F : Type u_7} [NormedAddGroup F] :

ENormedAddMonoid F

Equations

instance NormedCommGroup.toENormedCommMonoid {E : Type u_4} [NormedCommGroup E] :

ENormedCommMonoid E

Equations

instance NormedAddCommGroup.toENormedAddCommMonoid {E : Type u_4} [NormedAddCommGroup E] :

ENormedAddCommMonoid E

Equations

theorem Inseparable.norm_eq_norm' {E : Type u_4} [SeminormedGroup E] {u v : E} (h : Inseparable u v) :

‖u‖ = ‖v‖

theorem Inseparable.norm_eq_norm {E : Type u_4} [SeminormedAddGroup E] {u v : E} (h : Inseparable u v) :

‖u‖ = ‖v‖

theorem Inseparable.nnnorm_eq_nnnorm' {E : Type u_4} [SeminormedGroup E] {u v : E} (h : Inseparable u v) :

‖u‖₊ = ‖v‖₊

theorem Inseparable.nnnorm_eq_nnnorm {E : Type u_4} [SeminormedAddGroup E] {u v : E} (h : Inseparable u v) :

‖u‖₊ = ‖v‖₊

theorem Inseparable.enorm_eq_enorm {E : Type u_7} [TopologicalSpace E] [ContinuousENorm E] {u v : E} (h : Inseparable u v) :

‖u‖ₑ = ‖v‖ₑ

@[deprecated Inseparable.enorm_eq_enorm (since := "2025-12-23")]

theorem Inseparable.enorm_eq_enorm' {E : Type u_7} [TopologicalSpace E] [ContinuousENorm E] {u v : E} (h : Inseparable u v) :

‖u‖ₑ = ‖v‖ₑ

Alias of Inseparable.enorm_eq_enorm.

theorem mem_closure_one_iff_norm {E : Type u_4} [SeminormedGroup E] {x : E} :

x ∈ closure {1} ↔ ‖x‖ = 0

theorem mem_closure_zero_iff_norm {E : Type u_4} [SeminormedAddGroup E] {x : E} :

x ∈ closure {0} ↔ ‖x‖ = 0

theorem closure_one_eq {E : Type u_4} [SeminormedGroup E] :

closure {1} = {x : E | ‖x‖ = 0}

theorem closure_zero_eq {E : Type u_4} [SeminormedAddGroup E] :

closure {0} = {x : E | ‖x‖ = 0}

theorem Filter.Tendsto.norm' {α : Type u_1} {E : Type u_4} [SeminormedGroup E] {a : E} {l : Filter α} {f : α → E} (h : Tendsto f l (nhds a)) :

Tendsto (fun (x : α) => ‖f x‖) l (nhds ‖a‖)

theorem Filter.Tendsto.norm {α : Type u_1} {E : Type u_4} [SeminormedAddGroup E] {a : E} {l : Filter α} {f : α → E} (h : Tendsto f l (nhds a)) :

Tendsto (fun (x : α) => ‖f x‖) l (nhds ‖a‖)

theorem Filter.Tendsto.nnnorm' {α : Type u_1} {E : Type u_4} [SeminormedGroup E] {a : E} {l : Filter α} {f : α → E} (h : Tendsto f l (nhds a)) :

Tendsto (fun (x : α) => ‖f x‖₊) l (nhds ‖a‖₊)

theorem Filter.Tendsto.nnnorm {α : Type u_1} {E : Type u_4} [SeminormedAddGroup E] {a : E} {l : Filter α} {f : α → E} (h : Tendsto f l (nhds a)) :

Tendsto (fun (x : α) => ‖f x‖₊) l (nhds ‖a‖₊)

theorem Continuous.norm' {α : Type u_1} {E : Type u_4} [SeminormedGroup E] [TopologicalSpace α] {f : α → E} :

Continuous f → Continuous fun (x : α) => ‖f x‖

theorem Continuous.norm {α : Type u_1} {E : Type u_4} [SeminormedAddGroup E] [TopologicalSpace α] {f : α → E} :

Continuous f → Continuous fun (x : α) => ‖f x‖

theorem Continuous.nnnorm' {α : Type u_1} {E : Type u_4} [SeminormedGroup E] [TopologicalSpace α] {f : α → E} :

Continuous f → Continuous fun (x : α) => ‖f x‖₊

theorem Continuous.nnnorm {α : Type u_1} {E : Type u_4} [SeminormedAddGroup E] [TopologicalSpace α] {f : α → E} :

Continuous f → Continuous fun (x : α) => ‖f x‖₊

theorem Filter.Tendsto.enorm {α : Type u_1} {E : Type u_4} [TopologicalSpace E] [ContinuousENorm E] {a : E} {l : Filter α} {f : α → E} (h : Tendsto f l (nhds a)) :

Tendsto (fun (x : α) => ‖f x‖ₑ) l (nhds ‖a‖ₑ)

@[deprecated Filter.Tendsto.enorm (since := "2025-12-23")]

theorem Filter.Tendsto.enorm' {α : Type u_1} {E : Type u_4} [TopologicalSpace E] [ContinuousENorm E] {a : E} {l : Filter α} {f : α → E} (h : Tendsto f l (nhds a)) :

Tendsto (fun (x : α) => ‖f x‖ₑ) l (nhds ‖a‖ₑ)

Alias of Filter.Tendsto.enorm.

theorem ContinuousAt.norm' {α : Type u_1} {E : Type u_4} [SeminormedGroup E] [TopologicalSpace α] {f : α → E} {a : α} (h : ContinuousAt f a) :

ContinuousAt (fun (x : α) => ‖f x‖) a

theorem ContinuousAt.norm {α : Type u_1} {E : Type u_4} [SeminormedAddGroup E] [TopologicalSpace α] {f : α → E} {a : α} (h : ContinuousAt f a) :

ContinuousAt (fun (x : α) => ‖f x‖) a

theorem ContinuousAt.nnnorm' {α : Type u_1} {E : Type u_4} [SeminormedGroup E] [TopologicalSpace α] {f : α → E} {a : α} (h : ContinuousAt f a) :

ContinuousAt (fun (x : α) => ‖f x‖₊) a

theorem ContinuousAt.nnnorm {α : Type u_1} {E : Type u_4} [SeminormedAddGroup E] [TopologicalSpace α] {f : α → E} {a : α} (h : ContinuousAt f a) :

ContinuousAt (fun (x : α) => ‖f x‖₊) a

theorem ContinuousWithinAt.norm' {α : Type u_1} {E : Type u_4} [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_1} {E : Type u_4} [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_1} {E : Type u_4} [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_1} {E : Type u_4} [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_1} {E : Type u_4} [SeminormedGroup E] [TopologicalSpace α] {f : α → E} {s : Set α} (h : ContinuousOn f s) :

ContinuousOn (fun (x : α) => ‖f x‖) s

theorem ContinuousOn.norm {α : Type u_1} {E : Type u_4} [SeminormedAddGroup E] [TopologicalSpace α] {f : α → E} {s : Set α} (h : ContinuousOn f s) :

ContinuousOn (fun (x : α) => ‖f x‖) s

theorem ContinuousOn.nnnorm' {α : Type u_1} {E : Type u_4} [SeminormedGroup E] [TopologicalSpace α] {f : α → E} {s : Set α} (h : ContinuousOn f s) :

ContinuousOn (fun (x : α) => ‖f x‖₊) s

theorem ContinuousOn.nnnorm {α : Type u_1} {E : Type u_4} [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_1} {E : Type u_4} [SeminormedGroup E] {l : Filter α} {f : α → E} (h : Filter.Tendsto (fun (y : α) => ‖f y‖) l Filter.atTop) (x : E) :

∀ᶠ (y : α) in l, f y ≠ x

If ‖y‖ → ∞, then we can assume y ≠ x for any fixed x.

theorem eventually_ne_of_tendsto_norm_atTop {α : Type u_1} {E : Type u_4} [SeminormedAddGroup E] {l : Filter α} {f : α → E} (h : Filter.Tendsto (fun (y : α) => ‖f y‖) l Filter.atTop) (x : E) :

∀ᶠ (y : α) in l, f y ≠ x

If ‖y‖→∞, then we can assume y≠x for any fixed x

theorem SeminormedCommGroup.mem_closure_iff {E : Type u_4} [SeminormedGroup E] {s : Set E} {a : E} :

a ∈ closure s ↔ ∀ (ε : ℝ), 0 < ε → ∃ b ∈ s, ‖a / b‖ < ε

theorem SeminormedAddCommGroup.mem_closure_iff {E : Type u_4} [SeminormedAddGroup E] {s : Set E} {a : E} :

a ∈ closure s ↔ ∀ (ε : ℝ), 0 < ε → ∃ b ∈ s, ‖a - b‖ < ε

theorem SeminormedGroup.tendstoUniformlyOn_one {ι : Type u_2} {κ : Type u_3} {G : Type u_6} [SeminormedGroup G] {f : ι → κ → G} {s : Set κ} {l : Filter ι} :

TendstoUniformlyOn f 1 l s ↔ ∀ ε > 0, ∀ᶠ (i : ι) in l, ∀ x ∈ s, ‖f i x‖ < ε

theorem SeminormedAddGroup.tendstoUniformlyOn_zero {ι : Type u_2} {κ : Type u_3} {G : Type u_6} [SeminormedAddGroup G] {f : ι → κ → G} {s : Set κ} {l : Filter ι} :

TendstoUniformlyOn f 0 l s ↔ ∀ ε > 0, ∀ᶠ (i : ι) in l, ∀ x ∈ s, ‖f i x‖ < ε

theorem SeminormedGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_one {ι : Type u_2} {κ : Type u_3} {G : Type u_6} [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_2} {κ : Type u_3} {G : Type u_6} [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_2} {κ : Type u_3} {G : Type u_6} [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_2} {κ : Type u_3} {G : Type u_6} [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_4} [SeminormedCommGroup E] {a : E} {s : Subgroup E} (hg : a ∈ closure ↑s) {b : ℕ → ℝ} (b_pos : ∀ (n : ℕ), 0 < b n) :

∃ (v : ℕ → E), Filter.Tendsto (fun (n : ℕ) => ∏ i ∈ Finset.range (n + 1), v i) Filter.atTop (nhds a) ∧ (∀ (n : ℕ), v n ∈ s) ∧ ‖v 0 / a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n

theorem controlled_sum_of_mem_closure {E : Type u_4} [SeminormedAddCommGroup E] {a : E} {s : AddSubgroup E} (hg : a ∈ closure ↑s) {b : ℕ → ℝ} (b_pos : ∀ (n : ℕ), 0 < b n) :

∃ (v : ℕ → E), Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range (n + 1), v i) Filter.atTop (nhds a) ∧ (∀ (n : ℕ), v n ∈ s) ∧ ‖v 0 - a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n

theorem controlled_prod_of_mem_closure_range {E : Type u_4} {F : Type u_5} [SeminormedCommGroup E] [SeminormedCommGroup F] {j : E →* F} {b : F} (hb : b ∈ closure ↑j.range) {f : ℕ → ℝ} (b_pos : ∀ (n : ℕ), 0 < f n) :

∃ (a : ℕ → E), Filter.Tendsto (fun (n : ℕ) => ∏ i ∈ Finset.range (n + 1), j (a i)) Filter.atTop (nhds b) ∧ ‖j (a 0) / b‖ < f 0 ∧ ∀ (n : ℕ), 0 < n → ‖j (a n)‖ < f n

theorem controlled_sum_of_mem_closure_range {E : Type u_4} {F : Type u_5} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] {j : E →+ F} {b : F} (hb : b ∈ closure ↑j.range) {f : ℕ → ℝ} (b_pos : ∀ (n : ℕ), 0 < f n) :

∃ (a : ℕ → E), Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range (n + 1), j (a i)) Filter.atTop (nhds b) ∧ ‖j (a 0) - b‖ < f 0 ∧ ∀ (n : ℕ), 0 < n → ‖j (a n)‖ < f n