Sums of finite sequences of elements in real Banach spaces

Content created by Louis Wasserman.

Created on 2025-12-25.
Last modified on 2025-12-25.

module linear-algebra.sums-of-finite-sequences-of-elements-real-banach-spaces where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.function-types
open import foundation.universe-levels

open import linear-algebra.real-banach-spaces
open import linear-algebra.sums-of-finite-sequences-of-elements-normed-real-vector-spaces

open import lists.finite-sequences

open import real-numbers.inequality-real-numbers
open import real-numbers.sums-of-finite-sequences-of-real-numbers

Idea

The sum of a finite sequence of elements of a real Banach space is the sum of the sequence in the abelian group of the space under addition.

Definition

sum-fin-sequence-type-ℝ-Banach-Space :
  {l1 l2 : Level} (V : ℝ-Banach-Space l1 l2) →
  (n : ℕ) → fin-sequence (type-ℝ-Banach-Space V) n → type-ℝ-Banach-Space V
sum-fin-sequence-type-ℝ-Banach-Space V =
  sum-fin-sequence-type-Normed-ℝ-Vector-Space
    ( normed-vector-space-ℝ-Banach-Space V)

Properties

The norm of the sum of a finite sequence is at most the sum of the norms of the terms of the sequence

module _
  {l1 l2 : Level}
  (V : ℝ-Banach-Space l1 l2)
  where

  abstract
    triangle-inequality-norm-sum-fin-sequence-type-ℝ-Banach-Space :
      (n : ℕ) (σ : fin-sequence (type-ℝ-Banach-Space V) n) →
      leq-ℝ
        ( map-norm-ℝ-Banach-Space V
          ( sum-fin-sequence-type-ℝ-Banach-Space V n σ))
        ( sum-fin-sequence-ℝ n (map-norm-ℝ-Banach-Space V ∘ σ))
    triangle-inequality-norm-sum-fin-sequence-type-ℝ-Banach-Space =
      triangle-inequality-norm-sum-fin-sequence-type-Normed-ℝ-Vector-Space
        ( normed-vector-space-ℝ-Banach-Space V)

Recent changes