Real Banach spaces

Content created by Louis Wasserman.

Created on 2025-11-26.
Last modified on 2025-11-26.

{-# OPTIONS --lossy-unification #-}

module linear-algebra.real-banach-spaces where
Imports 
open import foundation.dependent-pair-types
open import foundation.propositions
open import foundation.subtypes
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import linear-algebra.normed-real-vector-spaces

open import metric-spaces.complete-metric-spaces

open import real-numbers.cauchy-completeness-dedekind-real-numbers

Idea

A real Banach space is a normed real vector space such that the metric space induced by the norm is complete.

Definition

is-banach-prop-Normed-ℝ-Vector-Space :
  {l1 l2 : Level} (V : Normed-ℝ-Vector-Space l1 l2) → Prop (l1 ⊔ l2)
is-banach-prop-Normed-ℝ-Vector-Space V =
  is-complete-prop-Metric-Space (metric-space-Normed-ℝ-Vector-Space V)

is-banach-Normed-ℝ-Vector-Space :
  {l1 l2 : Level} (V : Normed-ℝ-Vector-Space l1 l2) → UU (l1 ⊔ l2)
is-banach-Normed-ℝ-Vector-Space V =
  type-Prop (is-banach-prop-Normed-ℝ-Vector-Space V)

ℝ-Banach-Space : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
ℝ-Banach-Space l1 l2 =
  type-subtype (is-banach-prop-Normed-ℝ-Vector-Space {l1} {l2})

Properties

The real numbers are a real Banach space with norm x ↦ |x|

abstract
  is-banach-normed-real-vector-space-ℝ :
    (l : Level) →
    is-banach-Normed-ℝ-Vector-Space (normed-real-vector-space-ℝ l)
  is-banach-normed-real-vector-space-ℝ l =
    inv-tr
      ( is-complete-Metric-Space)
      ( eq-metric-space-normed-real-vector-space-metric-space-ℝ l)
      ( is-complete-metric-space-ℝ l)

real-banach-space-ℝ : (l : Level) → ℝ-Banach-Space l (lsuc l)
real-banach-space-ℝ l =
  ( normed-real-vector-space-ℝ l ,
    is-banach-normed-real-vector-space-ℝ l)

Recent changes