The ratio test for series in real Banach spaces

Content created by Louis Wasserman.

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

module functional-analysis.ratio-test-series-real-banach-spaces where
Imports 
open import analysis.ratio-test-series-real-numbers

open import elementary-number-theory.natural-numbers

open import foundation.binary-transport
open import foundation.conjunction
open import foundation.dependent-pair-types
open import foundation.existential-quantification
open import foundation.identity-types
open import foundation.propositions
open import foundation.universe-levels

open import functional-analysis.absolute-convergence-series-real-banach-spaces
open import functional-analysis.convergent-series-real-banach-spaces
open import functional-analysis.real-banach-spaces
open import functional-analysis.series-real-banach-spaces

open import logic.functoriality-existential-quantification

open import real-numbers.absolute-value-real-numbers
open import real-numbers.inequality-real-numbers
open import real-numbers.multiplication-real-numbers
open import real-numbers.nonnegative-real-numbers
open import real-numbers.strict-inequality-nonnegative-real-numbers

Idea

To prove that a series ∑ aₙ in a real Banach space converges, it is sufficient to show that there exists a nonnegative real number r less than 1 such that for all n, ∥aₙ₊₁∥ ≤ r∥aₙ∥. This condition is known as the ratio test.

Definition

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

  ratio-test-prop-series-ℝ-Banach-Space : Prop (lsuc l1)
  ratio-test-prop-series-ℝ-Banach-Space =
    ∃ ( ℝ⁰⁺ l1)
      ( λ r →
        le-prop-ℝ⁰⁺ r one-ℝ⁰⁺ ∧
        Π-Prop
          ( ℕ)
          ( λ n →
            leq-prop-ℝ
              ( map-norm-ℝ-Banach-Space V
                ( term-series-ℝ-Banach-Space V σ (succ-ℕ n)))
              ( ( real-ℝ⁰⁺ r) *ℝ
                ( map-norm-ℝ-Banach-Space V
                  ( term-series-ℝ-Banach-Space V σ n)))))

  ratio-test-series-ℝ-Banach-Space : UU (lsuc l1)
  ratio-test-series-ℝ-Banach-Space =
    type-Prop ratio-test-prop-series-ℝ-Banach-Space

Properties

The ratio test implies convergence

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

  abstract
    is-convergent-ratio-test-series-ℝ-Banach-Space :
      ratio-test-series-ℝ-Banach-Space V σ →
      is-convergent-series-ℝ-Banach-Space V σ
    is-convergent-ratio-test-series-ℝ-Banach-Space H =
      is-convergent-is-absolutely-convergent-series-ℝ-Banach-Space
        ( V)
        ( σ)
        ( is-convergent-ratio-test-series-ℝ
          ( map-norm-series-ℝ-Banach-Space V σ)
          ( map-tot-exists
            ( λ r (r<1 , K) →
              ( r<1 ,
                λ n →
                binary-tr
                  ( leq-ℝ)
                  ( inv (abs-real-ℝ⁰⁺ (nonnegative-norm-ℝ-Banach-Space V _)))
                  ( ap-mul-ℝ
                    ( refl)
                    ( inv
                      ( abs-real-ℝ⁰⁺ (nonnegative-norm-ℝ-Banach-Space V _))))
                  ( K n)))
            ( H)))

See also

Recent changes