Normed (semi)groups #
In this file we define four classes:
has_norm,has_nnnorm: auxiliary classes endowing a typeαwith a functionnorm : α → ℝ(notation:∥x∥) andnnnorm : α → ℝ≥0(notation:∥x∥₊), respectively;semi_normed_group: a seminormed group is an additive group with a norm and a pseudo metric space structures that agree with each other:∀ x y, dist x y = ∥x - y∥;normed_group: a normed group is an additive group with a norm and a metric space structures that agree with each other:∀ x y, dist x y = ∥x - y∥.
We also prove basic properties of (semi)normed groups and provide some instances.
Tags #
normed group
@[class]
- norm : E → ℝ
Auxiliary class, endowing a type E with a function norm : E → ℝ with notation ∥x∥. This
class is designed to be extended in more interesting classes specifying the properties of the norm.
Instances
- semi_normed_group.to_has_norm
- normed_group.to_has_norm
- semi_normed_ring.to_has_norm
- normed_ring.to_has_norm
- normed_field.to_has_norm
- normed_linear_ordered_group.to_has_norm
- normed_linear_ordered_field.to_has_norm
- continuous_linear_map.has_op_norm
- normed_group_hom.has_op_norm
- complex.has_norm
- continuous_multilinear_map.has_op_norm
- bounded_continuous_function.has_norm
- continuous_map.has_norm
- measure_theory.Lp.has_norm
- continuous_affine_map.has_norm
- lp.has_norm
- uniform_space.completion.has_norm
- norm_on_quotient
- padic.has_norm
- padic_int.has_norm
@[class]
- to_has_norm : has_norm E
- to_add_comm_group : add_comm_group E
- to_pseudo_metric_space : pseudo_metric_space E
- dist_eq : ∀ (x y : E), dist x y = ∥x - y∥
A seminormed group is an additive group endowed with a norm for which dist x y = ∥x - y∥
defines a pseudometric space structure.
Instances
- normed_group.to_semi_normed_group
- semi_normed_ring.to_semi_normed_group
- add_subgroup.semi_normed_group
- submodule.semi_normed_group
- prod.semi_normed_group
- pi.semi_normed_group
- restrict_scalars.semi_normed_group
- continuous_linear_map.to_semi_normed_group
- normed_group_hom.to_semi_normed_group
- normed_space.dual.semi_normed_group
- pi_Lp.semi_normed_group
- SemiNormedGroup.semi_normed_group
- SemiNormedGroup₁.semi_normed_group
- add_subgroup.semi_normed_group_quotient
@[class]
- to_has_norm : has_norm E
- to_add_comm_group : add_comm_group E
- to_metric_space : metric_space E
- dist_eq : ∀ (x y : E), dist x y = ∥x - y∥
A normed group is an additive group endowed with a norm for which dist x y = ∥x - y∥ defines
a metric space structure.
Instances
- normed_ring.to_normed_group
- normed_linear_ordered_group.to_normed_group
- inner_product_space.to_normed_group
- normed_lattice_add_comm_group.to_normed_group
- order_dual.normed_group
- punit.normed_group
- real.normed_group
- add_subgroup.normed_group
- submodule.normed_group
- prod.normed_group
- pi.normed_group
- restrict_scalars.normed_group
- continuous_linear_map.to_normed_group
- normed_group_hom.to_normed_group
- complex.normed_group
- continuous_multilinear_map.to_normed_group
- normed_space.dual.normed_group
- bounded_continuous_function.normed_group
- continuous_map.normed_group
- measure_theory.Lp.normed_group
- measure_theory.Lp.normed_group_L1
- measure_theory.Lp.normed_group_L2
- measure_theory.Lp.normed_group_Ltop
- continuous_affine_map.normed_group
- pi_Lp.normed_group
- lp.normed_group
- uniform_space.completion.normed_group
- add_subgroup.normed_group_quotient
- enorm.finite_subspace.normed_group
@[protected, instance]
A normed group is a seminormed group.
def
semi_normed_group.of_add_dist
{E : Type u_3}
[has_norm E]
[add_comm_group E]
[pseudo_metric_space E]
(H1 : ∀ (x : E), ∥x∥ = dist x 0)
(H2 : ∀ (x y z : E), dist x y ≤ dist (x + z) (y + z)) :
Construct a seminormed group from a translation invariant pseudodistance.
Equations
- semi_normed_group.of_add_dist H1 H2 = {to_has_norm := _inst_1, to_add_comm_group := _inst_2, to_pseudo_metric_space := _inst_3, dist_eq := _}
def
semi_normed_group.of_add_dist'
{E : Type u_3}
[has_norm E]
[add_comm_group E]
[pseudo_metric_space E]
(H1 : ∀ (x : E), ∥x∥ = dist x 0)
(H2 : ∀ (x y z : E), dist (x + z) (y + z) ≤ dist x y) :
Construct a seminormed group from a translation invariant pseudodistance
Equations
- semi_normed_group.of_add_dist' H1 H2 = {to_has_norm := _inst_1, to_add_comm_group := _inst_2, to_pseudo_metric_space := _inst_3, dist_eq := _}
A seminormed group can be built from a seminorm that satisfies algebraic properties. This is formalised in this structure.
def
semi_normed_group.of_core
(E : Type u_1)
[add_comm_group E]
[has_norm E]
(C : semi_normed_group.core E) :
Constructing a seminormed group from core properties of a seminorm, i.e., registering the
pseudodistance and the pseudometric space structure from the seminorm properties. Note that in most
cases this instance creates bad definitional equalities (e.g., it does not take into account
a possibly existing uniform_space instance on E).
Equations
- semi_normed_group.of_core E C = {to_has_norm := _inst_2, to_add_comm_group := _inst_1, to_pseudo_metric_space := {to_has_dist := {dist := λ (x y : E), ∥x - y∥}, dist_self := _, dist_comm := _, dist_triangle := _, edist := λ (x y : E), ↑⟨(λ (x y : E), ∥x - y∥) x y, _⟩, edist_dist := _, to_uniform_space := uniform_space_of_dist (λ (x y : E), ∥x - y∥) _ _ _, uniformity_dist := _}, dist_eq := _}
@[protected, instance]
Equations
- punit.normed_group = {to_has_norm := {norm := function.const punit 0}, to_add_comm_group := punit.add_comm_group, to_metric_space := punit.metric_space, dist_eq := punit.normed_group._proof_1}
@[protected, instance]
Equations
- real.normed_group = {to_has_norm := {norm := λ (x : ℝ), |x|}, to_add_comm_group := real.add_comm_group, to_metric_space := real.metric_space, dist_eq := real.normed_group._proof_1}
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
norm_sum_le
{ι : Type u_2}
{E : Type u_3}
[semi_normed_group E]
(s : finset ι)
(f : ι → E) :
theorem
dist_sum_sum_le_of_le
{ι : Type u_2}
{E : Type u_3}
[semi_normed_group E]
(s : finset ι)
{f g : ι → E}
{d : ι → ℝ}
(h : ∀ (b : ι), b ∈ s → dist (f b) (g b) ≤ d b) :
theorem
dist_sum_sum_le
{ι : Type u_2}
{E : Type u_3}
[semi_normed_group E]
(s : finset ι)
(f g : ι → E) :
theorem
ball_zero_eq
{E : Type u_3}
[semi_normed_group E]
(ε : ℝ) :
metric.ball 0 ε = {x : E | ∥x∥ < ε}
@[simp]
@[simp]
theorem
norm_le_of_mem_closed_ball
{E : Type u_3}
[semi_normed_group E]
{g h : E}
{r : ℝ}
(H : h ∈ metric.closed_ball g r) :
theorem
norm_lt_of_mem_ball
{E : Type u_3}
[semi_normed_group E]
{g h : E}
{r : ℝ}
(H : h ∈ metric.ball g r) :
@[simp]
theorem
preimage_add_ball
{E : Type u_3}
[semi_normed_group E]
(x y : E)
(r : ℝ) :
has_add.add y ⁻¹' metric.ball x r = metric.ball (x - y) r
@[simp]
theorem
preimage_add_closed_ball
{E : Type u_3}
[semi_normed_group E]
(x y : E)
(r : ℝ) :
has_add.add y ⁻¹' metric.closed_ball x r = metric.closed_ball (x - y) r
@[simp]
@[simp]
@[simp]
theorem
norm_eq_of_mem_sphere
{E : Type u_3}
[semi_normed_group E]
{r : ℝ}
(x : ↥(metric.sphere 0 r)) :
theorem
preimage_add_sphere
{E : Type u_3}
[semi_normed_group E]
(x y : E)
(r : ℝ) :
has_add.add y ⁻¹' metric.sphere x r = metric.sphere (x - y) r
theorem
ne_zero_of_mem_sphere
{E : Type u_3}
[semi_normed_group E]
{r : ℝ}
(hr : r ≠ 0)
(x : ↥(metric.sphere 0 r)) :
theorem
ne_zero_of_mem_unit_sphere
{E : Type u_3}
[semi_normed_group E]
(x : ↥(metric.sphere 0 1)) :
@[protected, instance]
def
metric.sphere.has_neg
{E : Type u_3}
[semi_normed_group E]
{r : ℝ} :
has_neg ↥(metric.sphere 0 r)
We equip the sphere, in a seminormed group, with a formal operation of negation, namely the antipodal map.
Equations
- metric.sphere.has_neg = {neg := λ (w : ↥(metric.sphere 0 r)), ⟨-↑w, _⟩}
@[simp]
@[protected]
Addition y ↦ y + x as an isometry.
Equations
- isometric.add_right x = {to_equiv := {to_fun := (equiv.add_right x).to_fun, inv_fun := (equiv.add_right x).inv_fun, left_inv := _, right_inv := _}, isometry_to_fun := _}
@[simp]
@[simp]
theorem
isometric.coe_add_right
{E : Type u_3}
[semi_normed_group E]
(x : E) :
⇑(isometric.add_right x) = λ (y : E), y + x
theorem
isometric.add_right_apply
{E : Type u_3}
[semi_normed_group E]
(x y : E) :
⇑(isometric.add_right x) y = y + x
@[simp]
theorem
isometric.add_right_symm
{E : Type u_3}
[semi_normed_group E]
(x : E) :
(isometric.add_right x).symm = isometric.add_right (-x)
@[protected]
Addition y ↦ x + y as an isometry.
Equations
- isometric.add_left x = {to_equiv := equiv.add_left x, isometry_to_fun := _}
@[simp]
@[simp]
theorem
isometric.coe_add_left
{E : Type u_3}
[semi_normed_group E]
(x : E) :
⇑(isometric.add_left x) = has_add.add x
@[simp]
theorem
isometric.add_left_symm
{E : Type u_3}
[semi_normed_group E]
(x : E) :
(isometric.add_left x).symm = isometric.add_left (-x)
@[protected]
Negation x ↦ -x as an isometry.
Equations
- isometric.neg E = {to_equiv := equiv.neg E (add_comm_group.to_add_group E), isometry_to_fun := _}
@[simp]
theorem
isometric.neg_symm
{E : Type u_3}
[semi_normed_group E] :
(isometric.neg E).symm = isometric.neg E
@[simp]
theorem
isometric.neg_to_equiv
{E : Type u_3}
[semi_normed_group E] :
(isometric.neg E).to_equiv = equiv.neg E
@[simp]
theorem
normed_group.tendsto_nhds_zero
{α : Type u_1}
{E : Type u_3}
[semi_normed_group E]
{f : α → E}
{l : filter α} :
theorem
normed_group.tendsto_nhds_nhds
{E : Type u_3}
{F : Type u_4}
[semi_normed_group E]
[semi_normed_group F]
{f : E → F}
{x : E}
{y : F} :
theorem
normed_group.cauchy_seq_iff
{α : Type u_1}
{E : Type u_3}
[semi_normed_group E]
[nonempty α]
[semilattice_sup α]
{u : α → E} :
theorem
add_monoid_hom.lipschitz_of_bound
{E : Type u_3}
{F : Type u_4}
[semi_normed_group E]
[semi_normed_group F]
(f : E →+ F)
(C : ℝ)
(h : ∀ (x : E), ∥⇑f x∥ ≤ C * ∥x∥) :
A homomorphism f of seminormed groups is Lipschitz, if there exists a constant C such that
for all x, one has ∥f x∥ ≤ C * ∥x∥. The analogous condition for a linear map of
(semi)normed spaces is in normed_space.operator_norm.
theorem
lipschitz_on_with_iff_norm_sub_le
{E : Type u_3}
{F : Type u_4}
[semi_normed_group E]
[semi_normed_group F]
{f : E → F}
{C : ℝ≥0}
{s : set E} :
theorem
lipschitz_on_with.norm_sub_le
{E : Type u_3}
{F : Type u_4}
[semi_normed_group E]
[semi_normed_group F]
{f : E → F}
{C : ℝ≥0}
{s : set E}
(h : lipschitz_on_with C f s)
{x y : E}
(x_in : x ∈ s)
(y_in : y ∈ s) :
theorem
lipschitz_on_with.norm_sub_le_of_le
{E : Type u_3}
{F : Type u_4}
[semi_normed_group E]
[semi_normed_group F]
{f : E → F}
{C : ℝ≥0}
{s : set E}
(h : lipschitz_on_with C f s)
{x y : E}
(x_in : x ∈ s)
(y_in : y ∈ s)
{d : ℝ}
(hd : ∥x - y∥ ≤ d) :
theorem
lipschitz_with_iff_norm_sub_le
{E : Type u_3}
{F : Type u_4}
[semi_normed_group E]
[semi_normed_group F]
{f : E → F}
{C : ℝ≥0} :
theorem
lipschitz_with.norm_sub_le
{E : Type u_3}
{F : Type u_4}
[semi_normed_group E]
[semi_normed_group F]
{f : E → F}
{C : ℝ≥0} :
Alias of lipschitz_with_iff_norm_sub_le.
theorem
lipschitz_with.norm_sub_le_of_le
{E : Type u_3}
{F : Type u_4}
[semi_normed_group E]
[semi_normed_group F]
{f : E → F}
{C : ℝ≥0}
(h : lipschitz_with C f)
{x y : E}
{d : ℝ}
(hd : ∥x - y∥ ≤ d) :
theorem
add_monoid_hom.continuous_of_bound
{E : Type u_3}
{F : Type u_4}
[semi_normed_group E]
[semi_normed_group F]
(f : E →+ F)
(C : ℝ)
(h : ∀ (x : E), ∥⇑f x∥ ≤ C * ∥x∥) :
A homomorphism f of seminormed groups is continuous, if there exists a constant C such that
for all x, one has ∥f x∥ ≤ C * ∥x∥.
The analogous condition for a linear map of normed spaces is in normed_space.operator_norm.
theorem
is_compact.exists_bound_of_continuous_on
{α : Type u_1}
{E : Type u_3}
[semi_normed_group E]
[topological_space α]
{s : set α}
(hs : is_compact s)
{f : α → E}
(hf : continuous_on f s) :
theorem
add_monoid_hom.isometry_iff_norm
{E : Type u_3}
{F : Type u_4}
[semi_normed_group E]
[semi_normed_group F]
(f : E →+ F) :
theorem
add_monoid_hom.isometry_of_norm
{E : Type u_3}
{F : Type u_4}
[semi_normed_group E]
[semi_normed_group F]
(f : E →+ F)
(hf : ∀ (x : E), ∥⇑f x∥ = ∥x∥) :
theorem
controlled_sum_of_mem_closure
{E : Type u_3}
[semi_normed_group E]
{s : add_subgroup E}
{g : E}
(hg : g ∈ closure ↑s)
{b : ℕ → ℝ}
(b_pos : ∀ (n : ℕ), 0 < b n) :
theorem
controlled_sum_of_mem_closure_range
{E : Type u_3}
{F : Type u_4}
[semi_normed_group E]
[semi_normed_group F]
{j : E →+ F}
{h : F}
(Hh : h ∈ closure ↑(j.range))
{b : ℕ → ℝ}
(b_pos : ∀ (n : ℕ), 0 < b n) :
@[class]
- nnnorm : E → ℝ≥0
Auxiliary class, endowing a type α with a function nnnorm : α → ℝ≥0 with notation ∥x∥₊.
Instances
@[protected, instance]
@[simp, norm_cast]
theorem
nnnorm_sum_le
{ι : Type u_2}
{E : Type u_3}
[semi_normed_group E]
(s : finset ι)
(f : ι → E) :
theorem
add_monoid_hom.lipschitz_of_bound_nnnorm
{E : Type u_3}
{F : Type u_4}
[semi_normed_group E]
[semi_normed_group F]
(f : E →+ F)
(C : ℝ≥0)
(h : ∀ (x : E), ∥⇑f x∥₊ ≤ C * ∥x∥₊) :
lipschitz_with C ⇑f
theorem
lipschitz_with.neg
{α : Type u_1}
{E : Type u_3}
[semi_normed_group E]
[pseudo_emetric_space α]
{K : ℝ≥0}
{f : α → E}
(hf : lipschitz_with K f) :
lipschitz_with K (λ (x : α), -f x)
theorem
lipschitz_with.add
{α : Type u_1}
{E : Type u_3}
[semi_normed_group E]
[pseudo_emetric_space α]
{Kf Kg : ℝ≥0}
{f g : α → E}
(hf : lipschitz_with Kf f)
(hg : lipschitz_with Kg g) :
lipschitz_with (Kf + Kg) (λ (x : α), f x + g x)
theorem
lipschitz_with.sub
{α : Type u_1}
{E : Type u_3}
[semi_normed_group E]
[pseudo_emetric_space α]
{Kf Kg : ℝ≥0}
{f g : α → E}
(hf : lipschitz_with Kf f)
(hg : lipschitz_with Kg g) :
lipschitz_with (Kf + Kg) (λ (x : α), f x - g x)
theorem
antilipschitz_with.add_lipschitz_with
{α : Type u_1}
{E : Type u_3}
[semi_normed_group E]
[pseudo_emetric_space α]
{Kf Kg : ℝ≥0}
{f g : α → E}
(hf : antilipschitz_with Kf f)
(hg : lipschitz_with Kg g)
(hK : Kg < Kf⁻¹) :
antilipschitz_with (Kf⁻¹ - Kg)⁻¹ (λ (x : α), f x + g x)
theorem
antilipschitz_with.add_sub_lipschitz_with
{α : Type u_1}
{E : Type u_3}
[semi_normed_group E]
[pseudo_emetric_space α]
{Kf Kg : ℝ≥0}
{f g : α → E}
(hf : antilipschitz_with Kf f)
(hg : lipschitz_with Kg (g - f))
(hK : Kg < Kf⁻¹) :
antilipschitz_with (Kf⁻¹ - Kg)⁻¹ g
def
semi_normed_group.induced
{F : Type u_4}
[semi_normed_group F]
{E : Type u_1}
[add_comm_group E]
(f : E →+ F) :
A group homomorphism from an add_comm_group to a semi_normed_group induces a
semi_normed_group structure on the domain.
See note [reducible non-instances]
Equations
- semi_normed_group.induced f = {to_has_norm := {norm := λ (x : E), ∥⇑f x∥}, to_add_comm_group := _inst_3, to_pseudo_metric_space := {to_has_dist := pseudo_metric_space.to_has_dist (pseudo_metric_space.induced ⇑f semi_normed_group.to_pseudo_metric_space), dist_self := _, dist_comm := _, dist_triangle := _, edist := pseudo_metric_space.edist (pseudo_metric_space.induced ⇑f semi_normed_group.to_pseudo_metric_space), edist_dist := _, to_uniform_space := pseudo_metric_space.to_uniform_space (pseudo_metric_space.induced ⇑f semi_normed_group.to_pseudo_metric_space), uniformity_dist := _}, dist_eq := _}
@[protected, instance]
A subgroup of a seminormed group is also a seminormed group, with the restriction of the norm.
Equations
@[simp]
If x is an element of a subgroup s of a seminormed group E, its norm in s is equal to
its norm in E.
@[norm_cast]
If x is an element of a subgroup s of a seminormed group E, its norm in s is equal to
its norm in E.
This is a reversed version of the simp lemma add_subgroup.coe_norm for use by norm_cast.
@[protected, instance]
def
submodule.semi_normed_group
{𝕜 : Type u_1}
{_x : ring 𝕜}
{E : Type u_2}
[semi_normed_group E]
{_x_1 : module 𝕜 E}
(s : submodule 𝕜 E) :
A submodule of a seminormed group is also a seminormed group, with the restriction of the norm.
See note [implicit instance arguments].
Equations
- s.semi_normed_group = {to_has_norm := {norm := λ (x : ↥s), ∥↑x∥}, to_add_comm_group := s.add_comm_group, to_pseudo_metric_space := subtype.psudo_metric_space semi_normed_group.to_pseudo_metric_space, dist_eq := _}
@[simp]
theorem
submodule.coe_norm
{𝕜 : Type u_1}
{_x : ring 𝕜}
{E : Type u_2}
[semi_normed_group E]
{_x_1 : module 𝕜 E}
{s : submodule 𝕜 E}
(x : ↥s) :
If x is an element of a submodule s of a normed group E, its norm in s is equal to its
norm in E.
@[norm_cast]
theorem
submodule.norm_coe
{𝕜 : Type u_1}
{_x : ring 𝕜}
{E : Type u_2}
[semi_normed_group E]
{_x_1 : module 𝕜 E}
{s : submodule 𝕜 E}
(x : ↥s) :
If x is an element of a submodule s of a normed group E, its norm in E is equal to its
norm in s.
This is a reversed version of the simp lemma submodule.coe_norm for use by norm_cast.
@[protected, instance]
noncomputable
def
prod.semi_normed_group
{E : Type u_3}
{F : Type u_4}
[semi_normed_group E]
[semi_normed_group F] :
semi_normed_group (E × F)
seminormed group instance on the product of two seminormed groups, using the sup norm.
Equations
theorem
prod.norm_def
{E : Type u_3}
{F : Type u_4}
[semi_normed_group E]
[semi_normed_group F]
(x : E × F) :
theorem
prod.nnnorm_def
{E : Type u_3}
{F : Type u_4}
[semi_normed_group E]
[semi_normed_group F]
(x : E × F) :
theorem
norm_fst_le
{E : Type u_3}
{F : Type u_4}
[semi_normed_group E]
[semi_normed_group F]
(x : E × F) :
theorem
norm_snd_le
{E : Type u_3}
{F : Type u_4}
[semi_normed_group E]
[semi_normed_group F]
(x : E × F) :
@[protected, instance]
noncomputable
def
pi.semi_normed_group
{ι : Type u_2}
{π : ι → Type u_1}
[fintype ι]
[Π (i : ι), semi_normed_group (π i)] :
semi_normed_group (Π (i : ι), π i)
seminormed group instance on the product of finitely many seminormed groups, using the sup norm.
Equations
- pi.semi_normed_group = {to_has_norm := {norm := λ (f : Π (i : ι), π i), ↑(finset.univ.sup (λ (b : ι), ∥f b∥₊))}, to_add_comm_group := pi.add_comm_group (λ (i : ι), semi_normed_group.to_add_comm_group), to_pseudo_metric_space := pseudo_metric_space_pi (λ (b : ι), semi_normed_group.to_pseudo_metric_space), dist_eq := _}
theorem
norm_le_pi_norm
{ι : Type u_2}
{π : ι → Type u_1}
[fintype ι]
[Π (i : ι), semi_normed_group (π i)]
(x : Π (i : ι), π i)
(i : ι) :
@[simp]
theorem
pi_norm_const
{ι : Type u_2}
{E : Type u_3}
[semi_normed_group E]
[nonempty ι]
[fintype ι]
(a : E) :
@[simp]
theorem
pi_nnnorm_const
{ι : Type u_2}
{E : Type u_3}
[semi_normed_group E]
[nonempty ι]
[fintype ι]
(a : E) :
theorem
tendsto_iff_norm_tendsto_zero
{α : Type u_1}
{E : Type u_3}
[semi_normed_group E]
{f : α → E}
{a : filter α}
{b : E} :
filter.tendsto f a (𝓝 b) ↔ filter.tendsto (λ (e : α), ∥f e - b∥) a (𝓝 0)
theorem
is_bounded_under_of_tendsto
{α : Type u_1}
{E : Type u_3}
[semi_normed_group E]
{l : filter α}
{f : α → E}
{c : E}
(h : filter.tendsto f l (𝓝 c)) :
filter.is_bounded_under has_le.le l (λ (x : α), ∥f x∥)
theorem
tendsto_zero_iff_norm_tendsto_zero
{α : Type u_1}
{E : Type u_3}
[semi_normed_group E]
{f : α → E}
{a : filter α} :
filter.tendsto f a (𝓝 0) ↔ filter.tendsto (λ (e : α), ∥f e∥) a (𝓝 0)
theorem
squeeze_zero_norm'
{α : Type u_1}
{E : Type u_3}
[semi_normed_group E]
{f : α → E}
{g : α → ℝ}
{t₀ : filter α}
(h : ∀ᶠ (n : α) in t₀, ∥f n∥ ≤ g n)
(h' : filter.tendsto g t₀ (𝓝 0)) :
filter.tendsto f t₀ (𝓝 0)
Special case of the sandwich theorem: if the norm of f is eventually bounded by a real
function g 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.metric_space.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_3}
[semi_normed_group E]
{f : α → E}
{g : α → ℝ}
{t₀ : filter α}
(h : ∀ (n : α), ∥f n∥ ≤ g n)
(h' : filter.tendsto g t₀ (𝓝 0)) :
filter.tendsto f t₀ (𝓝 0)
Special case of the sandwich theorem: if the norm of f is bounded by a real function g which
tends to 0, then f tends to 0.
theorem
tendsto_norm_zero
{E : Type u_3}
[semi_normed_group E] :
filter.tendsto (λ (g : E), ∥g∥) (𝓝 0) (𝓝 0)
@[continuity]
@[continuity]
theorem
uniform_continuous_nnnorm
{E : Type u_3}
[semi_normed_group E] :
uniform_continuous (λ (a : E), ∥a∥₊)
theorem
filter.tendsto.norm
{α : Type u_1}
{E : Type u_3}
[semi_normed_group E]
{l : filter α}
{f : α → E}
{a : E}
(h : filter.tendsto f l (𝓝 a)) :
theorem
filter.tendsto.nnnorm
{α : Type u_1}
{E : Type u_3}
[semi_normed_group E]
{l : filter α}
{f : α → E}
{a : E}
(h : filter.tendsto f l (𝓝 a)) :
theorem
continuous.norm
{α : Type u_1}
{E : Type u_3}
[semi_normed_group E]
[topological_space α]
{f : α → E}
(h : continuous f) :
continuous (λ (x : α), ∥f x∥)
theorem
continuous.nnnorm
{α : Type u_1}
{E : Type u_3}
[semi_normed_group E]
[topological_space α]
{f : α → E}
(h : continuous f) :
continuous (λ (x : α), ∥f x∥₊)
theorem
continuous_at.norm
{α : Type u_1}
{E : Type u_3}
[semi_normed_group E]
[topological_space α]
{f : α → E}
{a : α}
(h : continuous_at f a) :
continuous_at (λ (x : α), ∥f x∥) a
theorem
continuous_at.nnnorm
{α : Type u_1}
{E : Type u_3}
[semi_normed_group E]
[topological_space α]
{f : α → E}
{a : α}
(h : continuous_at f a) :
continuous_at (λ (x : α), ∥f x∥₊) a
theorem
continuous_within_at.norm
{α : Type u_1}
{E : Type u_3}
[semi_normed_group E]
[topological_space α]
{f : α → E}
{s : set α}
{a : α}
(h : continuous_within_at f s a) :
continuous_within_at (λ (x : α), ∥f x∥) s a
theorem
continuous_within_at.nnnorm
{α : Type u_1}
{E : Type u_3}
[semi_normed_group E]
[topological_space α]
{f : α → E}
{s : set α}
{a : α}
(h : continuous_within_at f s a) :
continuous_within_at (λ (x : α), ∥f x∥₊) s a
theorem
continuous_on.norm
{α : Type u_1}
{E : Type u_3}
[semi_normed_group E]
[topological_space α]
{f : α → E}
{s : set α}
(h : continuous_on f s) :
continuous_on (λ (x : α), ∥f x∥) s
theorem
continuous_on.nnnorm
{α : Type u_1}
{E : Type u_3}
[semi_normed_group E]
[topological_space α]
{f : α → E}
{s : set α}
(h : continuous_on f s) :
continuous_on (λ (x : α), ∥f x∥₊) s
theorem
eventually_ne_of_tendsto_norm_at_top
{α : Type u_1}
{E : Type u_3}
[semi_normed_group E]
{l : filter α}
{f : α → E}
(h : filter.tendsto (λ (y : α), ∥f y∥) l filter.at_top)
(x : E) :
∀ᶠ (y : α) in l, f y ≠ x
If ∥y∥→∞, then we can assume y≠x for any fixed x.
@[protected, instance]
@[protected, instance]
A seminormed group is a uniform additive group, i.e., addition and subtraction are uniformly continuous.
@[protected, instance]
theorem
cauchy_seq_sum_of_eventually_eq
{E : Type u_3}
[semi_normed_group E]
{u v : ℕ → E}
{N : ℕ}
(huv : ∀ (n : ℕ), n ≥ N → u n = v n)
(hv : cauchy_seq (λ (n : ℕ), ∑ (k : ℕ) in finset.range (n + 1), v k)) :
cauchy_seq (λ (n : ℕ), ∑ (k : ℕ) in finset.range (n + 1), u k)
def
normed_group.of_add_dist
{E : Type u_3}
[has_norm E]
[add_comm_group E]
[metric_space E]
(H1 : ∀ (x : E), ∥x∥ = dist x 0)
(H2 : ∀ (x y z : E), dist x y ≤ dist (x + z) (y + z)) :
Construct a normed group from a translation invariant distance
Equations
- normed_group.of_add_dist H1 H2 = {to_has_norm := _inst_1, to_add_comm_group := _inst_2, to_metric_space := _inst_3, dist_eq := _}
theorem
normed_group.core.to_semi_normed_group.core
{E : Type u_1}
[add_comm_group E]
[has_norm E]
(C : normed_group.core E) :
The semi_normed_group.core induced by a normed_group.core.
Constructing a normed group from core properties of a norm, i.e., registering the distance and the metric space structure from the norm properties.
Equations
- normed_group.of_core E C = {to_has_norm := semi_normed_group.to_has_norm (semi_normed_group.of_core E _), to_add_comm_group := semi_normed_group.to_add_comm_group (semi_normed_group.of_core E _), to_metric_space := {to_pseudo_metric_space := semi_normed_group.to_pseudo_metric_space (semi_normed_group.of_core E _), eq_of_dist_eq_zero := _}, dist_eq := _}
def
normed_group.induced
{F : Type u_4}
[normed_group F]
{E : Type u_1}
[add_comm_group E]
(f : E →+ F)
(h : function.injective ⇑f) :
An injective group homomorphism from an add_comm_group to a normed_group induces a
normed_group structure on the domain.
See note [reducible non-instances].
Equations
- normed_group.induced f h = {to_has_norm := semi_normed_group.to_has_norm (semi_normed_group.induced f), to_add_comm_group := semi_normed_group.to_add_comm_group (semi_normed_group.induced f), to_metric_space := {to_pseudo_metric_space := semi_normed_group.to_pseudo_metric_space (semi_normed_group.induced f), eq_of_dist_eq_zero := _}, dist_eq := _}
@[protected, instance]
A subgroup of a normed group is also a normed group, with the restriction of the norm.
Equations
@[protected, instance]
def
submodule.normed_group
{𝕜 : Type u_1}
{_x : ring 𝕜}
{E : Type u_2}
[normed_group E]
{_x_1 : module 𝕜 E}
(s : submodule 𝕜 E) :
A submodule of a normed group is also a normed group, with the restriction of the norm.
@[protected, instance]
noncomputable
def
prod.normed_group
{E : Type u_3}
{F : Type u_4}
[normed_group E]
[normed_group F] :
normed_group (E × F)
normed group instance on the product of two normed groups, using the sup norm.
@[protected, instance]
noncomputable
def
pi.normed_group
{ι : Type u_2}
{π : ι → Type u_1}
[fintype ι]
[Π (i : ι), normed_group (π i)] :
normed_group (Π (i : ι), π i)
normed group instance on the product of finitely many normed groups, using the sup norm.