19.4. Banach and Hilbert spaces🔗

To add a Banach space to the environment one writes:

variable (E 𝕜 : Type*) [NormedField 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [CompleteSpace E]

Special notation for the norm is available for vectors in a Banach space:

example (x y : E) : ‖x + y‖ ≤ ‖x‖ + ‖y‖ := norm_add_le x y

For a Hilbert space one writes:

variable (E 𝕜 : Type*) [RCLike 𝕜]
  [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [CompleteSpace E]

Special notation for the inner product is available for vectors in a Hilbert space after opening the InnerProductSpace scope:

open scoped InnerProductSpace

example (x y : E) :
    ⟪x + y, x + y⟫_𝕜 + ⟪x - y, x - y⟫_𝕜 =
      2 * (⟪x, x⟫_𝕜 + ⟪y, y⟫_𝕜) :=
  parallelogram_law