Normed vector spaces on \(\R\) and \(\C\)

InstanceNorms \(\lVert\cdot\rVert_p\) on \(\R^n\) and \(\C^n\)#

The product of finitely many normed spaces is a normed space, with the L^p norm.

PiLp.normedSpace.{u_1, u_2, u_4} (p : ENNReal) (𝕜 : Type u_1) {ι : Type u_2} (β : ι → Type u_4)
  [hp : Fact (1 ≤ p)] [Fintype ι] [NormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (β i)]
  [(i : ι) → NormedSpace 𝕜 (β i)] : NormedSpace 𝕜 (PiLp p β)

Sources

MathlibPiLp.normedSpace

Uses 2 · Used by 5

Statement usesFinite set · Normed vector space over a normed field

Used byBehrend's construction · Sphere · Closed interval · Riemannian manifold · Whitney embedding theorem

TheoremUniform convergence norm (sup-norm)#

Expressing uniform convergence on a set using edist.

EMetric.tendstoUniformlyOn_iff.{u, v, u_2} {γ : Type u} {β : Type v} [PseudoEMetricSpace γ]
  {ι : Type u_2} {F : ι → β → γ} {f : β → γ} {p : Filter ι} {s : Set β} :
  TendstoUniformlyOn F f p s ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, edist (f x) (F n x) < ε

Sources

MathlibEMetric.tendstoUniformlyOn_iff

Uses 1 · Used by 1

Statement usesReal number

Used byEgorov's theorem

InstanceNormed space of bounded continuous functions #

Mathlib states this as BoundedContinuousFunction.instNormedSpace.

BoundedContinuousFunction.instNormedSpace.{u, v, u_1} {α : Type u} {β : Type v} {𝕜 : Type u_1}
  [TopologicalSpace α] [SeminormedAddCommGroup β] [NormedField 𝕜] [NormedSpace 𝕜 β] :
  NormedSpace 𝕜 (BoundedContinuousFunction α β)

Sources

MathlibBoundedContinuousFunction.instNormedSpace

Uses 2

Statement usesContinuous function · Normed vector space over a normed field

TheoremRiesz' lemma (unit-ball characterization of finite dimension)#

Riesz's theorem: if a closed ball of positive radius is compact in a vector space, then the space is finite-dimensional.

FiniteDimensional.of_isCompact_closedBall.{u, u_1} (𝕜 : Type u) [NontriviallyNormedField 𝕜]
  [CompleteSpace 𝕜] {V : Type u_1} [NormedAddCommGroup V] [_root_.Module 𝕜 V] [ContinuousSMul 𝕜 V]
  {r : ℝ} (rpos : 0 < r) {c : V} (h : IsCompact (Metric.closedBall c r)) : FiniteDimensional 𝕜 V