Normed spaces #
Since a lot of elementary properties don't require ∥x∥ = 0 → x = 0 we start setting up the
theory of semi_normed_group and we specialize to normed_group at the end.
@[class]
- norm : α → ℝ
Auxiliary class, endowing a type α with a function norm : α → ℝ. 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
- uniform_space.completion.has_norm
- continuous_linear_map.has_op_norm
- continuous_multilinear_map.has_op_norm
- complex.has_norm
- normed_group_hom.has_op_norm
- bounded_continuous_function.has_norm
- continuous_map.has_norm
- measure_theory.Lp.has_norm
- norm_on_quotient
- padic.has_norm
- padic_int.has_norm
@[class]
- to_has_norm : has_norm α
- to_add_comm_group : add_comm_group α
- to_pseudo_metric_space : pseudo_metric_space α
- dist_eq : ∀ (x y : α), 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
- pi_Lp.semi_normed_group
- SemiNormedGroup.semi_normed_group
- SemiNormedGroup₁.semi_normed_group
- normed_space.dual.semi_normed_group
- add_subgroup.semi_normed_group_quotient
@[class]
- to_has_norm : has_norm α
- to_add_comm_group : add_comm_group α
- to_metric_space : metric_space α
- dist_eq : ∀ (x y : α), 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
- punit.normed_group
- real.normed_group
- add_subgroup.normed_group
- submodule.normed_group
- prod.normed_group
- pi.normed_group
- restrict_scalars.normed_group
- uniform_space.completion.normed_group
- continuous_linear_map.to_normed_group
- continuous_multilinear_map.to_normed_group
- complex.normed_group
- normed_group_hom.to_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
- pi_Lp.normed_group
- normed_space.dual.normed_group
- enorm.finite_subspace.normed_group
- add_subgroup.normed_group_quotient
@[instance]
A normed group is a seminormed group.
def
semi_normed_group.of_add_dist
{α : Type u_1}
[has_norm α]
[add_comm_group α]
[pseudo_metric_space α]
(H1 : ∀ (x : α), ∥x∥ = dist x 0)
(H2 : ∀ (x y z : α), 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'
{α : Type u_1}
[has_norm α]
[add_comm_group α]
[pseudo_metric_space α]
(H1 : ∀ (x : α), ∥x∥ = dist x 0)
(H2 : ∀ (x y z : α), 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
(α : Type u_1)
[add_comm_group α]
[has_norm α]
(C : semi_normed_group.core α) :
Constructing a seminormed group from core properties of a seminorm, i.e., registering the pseudodistance and the pseudometric space structure from the seminorm properties.
Equations
- semi_normed_group.of_core α C = {to_has_norm := _inst_2, to_add_comm_group := _inst_1, to_pseudo_metric_space := {to_has_dist := {dist := λ (x y : α), ∥x - y∥}, dist_self := _, dist_comm := _, dist_triangle := _, edist := λ (x y : α), ennreal.of_real ((λ (x y : α), ∥x - y∥) x y), edist_dist := _, to_uniform_space := uniform_space_of_dist (λ (x y : α), ∥x - y∥) _ _ _, uniformity_dist := _}, dist_eq := _}
@[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}
@[instance]
Equations
- real.normed_group = {to_has_norm := {norm := λ (x : ℝ), abs 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_1}
[semi_normed_group α]
{β : Type u_2}
(s : finset β)
(f : β → α) :
theorem
ball_0_eq
{α : Type u_1}
[semi_normed_group α]
(ε : ℝ) :
metric.ball 0 ε = {x : α | ∥x∥ < ε}
@[simp]
theorem
norm_le_of_mem_closed_ball
{α : Type u_1}
[semi_normed_group α]
{g h : α}
{r : ℝ}
(H : h ∈ metric.closed_ball g r) :
theorem
norm_lt_of_mem_ball
{α : Type u_1}
[semi_normed_group α]
{g h : α}
{r : ℝ}
(H : h ∈ metric.ball g r) :
@[simp]
@[simp]
@[simp]
theorem
norm_eq_of_mem_sphere
{α : Type u_1}
[semi_normed_group α]
{r : ℝ}
(x : ↥(metric.sphere 0 r)) :
theorem
nonzero_of_mem_sphere
{α : Type u_1}
[semi_normed_group α]
{r : ℝ}
(hr : 0 < r)
(x : ↥(metric.sphere 0 r)) :
theorem
nonzero_of_mem_unit_sphere
{α : Type u_1}
[semi_normed_group α]
(x : ↥(metric.sphere 0 1)) :
@[instance]
def
metric.sphere.has_neg
{α : Type u_1}
[semi_normed_group α]
{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]
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
{α : Type u_1}
[semi_normed_group α]
(x : α) :
⇑(isometric.add_right x) = λ (y : α), y + x
theorem
isometric.add_right_apply
{α : Type u_1}
[semi_normed_group α]
(x y : α) :
⇑(isometric.add_right x) y = y + x
@[simp]
theorem
isometric.add_right_symm
{α : Type u_1}
[semi_normed_group α]
(x : α) :
(isometric.add_right x).symm = isometric.add_right (-x)
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
{α : Type u_1}
[semi_normed_group α]
(x : α) :
⇑(isometric.add_left x) = has_add.add x
@[simp]
theorem
isometric.add_left_symm
{α : Type u_1}
[semi_normed_group α]
(x : α) :
(isometric.add_left x).symm = isometric.add_left (-x)
Negation x ↦ -x as an isometry.
Equations
- isometric.neg α = {to_equiv := equiv.neg α (add_comm_group.to_add_group α), isometry_to_fun := _}
@[simp]
theorem
isometric.neg_symm
{α : Type u_1}
[semi_normed_group α] :
(isometric.neg α).symm = isometric.neg α
@[simp]
theorem
isometric.neg_to_equiv
{α : Type u_1}
[semi_normed_group α] :
(isometric.neg α).to_equiv = equiv.neg α
@[simp]
theorem
normed_group.tendsto_nhds_zero
{α : Type u_1}
{γ : Type u_3}
[semi_normed_group α]
{f : γ → α}
{l : filter γ} :
theorem
normed_group.tendsto_nhds_nhds
{α : Type u_1}
{β : Type u_2}
[semi_normed_group α]
[semi_normed_group β]
{f : α → β}
{x : α}
{y : β} :
theorem
cauchy_seq.add
{α : Type u_1}
[semi_normed_group α]
{u v : ℕ → α}
(hu : cauchy_seq u)
(hv : cauchy_seq v) :
cauchy_seq (u + v)
theorem
cauchy_seq_sum_of_eventually_eq
{α : Type u_1}
[semi_normed_group α]
{u v : ℕ → α}
{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)
theorem
add_monoid_hom.lipschitz_of_bound
{α : Type u_1}
{β : Type u_2}
[semi_normed_group α]
[semi_normed_group β]
(f : α →+ β)
(C : ℝ)
(h : ∀ (x : α), ∥⇑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
{α : Type u_1}
{β : Type u_2}
[semi_normed_group α]
[semi_normed_group β]
{f : α → β}
{C : ℝ≥0}
{s : set α} :
theorem
lipschitz_on_with.norm_sub_le
{α : Type u_1}
{β : Type u_2}
[semi_normed_group α]
[semi_normed_group β]
{f : α → β}
{C : ℝ≥0}
{s : set α}
(h : lipschitz_on_with C f s)
{x y : α}
(x_in : x ∈ s)
(y_in : y ∈ s) :
theorem
lipschitz_with_iff_norm_sub_le
{α : Type u_1}
{β : Type u_2}
[semi_normed_group α]
[semi_normed_group β]
{f : α → β}
{C : ℝ≥0} :
theorem
add_monoid_hom.continuous_of_bound
{α : Type u_1}
{β : Type u_2}
[semi_normed_group α]
[semi_normed_group β]
(f : α →+ β)
(C : ℝ)
(h : ∀ (x : α), ∥⇑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}
[semi_normed_group α]
{γ : Type u_2}
[topological_space γ]
{s : set γ}
(hs : is_compact s)
{f : γ → α}
(hf : continuous_on f s) :
theorem
add_monoid_hom.isometry_iff_norm
{α : Type u_1}
{β : Type u_2}
[semi_normed_group α]
[semi_normed_group β]
(f : α →+ β) :
theorem
add_monoid_hom.isometry_of_norm
{α : Type u_1}
{β : Type u_2}
[semi_normed_group α]
[semi_normed_group β]
(f : α →+ β)
(hf : ∀ (x : α), ∥⇑f x∥ = ∥x∥) :
theorem
controlled_sum_of_mem_closure
{α : Type u_1}
[semi_normed_group α]
{s : add_subgroup α}
{g : α}
(hg : g ∈ closure ↑s)
{b : ℕ → ℝ}
(b_pos : ∀ (n : ℕ), 0 < b n) :
theorem
controlled_sum_of_mem_closure_range
{α : Type u_1}
{β : Type u_2}
[semi_normed_group α]
[semi_normed_group β]
{j : α →+ β}
{h : β}
(Hh : h ∈ closure ↑(j.range))
{b : ℕ → ℝ}
(b_pos : ∀ (n : ℕ), 0 < b n) :
@[class]
- nnnorm : α → ℝ≥0
Auxiliary class, endowing a type α with a function nnnorm : α → ℝ≥0.
Instances
@[instance]
theorem
nnnorm_sum_le
{α : Type u_1}
[semi_normed_group α]
{β : Type u_2}
(s : finset β)
(f : β → α) :
theorem
add_monoid_hom.lipschitz_of_bound_nnnorm
{α : Type u_1}
{β : Type u_2}
[semi_normed_group α]
[semi_normed_group β]
(f : α →+ β)
(C : ℝ≥0)
(h : ∀ (x : α), ∥⇑f x∥₊ ≤ C * ∥x∥₊) :
lipschitz_with C ⇑f
theorem
lipschitz_with.neg
{β : Type u_2}
[semi_normed_group β]
{α : Type u_1}
[pseudo_emetric_space α]
{K : ℝ≥0}
{f : α → β}
(hf : lipschitz_with K f) :
lipschitz_with K (λ (x : α), -f x)
theorem
lipschitz_with.add
{β : Type u_2}
[semi_normed_group β]
{α : Type u_1}
[pseudo_emetric_space α]
{Kf : ℝ≥0}
{f : α → β}
(hf : lipschitz_with Kf f)
{Kg : ℝ≥0}
{g : α → β}
(hg : lipschitz_with Kg g) :
lipschitz_with (Kf + Kg) (λ (x : α), f x + g x)
theorem
lipschitz_with.sub
{β : Type u_2}
[semi_normed_group β]
{α : Type u_1}
[pseudo_emetric_space α]
{Kf : ℝ≥0}
{f : α → β}
(hf : lipschitz_with Kf f)
{Kg : ℝ≥0}
{g : α → β}
(hg : lipschitz_with Kg g) :
lipschitz_with (Kf + Kg) (λ (x : α), f x - g x)
theorem
antilipschitz_with.add_lipschitz_with
{β : Type u_2}
[semi_normed_group β]
{α : Type u_1}
[pseudo_metric_space α]
{Kf : ℝ≥0}
{f : α → β}
(hf : antilipschitz_with Kf f)
{Kg : ℝ≥0}
{g : α → β}
(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_2}
[semi_normed_group β]
{α : Type u_1}
[pseudo_metric_space α]
{Kf : ℝ≥0}
{f : α → β}
(hf : antilipschitz_with Kf f)
{Kg : ℝ≥0}
{g : α → β}
(hg : lipschitz_with Kg (g - f))
(hK : Kg < Kf⁻¹) :
antilipschitz_with (Kf⁻¹ - Kg)⁻¹ g
@[instance]
A subgroup of a seminormed group is also a seminormed group, with the restriction of the norm.
Equations
- s.semi_normed_group = {to_has_norm := {norm := λ (x : ↥s), ∥↑x∥}, to_add_comm_group := s.to_add_comm_group, to_pseudo_metric_space := subtype.psudo_metric_space semi_normed_group.to_pseudo_metric_space, dist_eq := _}
@[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.
@[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.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.
@[instance]
def
prod.semi_normed_group
{α : Type u_1}
{β : Type u_2}
[semi_normed_group α]
[semi_normed_group β] :
semi_normed_group (α × β)
seminormed group instance on the product of two seminormed groups, using the sup norm.
Equations
theorem
prod.semi_norm_def
{α : Type u_1}
{β : Type u_2}
[semi_normed_group α]
[semi_normed_group β]
(x : α × β) :
theorem
prod.nnsemi_norm_def
{α : Type u_1}
{β : Type u_2}
[semi_normed_group α]
[semi_normed_group β]
(x : α × β) :
theorem
semi_norm_fst_le
{α : Type u_1}
{β : Type u_2}
[semi_normed_group α]
[semi_normed_group β]
(x : α × β) :
theorem
semi_norm_snd_le
{α : Type u_1}
{β : Type u_2}
[semi_normed_group α]
[semi_normed_group β]
(x : α × β) :
@[instance]
def
pi.semi_normed_group
{ι : Type u_4}
{π : ι → 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
semi_norm_le_pi_norm
{ι : Type u_4}
{π : ι → Type u_1}
[fintype ι]
[Π (i : ι), semi_normed_group («π» i)]
(x : Π (i : ι), «π» i)
(i : ι) :
@[simp]
theorem
pi_semi_norm_const
{α : Type u_1}
{ι : Type u_4}
[semi_normed_group α]
[nonempty ι]
[fintype ι]
(a : α) :
@[simp]
theorem
pi_nnsemi_norm_const
{α : Type u_1}
{ι : Type u_4}
[semi_normed_group α]
[nonempty ι]
[fintype ι]
(a : α) :
theorem
tendsto_iff_norm_tendsto_zero
{β : Type u_2}
{ι : Type u_4}
[semi_normed_group β]
{f : ι → β}
{a : filter ι}
{b : β} :
filter.tendsto f a (𝓝 b) ↔ filter.tendsto (λ (e : ι), ∥f e - b∥) a (𝓝 0)
theorem
is_bounded_under_of_tendsto
{α : Type u_1}
{ι : Type u_4}
[semi_normed_group α]
{l : filter ι}
{f : ι → α}
{c : α}
(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_2}
{γ : Type u_3}
[semi_normed_group β]
{f : γ → β}
{a : filter γ} :
filter.tendsto f a (𝓝 0) ↔ filter.tendsto (λ (e : γ), ∥f e∥) a (𝓝 0)
theorem
squeeze_zero_norm'
{α : Type u_1}
{γ : Type u_3}
[semi_normed_group α]
{f : γ → α}
{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.ordered, the ' version is
phrased using "eventually" and the non-' version is phrased absolutely.
theorem
squeeze_zero_norm
{α : Type u_1}
{γ : Type u_3}
[semi_normed_group α]
{f : γ → α}
{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
{α : Type u_1}
[semi_normed_group α] :
filter.tendsto (λ (g : α), ∥g∥) (𝓝 0) (𝓝 0)
theorem
uniform_continuous_nnnorm
{α : Type u_1}
[semi_normed_group α] :
uniform_continuous (λ (a : α), ∥a∥₊)
theorem
filter.tendsto.norm
{α : Type u_1}
{γ : Type u_3}
[semi_normed_group α]
{l : filter γ}
{f : γ → α}
{a : α}
(h : filter.tendsto f l (𝓝 a)) :
theorem
filter.tendsto.nnnorm
{α : Type u_1}
{γ : Type u_3}
[semi_normed_group α]
{l : filter γ}
{f : γ → α}
{a : α}
(h : filter.tendsto f l (𝓝 a)) :
theorem
continuous.norm
{α : Type u_1}
{γ : Type u_3}
[semi_normed_group α]
[topological_space γ]
{f : γ → α}
(h : continuous f) :
continuous (λ (x : γ), ∥f x∥)
theorem
continuous.nnnorm
{α : Type u_1}
{γ : Type u_3}
[semi_normed_group α]
[topological_space γ]
{f : γ → α}
(h : continuous f) :
continuous (λ (x : γ), ∥f x∥₊)
theorem
continuous_at.norm
{α : Type u_1}
{γ : Type u_3}
[semi_normed_group α]
[topological_space γ]
{f : γ → α}
{a : γ}
(h : continuous_at f a) :
continuous_at (λ (x : γ), ∥f x∥) a
theorem
continuous_at.nnnorm
{α : Type u_1}
{γ : Type u_3}
[semi_normed_group α]
[topological_space γ]
{f : γ → α}
{a : γ}
(h : continuous_at f a) :
continuous_at (λ (x : γ), ∥f x∥₊) a
theorem
continuous_within_at.norm
{α : Type u_1}
{γ : Type u_3}
[semi_normed_group α]
[topological_space γ]
{f : γ → α}
{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}
{γ : Type u_3}
[semi_normed_group α]
[topological_space γ]
{f : γ → α}
{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}
{γ : Type u_3}
[semi_normed_group α]
[topological_space γ]
{f : γ → α}
{s : set γ}
(h : continuous_on f s) :
continuous_on (λ (x : γ), ∥f x∥) s
theorem
continuous_on.nnnorm
{α : Type u_1}
{γ : Type u_3}
[semi_normed_group α]
[topological_space γ]
{f : γ → α}
{s : set γ}
(h : continuous_on f s) :
continuous_on (λ (x : γ), ∥f x∥₊) s
theorem
eventually_ne_of_tendsto_norm_at_top
{α : Type u_1}
{γ : Type u_3}
[semi_normed_group α]
{l : filter γ}
{f : γ → α}
(h : filter.tendsto (λ (y : γ), ∥f y∥) l filter.at_top)
(x : α) :
∀ᶠ (y : γ) in l, f y ≠ x
If ∥y∥→∞, then we can assume y≠x for any fixed x.
@[instance]
A seminormed group is a uniform additive group, i.e., addition and subtraction are uniformly continuous.
@[instance]
@[instance]
def
normed_group.of_add_dist
{α : Type u_1}
[has_norm α]
[add_comm_group α]
[metric_space α]
(H1 : ∀ (x : α), ∥x∥ = dist x 0)
(H2 : ∀ (x y z : α), 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
{α : Type u_1}
[add_comm_group α]
[has_norm α]
(C : normed_group.core α) :
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 α C = {to_has_norm := semi_normed_group.to_has_norm (semi_normed_group.of_core α _), to_add_comm_group := semi_normed_group.to_add_comm_group (semi_normed_group.of_core α _), to_metric_space := {to_pseudo_metric_space := semi_normed_group.to_pseudo_metric_space (semi_normed_group.of_core α _), eq_of_dist_eq_zero := _}, dist_eq := _}
@[instance]
A subgroup of a normed group is also a normed group, with the restriction of the norm.
@[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.
@[instance]
def
prod.normed_group
{α : Type u_1}
{β : Type u_2}
[normed_group α]
[normed_group β] :
normed_group (α × β)
normed group instance on the product of two normed groups, using the sup norm.
theorem
prod.nnnorm_def
{α : Type u_1}
{β : Type u_2}
[normed_group α]
[normed_group β]
(x : α × β) :
@[instance]
def
pi.normed_group
{ι : Type u_4}
{π : ι → 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.
theorem
norm_le_pi_norm
{ι : Type u_4}
{π : ι → Type u_1}
[fintype ι]
[Π (i : ι), normed_group («π» i)]
(x : Π (i : ι), «π» i)
(i : ι) :
@[simp]
theorem
pi_norm_const
{α : Type u_1}
{ι : Type u_4}
[normed_group α]
[nonempty ι]
[fintype ι]
(a : α) :
@[simp]
theorem
pi_nnnorm_const
{α : Type u_1}
{ι : Type u_4}
[normed_group α]
[nonempty ι]
[fintype ι]
(a : α) :
@[instance]
A normed ring is a seminormed ring.
Equations
@[class]
- to_semi_normed_ring : semi_normed_ring α
- mul_comm : ∀ (x y : α), x * y = y * x
A seminormed commutative ring is a commutative ring endowed with a seminorm which satisfies
the inequality ∥x y∥ ≤ ∥x∥ ∥y∥.
@[class]
- to_normed_ring : normed_ring α
- mul_comm : ∀ (x y : α), x * y = y * x
A normed commutative ring is a commutative ring endowed with a norm which satisfies
the inequality ∥x y∥ ≤ ∥x∥ ∥y∥.
@[instance]
A normed commutative ring is a seminormed commutative ring.
Equations
- normed_comm_ring.to_semi_normed_comm_ring = {to_semi_normed_ring := {to_has_norm := normed_ring.to_has_norm normed_comm_ring.to_normed_ring, to_ring := normed_ring.to_ring normed_comm_ring.to_normed_ring, to_pseudo_metric_space := metric_space.to_pseudo_metric_space normed_ring.to_metric_space, dist_eq := _, norm_mul := _}, mul_comm := _}
@[instance]
Equations
- punit.normed_comm_ring = {to_normed_ring := {to_has_norm := normed_group.to_has_norm punit.normed_group, to_ring := {add := add_comm_group.add normed_group.to_add_comm_group, add_assoc := punit.normed_comm_ring._proof_1, zero := add_comm_group.zero normed_group.to_add_comm_group, zero_add := punit.normed_comm_ring._proof_2, add_zero := punit.normed_comm_ring._proof_3, nsmul := add_comm_group.nsmul normed_group.to_add_comm_group, nsmul_zero' := punit.normed_comm_ring._proof_4, nsmul_succ' := punit.normed_comm_ring._proof_5, neg := add_comm_group.neg normed_group.to_add_comm_group, sub := add_comm_group.sub normed_group.to_add_comm_group, sub_eq_add_neg := punit.normed_comm_ring._proof_6, gsmul := add_comm_group.gsmul normed_group.to_add_comm_group, gsmul_zero' := punit.normed_comm_ring._proof_7, gsmul_succ' := punit.normed_comm_ring._proof_8, gsmul_neg' := punit.normed_comm_ring._proof_9, add_left_neg := punit.normed_comm_ring._proof_10, add_comm := punit.normed_comm_ring._proof_11, mul := comm_ring.mul punit.comm_ring, mul_assoc := _, one := comm_ring.one punit.comm_ring, one_mul := _, mul_one := _, npow := comm_ring.npow punit.comm_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}, to_metric_space := normed_group.to_metric_space punit.normed_group, dist_eq := _, norm_mul := punit.normed_comm_ring._proof_12}, mul_comm := _}
@[class]
A mixin class with the axiom ∥1∥ = 1. Many normed_rings and all normed_fields satisfy this
axiom.
@[simp]
@[instance]
Equations
- semi_normed_comm_ring.to_comm_ring = {add := ring.add semi_normed_ring.to_ring, add_assoc := _, zero := ring.zero semi_normed_ring.to_ring, zero_add := _, add_zero := _, nsmul := ring.nsmul semi_normed_ring.to_ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg semi_normed_ring.to_ring, sub := ring.sub semi_normed_ring.to_ring, sub_eq_add_neg := _, gsmul := ring.gsmul semi_normed_ring.to_ring, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := ring.mul semi_normed_ring.to_ring, mul_assoc := _, one := ring.one semi_normed_ring.to_ring, one_mul := _, mul_one := _, npow := ring.npow semi_normed_ring.to_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}
@[instance]
Equations
- normed_ring.to_normed_group = {to_has_norm := normed_ring.to_has_norm β, to_add_comm_group := {add := ring.add normed_ring.to_ring, add_assoc := _, zero := ring.zero normed_ring.to_ring, zero_add := _, add_zero := _, nsmul := ring.nsmul normed_ring.to_ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg normed_ring.to_ring, sub := ring.sub normed_ring.to_ring, sub_eq_add_neg := _, gsmul := ring.gsmul normed_ring.to_ring, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _}, to_metric_space := normed_ring.to_metric_space β, dist_eq := _}
@[instance]
Equations
- semi_normed_ring.to_semi_normed_group = {to_has_norm := semi_normed_ring.to_has_norm β, to_add_comm_group := {add := ring.add semi_normed_ring.to_ring, add_assoc := _, zero := ring.zero semi_normed_ring.to_ring, zero_add := _, add_zero := _, nsmul := ring.nsmul semi_normed_ring.to_ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg semi_normed_ring.to_ring, sub := ring.sub semi_normed_ring.to_ring, sub_eq_add_neg := _, gsmul := ring.gsmul semi_normed_ring.to_ring, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _}, to_pseudo_metric_space := semi_normed_ring.to_pseudo_metric_space β, dist_eq := _}
@[instance]
def
prod.norm_one_class
{α : Type u_1}
{β : Type u_2}
[normed_group α]
[has_one α]
[norm_one_class α]
[normed_group β]
[has_one β]
[norm_one_class β] :
norm_one_class (α × β)
@[instance]
def
subalgebra.semi_normed_ring
{𝕜 : Type u_1}
{_x : comm_ring 𝕜}
{E : Type u_2}
[semi_normed_ring E]
{_x_1 : algebra 𝕜 E}
(s : subalgebra 𝕜 E) :
A subalgebra of a seminormed ring is also a seminormed ring, with the restriction of the norm.
See note [implicit instance arguments].
Equations
@[instance]
def
subalgebra.normed_ring
{𝕜 : Type u_1}
{_x : comm_ring 𝕜}
{E : Type u_2}
[normed_ring E]
{_x_1 : algebra 𝕜 E}
(s : subalgebra 𝕜 E) :
A subalgebra of a normed ring is also a normed ring, with the restriction of the norm.
See note [implicit instance arguments].
Equations
theorem
finset.norm_prod_le'
{ι : Type u_4}
{α : Type u_1}
[normed_comm_ring α]
(s : finset ι)
(hs : s.nonempty)
(f : ι → α) :
theorem
finset.norm_prod_le
{ι : Type u_4}
{α : Type u_1}
[normed_comm_ring α]
[norm_one_class α]
(s : finset ι)
(f : ι → α) :
If α is a seminormed ring, then ∥a^n∥≤ ∥a∥^n for n > 0. See also norm_pow_le.
If α is a seminormed ring with ∥1∥=1, then ∥a^n∥≤ ∥a∥^n. See also norm_pow_le'.
In a seminormed ring, the left-multiplication add_monoid_hom is bounded.
In a seminormed ring, the right-multiplication add_monoid_hom is bounded.
@[instance]
def
prod.semi_normed_ring
{α : Type u_1}
{β : Type u_2}
[semi_normed_ring α]
[semi_normed_ring β] :
semi_normed_ring (α × β)
Seminormed ring structure on the product of two seminormed rings, using the sup norm.
@[instance]
def
prod.normed_ring
{α : Type u_1}
{β : Type u_2}
[normed_ring α]
[normed_ring β] :
normed_ring (α × β)
Normed ring structure on the product of two normed rings, using the sup norm.
@[instance]
@[instance]
A seminormed ring is a topological ring.
@[class]
- to_normed_field : normed_field α
- non_trivial : ∃ (x : α), 1 < ∥x∥
A nondiscrete normed field is a normed field in which there is an element of norm different from
0 and 1. This makes it possible to bring any element arbitrarily close to 0 by multiplication
by the powers of any element, and thus to relate algebra and topology.
@[instance]
Equations
- normed_field.to_normed_comm_ring = {to_normed_ring := {to_has_norm := normed_field.to_has_norm _inst_1, to_ring := {add := field.add normed_field.to_field, add_assoc := _, zero := field.zero normed_field.to_field, zero_add := _, add_zero := _, nsmul := field.nsmul normed_field.to_field, nsmul_zero' := _, nsmul_succ' := _, neg := field.neg normed_field.to_field, sub := field.sub normed_field.to_field, sub_eq_add_neg := _, gsmul := field.gsmul normed_field.to_field, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := field.mul normed_field.to_field, mul_assoc := _, one := field.one normed_field.to_field, one_mul := _, mul_one := _, npow := field.npow normed_field.to_field, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}, to_metric_space := normed_field.to_metric_space _inst_1, dist_eq := _, norm_mul := _}, mul_comm := _}
@[instance]
@[simp]
norm as a monoid_hom.
Equations
- normed_field.norm_hom = {to_fun := norm normed_field.to_has_norm, map_zero' := _, map_one' := _, map_mul' := _}
@[simp]
nnnorm as a monoid_hom.
Equations
- normed_field.nnnorm_hom = {to_fun := nnnorm semi_normed_group.to_has_nnnorm, map_zero' := _, map_one' := _, map_mul' := _}
@[simp]
theorem
normed_field.norm_prod
{α : Type u_1}
{β : Type u_2}
[normed_field α]
(s : finset β)
(f : β → α) :
@[simp]
theorem
normed_field.nnnorm_prod
{α : Type u_1}
{β : Type u_2}
[normed_field α]
(s : finset β)
(f : β → α) :
@[simp]
@[simp]
@[instance]
Equations
@[instance]
@[instance]
@[instance]
Equations
@[instance]
Equations
- real.nondiscrete_normed_field = {to_normed_field := real.normed_field, non_trivial := real.nondiscrete_normed_field._proof_1}
theorem
normed_group.tendsto_at_top
{α : Type u_1}
[nonempty α]
[semilattice_sup α]
{β : Type u_2}
[semi_normed_group β]
{f : α → β}
{b : β} :
A restatement of metric_space.tendsto_at_top in terms of the norm.
theorem
normed_group.tendsto_at_top'
{α : Type u_1}
[nonempty α]
[semilattice_sup α]
[no_top_order α]
{β : Type u_2}
[semi_normed_group β]
{f : α → β}
{b : β} :
A variant of normed_group.tendsto_at_top that
uses ∃ N, ∀ n > N, ... rather than ∃ N, ∀ n ≥ N, ...
@[instance]
Equations
- int.normed_comm_ring = {to_normed_ring := {to_has_norm := {norm := λ (n : ℤ), ∥↑n∥}, to_ring := int.ring, to_metric_space := int.metric_space, dist_eq := int.normed_comm_ring._proof_1, norm_mul := int.normed_comm_ring._proof_2}, mul_comm := _}
@[instance]
Equations
- rat.normed_field = {to_has_norm := {norm := λ (r : ℚ), ∥↑r∥}, to_field := rat.field, to_metric_space := rat.metric_space, dist_eq := rat.normed_field._proof_1, norm_mul' := rat.normed_field._proof_2}
@[instance]
Equations
- rat.nondiscrete_normed_field = {to_normed_field := rat.normed_field, non_trivial := rat.nondiscrete_normed_field._proof_1}
@[class]
structure
semi_normed_space
(α : Type u_5)
(β : Type u_6)
[normed_field α]
[semi_normed_group β] :
Type (max u_5 u_6)
A seminormed space over a normed field is a vector space endowed with a seminorm which satisfies
the equality ∥c • x∥ = ∥c∥ ∥x∥. We require only ∥c • x∥ ≤ ∥c∥ ∥x∥ in the definition, then prove
∥c • x∥ = ∥c∥ ∥x∥ in norm_smul.
Instances
- normed_space.to_semi_normed_space
- semi_normed_algebra.to_semi_normed_space
- prod.semi_normed_space
- pi.semi_normed_space
- submodule.semi_normed_space
- module.restrict_scalars.semi_normed_space_orig
- restrict_scalars.semi_normed_space
- continuous_linear_map.to_semi_normed_space
- pi_Lp.semi_normed_space
- normed_space.dual.semi_normed_space
@[class]
structure
normed_space
(α : Type u_5)
(β : Type u_6)
[normed_field α]
[normed_group β] :
Type (max u_5 u_6)
A normed space over a normed field is a vector space endowed with a norm which satisfies the
equality ∥c • x∥ = ∥c∥ ∥x∥. We require only ∥c • x∥ ≤ ∥c∥ ∥x∥ in the definition, then prove
∥c • x∥ = ∥c∥ ∥x∥ in norm_smul.
Instances
- normed_algebra.to_normed_space
- inner_product_space.to_normed_space
- normed_field.to_normed_space
- prod.normed_space
- pi.normed_space
- submodule.normed_space
- module.restrict_scalars.normed_space_orig
- restrict_scalars.normed_space
- continuous_linear_map.to_normed_space
- continuous_multilinear_map.to_normed_space
- bounded_continuous_function.normed_space
- continuous_map.normed_space
- measure_theory.Lp.normed_space
- measure_theory.Lp.normed_space_L1
- measure_theory.Lp.normed_space_L2
- measure_theory.Lp.normed_space_Ltop
- pi_Lp.normed_space
- normed_space.dual.normed_space
- enorm.finite_subspace.normed_space
@[instance]
def
normed_space.to_semi_normed_space
{α : Type u_1}
{β : Type u_2}
[normed_field α]
[normed_group β]
[γ : normed_space α β] :
A normed space is a seminormed space.
Equations
@[instance]
Equations
theorem
norm_smul
{α : Type u_1}
{β : Type u_2}
[normed_field α]
[semi_normed_group β]
[semi_normed_space α β]
(s : α)
(x : β) :
@[simp]
theorem
dist_smul
{α : Type u_1}
{β : Type u_2}
[normed_field α]
[semi_normed_group β]
[semi_normed_space α β]
(s : α)
(x y : β) :
theorem
nnnorm_smul
{α : Type u_1}
{β : Type u_2}
[normed_field α]
[semi_normed_group β]
[semi_normed_space α β]
(s : α)
(x : β) :
theorem
nndist_smul
{α : Type u_1}
{β : Type u_2}
[normed_field α]
[semi_normed_group β]
[semi_normed_space α β]
(s : α)
(x y : β) :
theorem
norm_smul_of_nonneg
{β : Type u_2}
[semi_normed_group β]
[semi_normed_space ℝ β]
{t : ℝ}
(ht : 0 ≤ t)
(x : β) :
@[instance]
def
semi_normed_space.has_continuous_smul
{α : Type u_1}
[normed_field α]
{E : Type u_5}
[semi_normed_group E]
[semi_normed_space α E] :
theorem
eventually_nhds_norm_smul_sub_lt
{α : Type u_1}
[normed_field α]
{E : Type u_5}
[semi_normed_group E]
[semi_normed_space α E]
(c : α)
(x : E)
{ε : ℝ}
(h : 0 < ε) :
theorem
closure_ball
{E : Type u_5}
[semi_normed_group E]
[semi_normed_space ℝ E]
(x : E)
{r : ℝ}
(hr : 0 < r) :
closure (metric.ball x r) = metric.closed_ball x r
theorem
frontier_ball
{E : Type u_5}
[semi_normed_group E]
[semi_normed_space ℝ E]
(x : E)
{r : ℝ}
(hr : 0 < r) :
frontier (metric.ball x r) = metric.sphere x r
theorem
interior_closed_ball
{E : Type u_5}
[semi_normed_group E]
[semi_normed_space ℝ E]
(x : E)
{r : ℝ}
(hr : 0 < r) :
interior (metric.closed_ball x r) = metric.ball x r
theorem
frontier_closed_ball
{E : Type u_5}
[semi_normed_group E]
[semi_normed_space ℝ E]
(x : E)
{r : ℝ}
(hr : 0 < r) :
frontier (metric.closed_ball x r) = metric.sphere x r
theorem
ne_neg_of_mem_sphere
(α : Type u_1)
[normed_field α]
{E : Type u_5}
[semi_normed_group E]
[semi_normed_space α E]
[char_zero α]
{r : ℝ}
(hr : 0 < r)
(x : ↥(metric.sphere 0 r)) :
theorem
ne_neg_of_mem_unit_sphere
(α : Type u_1)
[normed_field α]
{E : Type u_5}
[semi_normed_group E]
[semi_normed_space α E]
[char_zero α]
(x : ↥(metric.sphere 0 1)) :
@[instance]
def
prod.semi_normed_space
{α : Type u_1}
[normed_field α]
{E : Type u_5}
[semi_normed_group E]
[semi_normed_space α E]
{F : Type u_6}
[semi_normed_group F]
[semi_normed_space α F] :
semi_normed_space α (E × F)
The product of two seminormed spaces is a seminormed space, with the sup norm.
Equations
- prod.semi_normed_space = {to_module := {to_distrib_mul_action := module.to_distrib_mul_action prod.module, add_smul := _, zero_smul := _}, norm_smul_le := _}
@[instance]
def
pi.semi_normed_space
{α : Type u_1}
{ι : Type u_4}
[normed_field α]
{E : ι → Type u_2}
[fintype ι]
[Π (i : ι), semi_normed_group (E i)]
[Π (i : ι), semi_normed_space α (E i)] :
semi_normed_space α (Π (i : ι), E i)
The product of finitely many seminormed spaces is a seminormed space, with the sup norm.
Equations
- pi.semi_normed_space = {to_module := pi.module ι (λ (i : ι), E i) α (λ (i : ι), semi_normed_space.to_module), norm_smul_le := _}
@[instance]
def
submodule.semi_normed_space
{𝕜 : Type u_1}
{R : Type u_2}
[has_scalar 𝕜 R]
[normed_field 𝕜]
[ring R]
{E : Type u_3}
[semi_normed_group E]
[semi_normed_space 𝕜 E]
[module R E]
[is_scalar_tower 𝕜 R E]
(s : submodule R E) :
A subspace of a seminormed space is also a normed space, with the restriction of the norm.
Equations
- s.semi_normed_space = {to_module := s.module' _inst_13, norm_smul_le := _}
theorem
rescale_to_shell_semi_normed
{α : Type u_1}
[normed_field α]
{E : Type u_5}
[semi_normed_group E]
[semi_normed_space α E]
{c : α}
(hc : 1 < ∥c∥)
{ε : ℝ}
(εpos : 0 < ε)
{x : E}
(hx : ∥x∥ ≠ 0) :
If there is a scalar c with ∥c∥>1, then any element of with norm different from 0 can be
moved by scalar multiplication to any shell of width ∥c∥. Also recap information on the norm of
the rescaling element that shows up in applications.
theorem
interior_closed_ball'
{E : Type u_5}
[normed_group E]
[normed_space ℝ E]
[nontrivial E]
(x : E)
(r : ℝ) :
interior (metric.closed_ball x r) = metric.ball x r
theorem
frontier_closed_ball'
{E : Type u_5}
[normed_group E]
[normed_space ℝ E]
[nontrivial E]
(x : E)
(r : ℝ) :
frontier (metric.closed_ball x r) = metric.sphere x r
theorem
rescale_to_shell
{α : Type u_1}
[normed_field α]
{E : Type u_5}
[normed_group E]
[normed_space α E]
{c : α}
(hc : 1 < ∥c∥)
{ε : ℝ}
(εpos : 0 < ε)
{x : E}
(hx : x ≠ 0) :
If there is a scalar c with ∥c∥>1, then any element can be moved by scalar multiplication to
any shell of width ∥c∥. Also recap information on the norm of the rescaling element that shows
up in applications.
@[instance]
def
prod.normed_space
{α : Type u_1}
[normed_field α]
{E : Type u_5}
[normed_group E]
[normed_space α E]
{F : Type u_6}
[normed_group F]
[normed_space α F] :
normed_space α (E × F)
The product of two normed spaces is a normed space, with the sup norm.
Equations
@[instance]
def
pi.normed_space
{α : Type u_1}
{ι : Type u_4}
[normed_field α]
{E : ι → Type u_2}
[fintype ι]
[Π (i : ι), normed_group (E i)]
[Π (i : ι), normed_space α (E i)] :
normed_space α (Π (i : ι), E i)
The product of finitely many normed spaces is a normed space, with the sup norm.
Equations
@[instance]
def
submodule.normed_space
{𝕜 : Type u_1}
{R : Type u_2}
[has_scalar 𝕜 R]
[normed_field 𝕜]
[ring R]
{E : Type u_3}
[normed_group E]
[normed_space 𝕜 E]
[module R E]
[is_scalar_tower 𝕜 R E]
(s : submodule R E) :
normed_space 𝕜 ↥s
A subspace of a normed space is also a normed space, with the restriction of the norm.
Equations
@[class]
structure
semi_normed_algebra
(𝕜 : Type u_5)
(𝕜' : Type u_6)
[normed_field 𝕜]
[semi_normed_ring 𝕜'] :
Type (max u_5 u_6)
A seminormed algebra 𝕜' over 𝕜 is an algebra endowed with a seminorm for which the
embedding of 𝕜 in 𝕜' is an isometry.
Instances
@[class]
structure
normed_algebra
(𝕜 : Type u_5)
(𝕜' : Type u_6)
[normed_field 𝕜]
[normed_ring 𝕜'] :
Type (max u_5 u_6)
A normed algebra 𝕜' over 𝕜 is an algebra endowed with a norm for which the embedding of
𝕜 in 𝕜' is an isometry.
@[instance]
def
normed_algebra.to_semi_normed_algebra
(𝕜 : Type u_1)
(𝕜' : Type u_2)
[normed_field 𝕜]
[normed_ring 𝕜']
[normed_algebra 𝕜 𝕜'] :
semi_normed_algebra 𝕜 𝕜'
A normed algebra is a seminormed algebra.
Equations
- normed_algebra.to_semi_normed_algebra 𝕜 𝕜' = {to_algebra := normed_algebra.to_algebra _inst_3, norm_algebra_map_eq := _}
@[simp]
theorem
norm_algebra_map_eq
{𝕜 : Type u_1}
(𝕜' : Type u_2)
[normed_field 𝕜]
[semi_normed_ring 𝕜']
[h : semi_normed_algebra 𝕜 𝕜']
(x : 𝕜) :
theorem
algebra_map_isometry
(𝕜 : Type u_1)
(𝕜' : Type u_2)
[normed_field 𝕜]
[semi_normed_ring 𝕜']
[semi_normed_algebra 𝕜 𝕜'] :
isometry ⇑(algebra_map 𝕜 𝕜')
In a normed algebra, the inclusion of the base field in the extended field is an isometry.
@[instance]
def
semi_normed_algebra.to_semi_normed_space
(𝕜 : Type u_5)
[normed_field 𝕜]
(𝕜' : Type u_6)
[semi_normed_ring 𝕜']
[h : semi_normed_algebra 𝕜 𝕜'] :
semi_normed_space 𝕜 𝕜'
Equations
@[instance]
def
normed_algebra.to_normed_space
(𝕜 : Type u_1)
[normed_field 𝕜]
(𝕜' : Type u_2)
[normed_ring 𝕜']
[h : normed_algebra 𝕜 𝕜'] :
normed_space 𝕜 𝕜'
Equations
@[instance]
Equations
- normed_algebra.id 𝕜 = {to_algebra := {to_has_scalar := algebra.to_has_scalar (algebra.id 𝕜), to_ring_hom := algebra.to_ring_hom (algebra.id 𝕜), commutes' := _, smul_def' := _}, norm_algebra_map_eq := _}
theorem
normed_algebra.norm_one
(𝕜 : Type u_5)
[normed_field 𝕜]
(𝕜' : Type u_6)
[semi_normed_ring 𝕜']
[semi_normed_algebra 𝕜 𝕜'] :
theorem
normed_algebra.norm_one_class
(𝕜 : Type u_5)
[normed_field 𝕜]
(𝕜' : Type u_6)
[semi_normed_ring 𝕜']
[semi_normed_algebra 𝕜 𝕜'] :
theorem
normed_algebra.zero_ne_one
(𝕜 : Type u_5)
[normed_field 𝕜]
(𝕜' : Type u_6)
[semi_normed_ring 𝕜']
[semi_normed_algebra 𝕜 𝕜'] :
0 ≠ 1
theorem
normed_algebra.nontrivial
(𝕜 : Type u_5)
[normed_field 𝕜]
(𝕜' : Type u_6)
[semi_normed_ring 𝕜']
[semi_normed_algebra 𝕜 𝕜'] :
nontrivial 𝕜'
def
semi_normed_space.restrict_scalars
(𝕜 : Type u_5)
(𝕜' : Type u_6)
[normed_field 𝕜]
[normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
(F : Type u_8)
[semi_normed_group F]
[semi_normed_space 𝕜' F] :
Warning: This declaration should be used judiciously.
Please consider using is_scalar_tower instead.
𝕜-seminormed space structure induced by a 𝕜'-seminormed space structure when 𝕜' is a
seminormed algebra over 𝕜. Not registered as an instance as 𝕜' can not be inferred.
The type synonym module.restrict_scalars 𝕜 𝕜' E will be endowed with this instance by default.
Equations
- semi_normed_space.restrict_scalars 𝕜 𝕜' F = {to_module := {to_distrib_mul_action := module.to_distrib_mul_action (restrict_scalars.module 𝕜 𝕜' F), add_smul := _, zero_smul := _}, norm_smul_le := _}
def
normed_space.restrict_scalars
(𝕜 : Type u_5)
(𝕜' : Type u_6)
[normed_field 𝕜]
[normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
(E : Type u_7)
[normed_group E]
[normed_space 𝕜' E] :
normed_space 𝕜 E
Warning: This declaration should be used judiciously.
Please consider using is_scalar_tower instead.
𝕜-normed space structure induced by a 𝕜'-normed space structure when 𝕜' is a
normed algebra over 𝕜. Not registered as an instance as 𝕜' can not be inferred.
The type synonym module.restrict_scalars 𝕜 𝕜' E will be endowed with this instance by default.
Equations
- normed_space.restrict_scalars 𝕜 𝕜' E = {to_module := {to_distrib_mul_action := module.to_distrib_mul_action (restrict_scalars.module 𝕜 𝕜' E), add_smul := _, zero_smul := _}, norm_smul_le := _}
@[instance]
def
restrict_scalars.semi_normed_group
{𝕜 : Type u_1}
{𝕜' : Type u_2}
{F : Type u_3}
[I : semi_normed_group F] :
semi_normed_group (restrict_scalars 𝕜 𝕜' F)
Equations
@[instance]
def
restrict_scalars.normed_group
{𝕜 : Type u_1}
{𝕜' : Type u_2}
{E : Type u_3}
[I : normed_group E] :
normed_group (restrict_scalars 𝕜 𝕜' E)
Equations
@[instance]
def
module.restrict_scalars.semi_normed_space_orig
{𝕜 : Type u_1}
{𝕜' : Type u_2}
{F : Type u_3}
[normed_field 𝕜']
[semi_normed_group F]
[I : semi_normed_space 𝕜' F] :
semi_normed_space 𝕜' (restrict_scalars 𝕜 𝕜' F)
Equations
@[instance]
def
module.restrict_scalars.normed_space_orig
{𝕜 : Type u_1}
{𝕜' : Type u_2}
{E : Type u_3}
[normed_field 𝕜']
[normed_group E]
[I : normed_space 𝕜' E] :
normed_space 𝕜' (restrict_scalars 𝕜 𝕜' E)
Equations
@[instance]
def
restrict_scalars.semi_normed_space
(𝕜 : Type u_5)
(𝕜' : Type u_6)
[normed_field 𝕜]
[normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
(F : Type u_8)
[semi_normed_group F]
[semi_normed_space 𝕜' F] :
semi_normed_space 𝕜 (restrict_scalars 𝕜 𝕜' F)
Equations
@[instance]
def
restrict_scalars.normed_space
(𝕜 : Type u_5)
(𝕜' : Type u_6)
[normed_field 𝕜]
[normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
(E : Type u_7)
[normed_group E]
[normed_space 𝕜' E] :
normed_space 𝕜 (restrict_scalars 𝕜 𝕜' E)
Equations
- restrict_scalars.normed_space 𝕜 𝕜' E = normed_space.restrict_scalars 𝕜 𝕜' E
theorem
cauchy_seq_finset_iff_vanishing_norm
{α : Type u_1}
{ι : Type u_4}
[semi_normed_group α]
{f : ι → α} :
theorem
summable_iff_vanishing_norm
{α : Type u_1}
{ι : Type u_4}
[semi_normed_group α]
[complete_space α]
{f : ι → α} :
theorem
cauchy_seq_finset_of_norm_bounded
{α : Type u_1}
{ι : Type u_4}
[semi_normed_group α]
{f : ι → α}
(g : ι → ℝ)
(hg : summable g)
(h : ∀ (i : ι), ∥f i∥ ≤ g i) :
cauchy_seq (λ (s : finset ι), ∑ (i : ι) in s, f i)
theorem
cauchy_seq_finset_of_summable_norm
{α : Type u_1}
{ι : Type u_4}
[semi_normed_group α]
{f : ι → α}
(hf : summable (λ (a : ι), ∥f a∥)) :
cauchy_seq (λ (s : finset ι), ∑ (a : ι) in s, f a)
theorem
has_sum_of_subseq_of_summable
{α : Type u_1}
{γ : Type u_3}
{ι : Type u_4}
[semi_normed_group α]
{f : ι → α}
(hf : summable (λ (a : ι), ∥f a∥))
{s : γ → finset ι}
{p : filter γ}
[p.ne_bot]
(hs : filter.tendsto s p filter.at_top)
{a : α}
(ha : filter.tendsto (λ (b : γ), ∑ (i : ι) in s b, f i) p (𝓝 a)) :
has_sum f a
If a function f is summable in norm, and along some sequence of finsets exhausting the space
its sum is converging to a limit a, then this holds along all finsets, i.e., f is summable
with sum a.
theorem
has_sum_iff_tendsto_nat_of_summable_norm
{α : Type u_1}
[semi_normed_group α]
{f : ℕ → α}
{a : α}
(hf : summable (λ (i : ℕ), ∥f i∥)) :
has_sum f a ↔ filter.tendsto (λ (n : ℕ), ∑ (i : ℕ) in finset.range n, f i) filter.at_top (𝓝 a)
theorem
summable_of_norm_bounded
{α : Type u_1}
{ι : Type u_4}
[semi_normed_group α]
[complete_space α]
{f : ι → α}
(g : ι → ℝ)
(hg : summable g)
(h : ∀ (i : ι), ∥f i∥ ≤ g i) :
summable f
The direct comparison test for series: if the norm of f is bounded by a real function g
which is summable, then f is summable.
theorem
tsum_of_norm_bounded
{α : Type u_1}
{ι : Type u_4}
[semi_normed_group α]
{f : ι → α}
{g : ι → ℝ}
{a : ℝ}
(hg : has_sum g a)
(h : ∀ (i : ι), ∥f i∥ ≤ g i) :
Quantitative result associated to the direct comparison test for series: If ∑' i, g i is
summable, and for all i, ∥f i∥ ≤ g i, then ∥∑' i, f i∥ ≤ ∑' i, g i. Note that we do not
assume that ∑' i, f i is summable, and it might not be the case if α is not a complete space.
theorem
norm_tsum_le_tsum_norm
{α : Type u_1}
{ι : Type u_4}
[semi_normed_group α]
{f : ι → α}
(hf : summable (λ (i : ι), ∥f i∥)) :
If ∑' i, ∥f i∥ is summable, then ∥∑' i, f i∥ ≤ (∑' i, ∥f i∥). Note that we do not assume
that ∑' i, f i is summable, and it might not be the case if α is not a complete space.
theorem
tsum_of_nnnorm_bounded
{α : Type u_1}
{ι : Type u_4}
[semi_normed_group α]
{f : ι → α}
{g : ι → ℝ≥0}
{a : ℝ≥0}
(hg : has_sum g a)
(h : ∀ (i : ι), ∥f i∥₊ ≤ g i) :
Quantitative result associated to the direct comparison test for series: If ∑' i, g i is
summable, and for all i, nnnorm (f i) ≤ g i, then nnnorm (∑' i, f i) ≤ ∑' i, g i. Note that we
do not assume that ∑' i, f i is summable, and it might not be the case if α is not a complete
space.
theorem
nnnorm_tsum_le
{α : Type u_1}
{ι : Type u_4}
[semi_normed_group α]
{f : ι → α}
(hf : summable (λ (i : ι), ∥f i∥₊)) :
If ∑' i, nnnorm (f i) is summable, then nnnorm (∑' i, f i) ≤ ∑' i, nnnorm (f i). Note that
we do not assume that ∑' i, f i is summable, and it might not be the case if α is not a complete
space.
theorem
summable_of_norm_bounded_eventually
{α : Type u_1}
{ι : Type u_4}
[semi_normed_group α]
[complete_space α]
{f : ι → α}
(g : ι → ℝ)
(hg : summable g)
(h : ∀ᶠ (i : ι) in filter.cofinite, ∥f i∥ ≤ g i) :
summable f
Variant of the direct comparison test for series: if the norm of f is eventually bounded by a
real function g which is summable, then f is summable.
theorem
summable_of_nnnorm_bounded
{α : Type u_1}
{ι : Type u_4}
[semi_normed_group α]
[complete_space α]
{f : ι → α}
(g : ι → ℝ≥0)
(hg : summable g)
(h : ∀ (i : ι), ∥f i∥₊ ≤ g i) :
summable f
theorem
summable_of_summable_norm
{α : Type u_1}
{ι : Type u_4}
[semi_normed_group α]
[complete_space α]
{f : ι → α}
(hf : summable (λ (a : ι), ∥f a∥)) :
summable f
theorem
summable_of_summable_nnnorm
{α : Type u_1}
{ι : Type u_4}
[semi_normed_group α]
[complete_space α]
{f : ι → α}
(hf : summable (λ (a : ι), ∥f a∥₊)) :
summable f
@[instance]
Equations
@[simp]
@[instance]
Equations
- uniform_space.completion.normed_group V = {to_has_norm := uniform_space.completion.has_norm V semi_normed_group.to_has_norm, to_add_comm_group := {add := add_comm_group.add (show add_comm_group (uniform_space.completion V), from uniform_space.completion.add_comm_group), add_assoc := _, zero := add_comm_group.zero (show add_comm_group (uniform_space.completion V), from uniform_space.completion.add_comm_group), zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul (show add_comm_group (uniform_space.completion V), from uniform_space.completion.add_comm_group), nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg (show add_comm_group (uniform_space.completion V), from uniform_space.completion.add_comm_group), sub := add_comm_group.sub (show add_comm_group (uniform_space.completion V), from uniform_space.completion.add_comm_group), sub_eq_add_neg := _, gsmul := add_comm_group.gsmul (show add_comm_group (uniform_space.completion V), from uniform_space.completion.add_comm_group), gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _}, to_metric_space := {to_pseudo_metric_space := metric_space.to_pseudo_metric_space (show metric_space (uniform_space.completion V), from metric.completion.metric_space), eq_of_dist_eq_zero := _}, dist_eq := _}