Finite dimensional normed spaces over complete fields #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Over a complete nontrivially normed field, in finite dimension, all norms are equivalent and all linear maps are continuous. Moreover, a finite-dimensional subspace is always complete and closed.
Main results: #
finite_dimensional.complete: a finite-dimensional space over a complete field is complete. This is not registered as an instance, as the field would be an unknown metavariable in typeclass resolution.submodule.closed_of_finite_dimensional: a finite-dimensional subspace over a complete field is closedfinite_dimensional.proper: a finite-dimensional space over a proper field is proper. This is not registered as an instance, as the field would be an unknown metavariable in typeclass resolution. It is however registered as an instance for𝕜 = ℝand𝕜 = ℂ. As properness implies completeness, there is no need to also registerfinite_dimensional.completeonℝorℂ.finite_dimensional_of_is_compact_closed_ball: Riesz' theorem: if the closed unit ball is compact, then the space is finite-dimensional.
Implementation notes #
The fact that all norms are equivalent is not written explicitly, as it would mean having two norms
on a single space, which is not the way type classes work. However, if one has a
finite-dimensional vector space E with a norm, and a copy E' of this type with another norm,
then the identities from E to E' and from E'to E are continuous thanks to
linear_map.continuous_of_finite_dimensional. This gives the desired norm equivalence.
noncomputable
def
linear_isometry.to_linear_isometry_equiv
{F : Type u_2}
{E₁ : Type u_3}
[seminormed_add_comm_group F]
[normed_add_comm_group E₁]
{R₁ : Type u_4}
[field R₁]
[module R₁ E₁]
[module R₁ F]
[finite_dimensional R₁ E₁]
[finite_dimensional R₁ F]
(li : E₁ →ₗᵢ[R₁] F)
(h : finite_dimensional.finrank R₁ E₁ = finite_dimensional.finrank R₁ F) :
A linear isometry between finite dimensional spaces of equal dimension can be upgraded to a linear isometry equivalence.
Equations
- li.to_linear_isometry_equiv h = {to_linear_equiv := li.to_linear_map.linear_equiv_of_injective _ h, norm_map' := _}
@[simp]
theorem
linear_isometry.coe_to_linear_isometry_equiv
{F : Type u_2}
{E₁ : Type u_3}
[seminormed_add_comm_group F]
[normed_add_comm_group E₁]
{R₁ : Type u_4}
[field R₁]
[module R₁ E₁]
[module R₁ F]
[finite_dimensional R₁ E₁]
[finite_dimensional R₁ F]
(li : E₁ →ₗᵢ[R₁] F)
(h : finite_dimensional.finrank R₁ E₁ = finite_dimensional.finrank R₁ F) :
⇑(li.to_linear_isometry_equiv h) = ⇑li
@[simp]
theorem
linear_isometry.to_linear_isometry_equiv_apply
{F : Type u_2}
{E₁ : Type u_3}
[seminormed_add_comm_group F]
[normed_add_comm_group E₁]
{R₁ : Type u_4}
[field R₁]
[module R₁ E₁]
[module R₁ F]
[finite_dimensional R₁ E₁]
[finite_dimensional R₁ F]
(li : E₁ →ₗᵢ[R₁] F)
(h : finite_dimensional.finrank R₁ E₁ = finite_dimensional.finrank R₁ F)
(x : E₁) :
⇑(li.to_linear_isometry_equiv h) x = ⇑li x
noncomputable
def
affine_isometry.to_affine_isometry_equiv
{𝕜 : Type u_1}
{V₁ : Type u_2}
{V₂ : Type u_3}
{P₁ : Type u_4}
{P₂ : Type u_5}
[normed_field 𝕜]
[normed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V₁]
[normed_space 𝕜 V₂]
[metric_space P₁]
[pseudo_metric_space P₂]
[normed_add_torsor V₁ P₁]
[normed_add_torsor V₂ P₂]
[finite_dimensional 𝕜 V₁]
[finite_dimensional 𝕜 V₂]
[inhabited P₁]
(li : P₁ →ᵃⁱ[𝕜] P₂)
(h : finite_dimensional.finrank 𝕜 V₁ = finite_dimensional.finrank 𝕜 V₂) :
An affine isometry between finite dimensional spaces of equal dimension can be upgraded to an affine isometry equivalence.
Equations
- li.to_affine_isometry_equiv h = affine_isometry_equiv.mk' ⇑li (li.linear_isometry.to_linear_isometry_equiv h) (arbitrary P₁) _
@[simp]
theorem
affine_isometry.coe_to_affine_isometry_equiv
{𝕜 : Type u_1}
{V₁ : Type u_2}
{V₂ : Type u_3}
{P₁ : Type u_4}
{P₂ : Type u_5}
[normed_field 𝕜]
[normed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V₁]
[normed_space 𝕜 V₂]
[metric_space P₁]
[pseudo_metric_space P₂]
[normed_add_torsor V₁ P₁]
[normed_add_torsor V₂ P₂]
[finite_dimensional 𝕜 V₁]
[finite_dimensional 𝕜 V₂]
[inhabited P₁]
(li : P₁ →ᵃⁱ[𝕜] P₂)
(h : finite_dimensional.finrank 𝕜 V₁ = finite_dimensional.finrank 𝕜 V₂) :
⇑(li.to_affine_isometry_equiv h) = ⇑li
@[simp]
theorem
affine_isometry.to_affine_isometry_equiv_apply
{𝕜 : Type u_1}
{V₁ : Type u_2}
{V₂ : Type u_3}
{P₁ : Type u_4}
{P₂ : Type u_5}
[normed_field 𝕜]
[normed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V₁]
[normed_space 𝕜 V₂]
[metric_space P₁]
[pseudo_metric_space P₂]
[normed_add_torsor V₁ P₁]
[normed_add_torsor V₂ P₂]
[finite_dimensional 𝕜 V₁]
[finite_dimensional 𝕜 V₂]
[inhabited P₁]
(li : P₁ →ᵃⁱ[𝕜] P₂)
(h : finite_dimensional.finrank 𝕜 V₁ = finite_dimensional.finrank 𝕜 V₂)
(x : P₁) :
⇑(li.to_affine_isometry_equiv h) x = ⇑li x
theorem
affine_map.continuous_of_finite_dimensional
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type v}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type w}
[normed_add_comm_group F]
[normed_space 𝕜 F]
[complete_space 𝕜]
{PE : Type u_1}
{PF : Type u_2}
[metric_space PE]
[normed_add_torsor E PE]
[metric_space PF]
[normed_add_torsor F PF]
[finite_dimensional 𝕜 E]
(f : PE →ᵃ[𝕜] PF) :
theorem
affine_equiv.continuous_of_finite_dimensional
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type v}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type w}
[normed_add_comm_group F]
[normed_space 𝕜 F]
[complete_space 𝕜]
{PE : Type u_1}
{PF : Type u_2}
[metric_space PE]
[normed_add_torsor E PE]
[metric_space PF]
[normed_add_torsor F PF]
[finite_dimensional 𝕜 E]
(f : PE ≃ᵃ[𝕜] PF) :
def
affine_equiv.to_homeomorph_of_finite_dimensional
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type v}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type w}
[normed_add_comm_group F]
[normed_space 𝕜 F]
[complete_space 𝕜]
{PE : Type u_1}
{PF : Type u_2}
[metric_space PE]
[normed_add_torsor E PE]
[metric_space PF]
[normed_add_torsor F PF]
[finite_dimensional 𝕜 E]
(f : PE ≃ᵃ[𝕜] PF) :
PE ≃ₜ PF
Reinterpret an affine equivalence as a homeomorphism.
Equations
- f.to_homeomorph_of_finite_dimensional = {to_equiv := f.to_equiv, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
affine_equiv.coe_to_homeomorph_of_finite_dimensional
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type v}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type w}
[normed_add_comm_group F]
[normed_space 𝕜 F]
[complete_space 𝕜]
{PE : Type u_1}
{PF : Type u_2}
[metric_space PE]
[normed_add_torsor E PE]
[metric_space PF]
[normed_add_torsor F PF]
[finite_dimensional 𝕜 E]
(f : PE ≃ᵃ[𝕜] PF) :
@[simp]
theorem
affine_equiv.coe_to_homeomorph_of_finite_dimensional_symm
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type v}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type w}
[normed_add_comm_group F]
[normed_space 𝕜 F]
[complete_space 𝕜]
{PE : Type u_1}
{PF : Type u_2}
[metric_space PE]
[normed_add_torsor E PE]
[metric_space PF]
[normed_add_torsor F PF]
[finite_dimensional 𝕜 E]
(f : PE ≃ᵃ[𝕜] PF) :
theorem
continuous_linear_map.continuous_det
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type v}
[normed_add_comm_group E]
[normed_space 𝕜 E]
[complete_space 𝕜] :
continuous (λ (f : E →L[𝕜] E), f.det)
@[irreducible]
noncomputable
def
lipschitz_extension_constant
(E' : Type u_1)
[normed_add_comm_group E']
[normed_space ℝ E']
[finite_dimensional ℝ E'] :
Any K-Lipschitz map from a subset s of a metric space α to a finite-dimensional real
vector space E' can be extended to a Lipschitz map on the whole space α, with a slightly worse
constant C * K where C only depends on E'. We record a working value for this constant C
as lipschitz_extension_constant E'.
Equations
- lipschitz_extension_constant E' = let A : E' ≃L[ℝ] ↥(basis.of_vector_space_index ℝ E') → ℝ := (basis.of_vector_space ℝ E').equiv_fun.to_continuous_linear_equiv in linear_order.max (‖A.symm.to_continuous_linear_map‖₊ * ‖A.to_continuous_linear_map‖₊) 1
theorem
lipschitz_extension_constant_pos
(E' : Type u_1)
[normed_add_comm_group E']
[normed_space ℝ E']
[finite_dimensional ℝ E'] :
theorem
lipschitz_on_with.extend_finite_dimension
{α : Type u_1}
[pseudo_metric_space α]
{E' : Type u_2}
[normed_add_comm_group E']
[normed_space ℝ E']
[finite_dimensional ℝ E']
{s : set α}
{f : α → E'}
{K : nnreal}
(hf : lipschitz_on_with K f s) :
∃ (g : α → E'), lipschitz_with (lipschitz_extension_constant E' * K) g ∧ set.eq_on f g s
Any K-Lipschitz map from a subset s of a metric space α to a finite-dimensional real
vector space E' can be extended to a Lipschitz map on the whole space α, with a slightly worse
constant lipschitz_extension_constant E' * K.
theorem
linear_map.exists_antilipschitz_with
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type v}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type w}
[normed_add_comm_group F]
[normed_space 𝕜 F]
[complete_space 𝕜]
[finite_dimensional 𝕜 E]
(f : E →ₗ[𝕜] F)
(hf : linear_map.ker f = ⊥) :
@[protected]
theorem
linear_independent.eventually
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type v}
[normed_add_comm_group E]
[normed_space 𝕜 E]
[complete_space 𝕜]
{ι : Type u_1}
[finite ι]
{f : ι → E}
(hf : linear_independent 𝕜 f) :
theorem
is_open_set_of_linear_independent
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type v}
[normed_add_comm_group E]
[normed_space 𝕜 E]
[complete_space 𝕜]
{ι : Type u_1}
[finite ι] :
is_open {f : ι → E | linear_independent 𝕜 f}
theorem
is_open_set_of_nat_le_rank
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type v}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type w}
[normed_add_comm_group F]
[normed_space 𝕜 F]
[complete_space 𝕜]
(n : ℕ) :
theorem
basis.op_nnnorm_le
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type v}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type w}
[normed_add_comm_group F]
[normed_space 𝕜 F]
[complete_space 𝕜]
{ι : Type u_1}
[fintype ι]
(v : basis ι 𝕜 E)
{u : E →L[𝕜] F}
(M : nnreal)
(hu : ∀ (i : ι), ‖⇑u (⇑v i)‖₊ ≤ M) :
theorem
basis.op_norm_le
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type v}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type w}
[normed_add_comm_group F]
[normed_space 𝕜 F]
[complete_space 𝕜]
{ι : Type u_1}
[fintype ι]
(v : basis ι 𝕜 E)
{u : E →L[𝕜] F}
{M : ℝ}
(hM : 0 ≤ M)
(hu : ∀ (i : ι), ‖⇑u (⇑v i)‖ ≤ M) :
theorem
basis.exists_op_nnnorm_le
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type v}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type w}
[normed_add_comm_group F]
[normed_space 𝕜 F]
[complete_space 𝕜]
{ι : Type u_1}
[finite ι]
(v : basis ι 𝕜 E) :
A weaker version of basis.op_nnnorm_le that abstracts away the value of C.
theorem
basis.exists_op_norm_le
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type v}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type w}
[normed_add_comm_group F]
[normed_space 𝕜 F]
[complete_space 𝕜]
{ι : Type u_1}
[finite ι]
(v : basis ι 𝕜 E) :
A weaker version of basis.op_norm_le that abstracts away the value of C.
@[protected, instance]
def
continuous_linear_map.topological_space.second_countable_topology
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type v}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type w}
[normed_add_comm_group F]
[normed_space 𝕜 F]
[complete_space 𝕜]
[finite_dimensional 𝕜 E]
[topological_space.second_countable_topology F] :
theorem
finite_dimensional.complete
(𝕜 : Type u)
[nontrivially_normed_field 𝕜]
(E : Type v)
[normed_add_comm_group E]
[normed_space 𝕜 E]
[complete_space 𝕜]
[finite_dimensional 𝕜 E] :
theorem
submodule.complete_of_finite_dimensional
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type v}
[normed_add_comm_group E]
[normed_space 𝕜 E]
[complete_space 𝕜]
(s : submodule 𝕜 E)
[finite_dimensional 𝕜 ↥s] :
A finite-dimensional subspace is complete.
theorem
submodule.closed_of_finite_dimensional
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type v}
[normed_add_comm_group E]
[normed_space 𝕜 E]
[complete_space 𝕜]
(s : submodule 𝕜 E)
[finite_dimensional 𝕜 ↥s] :
A finite-dimensional subspace is closed.
theorem
affine_subspace.closed_of_finite_dimensional
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type v}
[normed_add_comm_group E]
[normed_space 𝕜 E]
[complete_space 𝕜]
{P : Type u_1}
[metric_space P]
[normed_add_torsor E P]
(s : affine_subspace 𝕜 P)
[finite_dimensional 𝕜 ↥(s.direction)] :
theorem
exists_norm_le_le_norm_sub_of_finset
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type v}
[normed_add_comm_group E]
[normed_space 𝕜 E]
[complete_space 𝕜]
{c : 𝕜}
(hc : 1 < ‖c‖)
{R : ℝ}
(hR : ‖c‖ < R)
(h : ¬finite_dimensional 𝕜 E)
(s : finset E) :
In an infinite dimensional space, given a finite number of points, one may find a point
with norm at most R which is at distance at least 1 of all these points.
theorem
exists_seq_norm_le_one_le_norm_sub'
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type v}
[normed_add_comm_group E]
[normed_space 𝕜 E]
[complete_space 𝕜]
{c : 𝕜}
(hc : 1 < ‖c‖)
{R : ℝ}
(hR : ‖c‖ < R)
(h : ¬finite_dimensional 𝕜 E) :
In an infinite-dimensional normed space, there exists a sequence of points which are all
bounded by R and at distance at least 1. For a version not assuming c and R, see
exists_seq_norm_le_one_le_norm_sub.
theorem
finite_dimensional_of_is_compact_closed_ball₀
(𝕜 : Type u)
[nontrivially_normed_field 𝕜]
{E : Type v}
[normed_add_comm_group E]
[normed_space 𝕜 E]
[complete_space 𝕜]
{r : ℝ}
(rpos : 0 < r)
(h : is_compact (metric.closed_ball 0 r)) :
Riesz's theorem: if a closed ball with center zero of positive radius is compact in a vector space, then the space is finite-dimensional.
theorem
finite_dimensional_of_is_compact_closed_ball
(𝕜 : Type u)
[nontrivially_normed_field 𝕜]
{E : Type v}
[normed_add_comm_group E]
[normed_space 𝕜 E]
[complete_space 𝕜]
{r : ℝ}
(rpos : 0 < r)
{c : E}
(h : is_compact (metric.closed_ball c r)) :
Riesz's theorem: if a closed ball of positive radius is compact in a vector space, then the space is finite-dimensional.
theorem
has_compact_support.eq_zero_or_finite_dimensional
(𝕜 : Type u)
[nontrivially_normed_field 𝕜]
{E : Type v}
[normed_add_comm_group E]
[normed_space 𝕜 E]
[complete_space 𝕜]
{X : Type u_1}
[topological_space X]
[has_zero X]
[t2_space X]
{f : E → X}
(hf : has_compact_support f)
(h'f : continuous f) :
f = 0 ∨ finite_dimensional 𝕜 E
If a function has compact support, then either the function is trivial or the space if finite-dimensional.
theorem
has_compact_mul_support.eq_one_or_finite_dimensional
(𝕜 : Type u)
[nontrivially_normed_field 𝕜]
{E : Type v}
[normed_add_comm_group E]
[normed_space 𝕜 E]
[complete_space 𝕜]
{X : Type u_1}
[topological_space X]
[has_one X]
[t2_space X]
{f : E → X}
(hf : has_compact_mul_support f)
(h'f : continuous f) :
f = 1 ∨ finite_dimensional 𝕜 E
If a function has compact multiplicative support, then either the function is trivial or the space if finite-dimensional.
theorem
linear_equiv.closed_embedding_of_injective
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type v}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type w}
[normed_add_comm_group F]
[normed_space 𝕜 F]
[complete_space 𝕜]
{f : E →ₗ[𝕜] F}
(hf : linear_map.ker f = ⊥)
[finite_dimensional 𝕜 E] :
An injective linear map with finite-dimensional domain is a closed embedding.
theorem
continuous_linear_map.exists_right_inverse_of_surjective
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type v}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type w}
[normed_add_comm_group F]
[normed_space 𝕜 F]
[complete_space 𝕜]
[finite_dimensional 𝕜 F]
(f : E →L[𝕜] F)
(hf : linear_map.range f = ⊤) :
theorem
closed_embedding_smul_left
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type v}
[normed_add_comm_group E]
[normed_space 𝕜 E]
[complete_space 𝕜]
{c : E}
(hc : c ≠ 0) :
closed_embedding (λ (x : 𝕜), x • c)
theorem
is_closed_map_smul_left
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type v}
[normed_add_comm_group E]
[normed_space 𝕜 E]
[complete_space 𝕜]
(c : E) :
is_closed_map (λ (x : 𝕜), x • c)
def
continuous_linear_equiv.pi_ring
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type v}
[normed_add_comm_group E]
[normed_space 𝕜 E]
[complete_space 𝕜]
(ι : Type u_1)
[fintype ι]
[decidable_eq ι] :
Continuous linear equivalence between continuous linear functions 𝕜ⁿ → E and Eⁿ.
The spaces 𝕜ⁿ and Eⁿ are represented as ι → 𝕜 and ι → E, respectively,
where ι is a finite type.
Equations
- continuous_linear_equiv.pi_ring ι = {to_linear_equiv := {to_fun := (linear_map.to_continuous_linear_map.symm.trans (linear_equiv.pi_ring 𝕜 E ι 𝕜)).to_fun, map_add' := _, map_smul' := _, inv_fun := (linear_map.to_continuous_linear_map.symm.trans (linear_equiv.pi_ring 𝕜 E ι 𝕜)).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
theorem
continuous_on_clm_apply
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type v}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type w}
[normed_add_comm_group F]
[normed_space 𝕜 F]
[complete_space 𝕜]
{X : Type u_1}
[topological_space X]
[finite_dimensional 𝕜 E]
{f : X → (E →L[𝕜] F)}
{s : set X} :
continuous_on f s ↔ ∀ (y : E), continuous_on (λ (x : X), ⇑(f x) y) s
A family of continuous linear maps is continuous on s if all its applications are.
theorem
continuous_clm_apply
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type v}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type w}
[normed_add_comm_group F]
[normed_space 𝕜 F]
[complete_space 𝕜]
{X : Type u_1}
[topological_space X]
[finite_dimensional 𝕜 E]
{f : X → (E →L[𝕜] F)} :
continuous f ↔ ∀ (y : E), continuous (λ (x : X), ⇑(f x) y)
theorem
finite_dimensional.proper
(𝕜 : Type u)
[nontrivially_normed_field 𝕜]
(E : Type v)
[normed_add_comm_group E]
[normed_space 𝕜 E]
[proper_space 𝕜]
[finite_dimensional 𝕜 E] :
Any finite-dimensional vector space over a proper field is proper.
We do not register this as an instance to avoid an instance loop when trying to prove the
properness of 𝕜, and the search for 𝕜 as an unknown metavariable. Declare the instance
explicitly when needed.
@[protected, instance]
def
finite_dimensional.proper_real
(E : Type u)
[normed_add_comm_group E]
[normed_space ℝ E]
[finite_dimensional ℝ E] :
theorem
exists_mem_frontier_inf_dist_compl_eq_dist
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
[finite_dimensional ℝ E]
{x : E}
{s : set E}
(hx : x ∈ s)
(hs : s ≠ set.univ) :
∃ (y : E) (H : y ∈ frontier s), metric.inf_dist x sᶜ = has_dist.dist x y
If E is a finite dimensional normed real vector space, x : E, and s is a neighborhood of
x that is not equal to the whole space, then there exists a point y ∈ frontier s at distance
metric.inf_dist x sᶜ from x. See also
is_compact.exists_mem_frontier_inf_dist_compl_eq_dist.
theorem
is_compact.exists_mem_frontier_inf_dist_compl_eq_dist
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
[nontrivial E]
{x : E}
{K : set E}
(hK : is_compact K)
(hx : x ∈ K) :
∃ (y : E) (H : y ∈ frontier K), metric.inf_dist x Kᶜ = has_dist.dist x y
If K is a compact set in a nontrivial real normed space and x ∈ K, then there exists a point
y of the boundary of K at distance metric.inf_dist x Kᶜ from x. See also
exists_mem_frontier_inf_dist_compl_eq_dist.
theorem
summable_norm_iff
{α : Type u_1}
{E : Type u_2}
[normed_add_comm_group E]
[normed_space ℝ E]
[finite_dimensional ℝ E]
{f : α → E} :
In a finite dimensional vector space over ℝ, the series ∑ x, ‖f x‖ is unconditionally
summable if and only if the series ∑ x, f x is unconditionally summable. One implication holds in
any complete normed space, while the other holds only in finite dimensional spaces.
theorem
summable_of_is_O'
{ι : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_add_comm_group F]
[normed_space ℝ F]
[finite_dimensional ℝ F]
{f : ι → E}
{g : ι → F}
(hg : summable g)
(h : f =O[filter.cofinite] g) :
summable f
theorem
summable_of_is_O_nat'
{E : Type u_1}
{F : Type u_2}
[normed_add_comm_group E]
[complete_space E]
[normed_add_comm_group F]
[normed_space ℝ F]
[finite_dimensional ℝ F]
{f : ℕ → E}
{g : ℕ → F}
(hg : summable g)
(h : f =O[filter.at_top] g) :
summable f
theorem
summable_of_is_equivalent
{ι : Type u_1}
{E : Type u_2}
[normed_add_comm_group E]
[normed_space ℝ E]
[finite_dimensional ℝ E]
{f g : ι → E}
(hg : summable g)
(h : asymptotics.is_equivalent filter.cofinite f g) :
summable f
theorem
summable_of_is_equivalent_nat
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
[finite_dimensional ℝ E]
{f g : ℕ → E}
(hg : summable g)
(h : asymptotics.is_equivalent filter.at_top f g) :
summable f
theorem
is_equivalent.summable_iff
{ι : Type u_1}
{E : Type u_2}
[normed_add_comm_group E]
[normed_space ℝ E]
[finite_dimensional ℝ E]
{f g : ι → E}
(h : asymptotics.is_equivalent filter.cofinite f g) :
theorem
is_equivalent.summable_iff_nat
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
[finite_dimensional ℝ E]
{f g : ℕ → E}
(h : asymptotics.is_equivalent filter.at_top f g) :