Documentation

Mathlib.Analysis.InnerProductSpace.l2Space

Hilbert sum of a family of inner product spaces #

Given a family (G : ι → Type*) [Π i, InnerProductSpace 𝕜 (G i)] of inner product spaces, this file equips lp G 2 with an inner product space structure, where lp G 2 consists of those dependent functions f : Π i, G i for which ∑' i, ‖f i‖ ^ 2, the sum of the norms-squared, is summable. This construction is sometimes called the Hilbert sum of the family G. By choosing G to be ι → 𝕜, the Hilbert space ℓ²(ι, 𝕜) may be seen as a special case of this construction.

We also define a predicate IsHilbertSum 𝕜 G V, where V : Π i, G i →ₗᵢ[𝕜] E, expressing that V is an OrthogonalFamily and that the associated map lp G 2 →ₗᵢ[𝕜] E is surjective.

Main definitions #

Main results #

Keywords #

Hilbert space, Hilbert sum, l2, Hilbert basis, unitary equivalence, isometric isomorphism

ℓ²(ι, 𝕜) is the Hilbert space of square-summable functions ι → 𝕜, herein implemented as lp (fun i : ι => 𝕜) 2.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    Inner product space structure on lp G 2 #

    theorem lp.summable_inner {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] (f : (lp G 2)) (g : (lp G 2)) :
    Summable fun (i : ι) => inner (f i) (g i)
    instance lp.instInnerProductSpace {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] :
    InnerProductSpace 𝕜 (lp G 2)
    Equations
    theorem lp.inner_eq_tsum {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] (f : (lp G 2)) (g : (lp G 2)) :
    inner f g = ∑' (i : ι), inner (f i) (g i)
    theorem lp.hasSum_inner {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] (f : (lp G 2)) (g : (lp G 2)) :
    HasSum (fun (i : ι) => inner (f i) (g i)) (inner f g)
    theorem lp.inner_single_left {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] [DecidableEq ι] (i : ι) (a : G i) (f : (lp G 2)) :
    inner (lp.single 2 i a) f = inner a (f i)
    theorem lp.inner_single_right {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] [DecidableEq ι] (i : ι) (a : G i) (f : (lp G 2)) :
    inner f (lp.single 2 i a) = inner (f i) a

    Identification of a general Hilbert space E with a Hilbert sum #

    theorem OrthogonalFamily.summable_of_lp {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] [CompleteSpace E] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : OrthogonalFamily 𝕜 G V) (f : (lp G 2)) :
    Summable fun (i : ι) => (V i) (f i)
    def OrthogonalFamily.linearIsometry {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] [CompleteSpace E] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : OrthogonalFamily 𝕜 G V) :
    (lp G 2) →ₗᵢ[𝕜] E

    A mutually orthogonal family of subspaces of E induce a linear isometry from lp 2 of the subspaces into E.

    Equations
    • hV.linearIsometry = { toFun := fun (f : (lp G 2)) => ∑' (i : ι), (V i) (f i), map_add' := , map_smul' := , norm_map' := }
    Instances For
      theorem OrthogonalFamily.linearIsometry_apply {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] [CompleteSpace E] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : OrthogonalFamily 𝕜 G V) (f : (lp G 2)) :
      hV.linearIsometry f = ∑' (i : ι), (V i) (f i)
      theorem OrthogonalFamily.hasSum_linearIsometry {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] [CompleteSpace E] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : OrthogonalFamily 𝕜 G V) (f : (lp G 2)) :
      HasSum (fun (i : ι) => (V i) (f i)) (hV.linearIsometry f)
      @[simp]
      theorem OrthogonalFamily.linearIsometry_apply_single {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] [CompleteSpace E] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : OrthogonalFamily 𝕜 G V) [DecidableEq ι] {i : ι} (x : G i) :
      hV.linearIsometry (lp.single 2 i x) = (V i) x
      theorem OrthogonalFamily.linearIsometry_apply_dfinsupp_sum_single {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] [CompleteSpace E] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : OrthogonalFamily 𝕜 G V) [DecidableEq ι] [(i : ι) → DecidableEq (G i)] (W₀ : Π₀ (i : ι), G i) :
      hV.linearIsometry (W₀.sum (lp.single 2)) = W₀.sum fun (i : ι) => (V i)
      theorem OrthogonalFamily.range_linearIsometry {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] [CompleteSpace E] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : OrthogonalFamily 𝕜 G V) [∀ (i : ι), CompleteSpace (G i)] :
      LinearMap.range hV.linearIsometry.toLinearMap = (⨆ (i : ι), LinearMap.range (V i).toLinearMap).topologicalClosure

      The canonical linear isometry from the lp 2 of a mutually orthogonal family of subspaces of E into E, has range the closure of the span of the subspaces.

      structure IsHilbertSum {ι : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (G : ιType u_4) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] [CompleteSpace E] (V : (i : ι) → G i →ₗᵢ[𝕜] E) :

      Given a family of Hilbert spaces G : ι → Type*, a Hilbert sum of G consists of a Hilbert space E and an orthogonal family V : Π i, G i →ₗᵢ[𝕜] E such that the induced isometry Φ : lp G 2 → E is surjective.

      Keeping in mind that lp G 2 is "the" external Hilbert sum of G : ι → Type*, this is analogous to DirectSum.IsInternal, except that we don't express it in terms of actual submodules.

      • ofSurjective :: (
        • OrthogonalFamily : OrthogonalFamily 𝕜 G V

          The orthogonal family constituting the summands in the Hilbert sum.

        • surjective_isometry : Function.Surjective .linearIsometry

          The isometry lp G 2 → E induced by the orthogonal family is surjective.

      • )
      Instances For
        theorem IsHilbertSum.OrthogonalFamily {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] [CompleteSpace E] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (self : IsHilbertSum 𝕜 G V) :

        The orthogonal family constituting the summands in the Hilbert sum.

        theorem IsHilbertSum.surjective_isometry {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] [CompleteSpace E] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (self : IsHilbertSum 𝕜 G V) :
        Function.Surjective .linearIsometry

        The isometry lp G 2 → E induced by the orthogonal family is surjective.

        theorem IsHilbertSum.mk {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] [CompleteSpace E] {V : (i : ι) → G i →ₗᵢ[𝕜] E} [∀ (i : ι), CompleteSpace (G i)] (hVortho : OrthogonalFamily 𝕜 G V) (hVtotal : (⨆ (i : ι), LinearMap.range (V i).toLinearMap).topologicalClosure) :
        IsHilbertSum 𝕜 G V

        If V : Π i, G i →ₗᵢ[𝕜] E is an orthogonal family such that the supremum of the ranges of V i is dense, then (E, V) is a Hilbert sum of G.

        theorem IsHilbertSum.mkInternal {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (F : ιSubmodule 𝕜 E) [∀ (i : ι), CompleteSpace (F i)] (hFortho : OrthogonalFamily 𝕜 (fun (i : ι) => (F i)) fun (i : ι) => (F i).subtypeₗᵢ) (hFtotal : (⨆ (i : ι), F i).topologicalClosure) :
        IsHilbertSum 𝕜 (fun (i : ι) => (F i)) fun (i : ι) => (F i).subtypeₗᵢ

        This is Orthonormal.isHilbertSum in the case of actual inclusions from subspaces.

        noncomputable def IsHilbertSum.linearIsometryEquiv {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] [CompleteSpace E] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : IsHilbertSum 𝕜 G V) :
        E ≃ₗᵢ[𝕜] (lp G 2)

        A Hilbert sum (E, V) of G is canonically isomorphic to the Hilbert sum of G, i.e lp G 2.

        Note that this goes in the opposite direction from OrthogonalFamily.linearIsometry.

        Equations
        Instances For
          theorem IsHilbertSum.linearIsometryEquiv_symm_apply {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] [CompleteSpace E] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : IsHilbertSum 𝕜 G V) (w : (lp G 2)) :
          hV.linearIsometryEquiv.symm w = ∑' (i : ι), (V i) (w i)

          In the canonical isometric isomorphism between a Hilbert sum E of G and lp G 2, a vector w : lp G 2 is the image of the infinite sum of the associated elements in E.

          theorem IsHilbertSum.hasSum_linearIsometryEquiv_symm {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] [CompleteSpace E] {V : (i : ι) → G i →ₗᵢ[𝕜] E} (hV : IsHilbertSum 𝕜 G V) (w : (lp G 2)) :
          HasSum (fun (i : ι) => (V i) (w i)) (hV.linearIsometryEquiv.symm w)

          In the canonical isometric isomorphism between a Hilbert sum E of G and lp G 2, a vector w : lp G 2 is the image of the infinite sum of the associated elements in E, and this sum indeed converges.

          @[simp]
          theorem IsHilbertSum.linearIsometryEquiv_symm_apply_single {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] [CompleteSpace E] {V : (i : ι) → G i →ₗᵢ[𝕜] E} [DecidableEq ι] (hV : IsHilbertSum 𝕜 G V) {i : ι} (x : G i) :
          hV.linearIsometryEquiv.symm (lp.single 2 i x) = (V i) x

          In the canonical isometric isomorphism between a Hilbert sum E of G : ι → Type* and lp G 2, an "elementary basis vector" in lp G 2 supported at i : ι is the image of the associated element in E.

          theorem IsHilbertSum.linearIsometryEquiv_symm_apply_dfinsupp_sum_single {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] [CompleteSpace E] {V : (i : ι) → G i →ₗᵢ[𝕜] E} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] (hV : IsHilbertSum 𝕜 G V) (W₀ : Π₀ (i : ι), G i) :
          hV.linearIsometryEquiv.symm (W₀.sum (lp.single 2)) = W₀.sum fun (i : ι) => (V i)

          In the canonical isometric isomorphism between a Hilbert sum E of G : ι → Type* and lp G 2, a finitely-supported vector in lp G 2 is the image of the associated finite sum of elements of E.

          @[simp]
          theorem IsHilbertSum.linearIsometryEquiv_apply_dfinsupp_sum_single {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {G : ιType u_4} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] [CompleteSpace E] {V : (i : ι) → G i →ₗᵢ[𝕜] E} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] (hV : IsHilbertSum 𝕜 G V) (W₀ : Π₀ (i : ι), G i) :
          (W₀.sum fun (a : ι) (b : G a) => hV.linearIsometryEquiv ((V a) b)) = W₀

          In the canonical isometric isomorphism between a Hilbert sum E of G : ι → Type* and lp G 2, a finitely-supported vector in lp G 2 is the image of the associated finite sum of elements of E.

          theorem Orthonormal.isHilbertSum {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {v : ιE} (hv : Orthonormal 𝕜 v) (hsp : (Submodule.span 𝕜 (Set.range v)).topologicalClosure) :
          IsHilbertSum 𝕜 (fun (x : ι) => 𝕜) fun (i : ι) => LinearIsometry.toSpanSingleton 𝕜 E

          Given a total orthonormal family v : ι → E, E is a Hilbert sum of fun i : ι => 𝕜 relative to the family of linear isometries fun i k => k • v i.

          theorem Submodule.isHilbertSumOrthogonal {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (K : Submodule 𝕜 E) [hK : CompleteSpace K] :
          IsHilbertSum 𝕜 (fun (b : Bool) => (bif b then K else K)) fun (b : Bool) => (bif b then K else K).subtypeₗᵢ

          Hilbert bases #

          structure HilbertBasis (ι : Type u_1) (𝕜 : Type u_2) [RCLike 𝕜] (E : Type u_3) [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] :
          Type (max (max u_1 u_2) u_3)

          A Hilbert basis on ι for an inner product space E is an identification of E with the lp space ℓ²(ι, 𝕜).

          • ofRepr :: (
            • repr : E ≃ₗᵢ[𝕜] (lp (fun (i : ι) => 𝕜) 2)

              The linear isometric equivalence implementing identifying the Hilbert space with ℓ².

          • )
          Instances For
            instance HilbertBasis.instInhabitedSubtypePreLpMemAddSubgroupLpOfNatENNReal {𝕜 : Type u_2} [RCLike 𝕜] {ι : Type u_5} :
            Inhabited (HilbertBasis ι 𝕜 (lp (fun (i : ι) => 𝕜) 2))
            Equations
            • HilbertBasis.instInhabitedSubtypePreLpMemAddSubgroupLpOfNatENNReal = { default := { repr := LinearIsometryEquiv.refl 𝕜 (lp (fun (i : ι) => 𝕜) 2) } }
            instance HilbertBasis.instCoeFun {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] :
            CoeFun (HilbertBasis ι 𝕜 E) fun (x : HilbertBasis ι 𝕜 E) => ιE

            b i is the ith basis vector.

            Equations
            • HilbertBasis.instCoeFun = { coe := fun (b : HilbertBasis ι 𝕜 E) (i : ι) => b.repr.symm (lp.single 2 i 1) }
            theorem HilbertBasis.repr_symm_single {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [DecidableEq ι] (b : HilbertBasis ι 𝕜 E) (i : ι) :
            b.repr.symm (lp.single 2 i 1) = (fun (i : ι) => b.repr.symm (lp.single 2 i 1)) i
            theorem HilbertBasis.repr_self {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [DecidableEq ι] (b : HilbertBasis ι 𝕜 E) (i : ι) :
            b.repr ((fun (i : ι) => b.repr.symm (lp.single 2 i 1)) i) = lp.single 2 i 1
            theorem HilbertBasis.repr_apply_apply {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (b : HilbertBasis ι 𝕜 E) (v : E) (i : ι) :
            (b.repr v) i = inner ((fun (i : ι) => b.repr.symm (lp.single 2 i 1)) i) v
            @[simp]
            theorem HilbertBasis.orthonormal {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (b : HilbertBasis ι 𝕜 E) :
            Orthonormal 𝕜 fun (i : ι) => b.repr.symm (lp.single 2 i 1)
            theorem HilbertBasis.hasSum_repr_symm {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (b : HilbertBasis ι 𝕜 E) (f : (lp (fun (i : ι) => 𝕜) 2)) :
            HasSum (fun (i : ι) => f i (fun (i : ι) => b.repr.symm (lp.single 2 i 1)) i) (b.repr.symm f)
            theorem HilbertBasis.hasSum_repr {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (b : HilbertBasis ι 𝕜 E) (x : E) :
            HasSum (fun (i : ι) => (b.repr x) i (fun (i : ι) => b.repr.symm (lp.single 2 i 1)) i) x
            @[simp]
            theorem HilbertBasis.dense_span {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (b : HilbertBasis ι 𝕜 E) :
            (Submodule.span 𝕜 (Set.range fun (i : ι) => b.repr.symm (lp.single 2 i 1))).topologicalClosure =
            theorem HilbertBasis.hasSum_inner_mul_inner {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (b : HilbertBasis ι 𝕜 E) (x : E) (y : E) :
            HasSum (fun (i : ι) => inner x ((fun (i : ι) => b.repr.symm (lp.single 2 i 1)) i) * inner ((fun (i : ι) => b.repr.symm (lp.single 2 i 1)) i) y) (inner x y)
            theorem HilbertBasis.summable_inner_mul_inner {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (b : HilbertBasis ι 𝕜 E) (x : E) (y : E) :
            Summable fun (i : ι) => inner x ((fun (i : ι) => b.repr.symm (lp.single 2 i 1)) i) * inner ((fun (i : ι) => b.repr.symm (lp.single 2 i 1)) i) y
            theorem HilbertBasis.tsum_inner_mul_inner {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (b : HilbertBasis ι 𝕜 E) (x : E) (y : E) :
            ∑' (i : ι), inner x ((fun (i : ι) => b.repr.symm (lp.single 2 i 1)) i) * inner ((fun (i : ι) => b.repr.symm (lp.single 2 i 1)) i) y = inner x y
            def HilbertBasis.toOrthonormalBasis {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : HilbertBasis ι 𝕜 E) :

            A finite Hilbert basis is an orthonormal basis.

            Equations
            Instances For
              @[simp]
              theorem HilbertBasis.coe_toOrthonormalBasis {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : HilbertBasis ι 𝕜 E) :
              b.toOrthonormalBasis = fun (i : ι) => b.repr.symm (lp.single 2 i 1)
              theorem HilbertBasis.hasSum_orthogonalProjection {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} [CompleteSpace U] (b : HilbertBasis ι 𝕜 U) (x : E) :
              HasSum (fun (i : ι) => inner (↑((fun (i : ι) => b.repr.symm (lp.single 2 i 1)) i)) x (fun (i : ι) => b.repr.symm (lp.single 2 i 1)) i) ((orthogonalProjection U) x)
              theorem HilbertBasis.finite_spans_dense {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [DecidableEq E] (b : HilbertBasis ι 𝕜 E) :
              (⨆ (J : Finset ι), Submodule.span 𝕜 (Finset.image (fun (i : ι) => b.repr.symm (lp.single 2 i 1)) J)).topologicalClosure =
              def HilbertBasis.mk {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {v : ιE} (hv : Orthonormal 𝕜 v) (hsp : (Submodule.span 𝕜 (Set.range v)).topologicalClosure) :
              HilbertBasis ι 𝕜 E

              An orthonormal family of vectors whose span is dense in the whole module is a Hilbert basis.

              Equations
              Instances For
                theorem Orthonormal.linearIsometryEquiv_symm_apply_single_one {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {v : ιE} (hv : Orthonormal 𝕜 v) [DecidableEq ι] (h : (Submodule.span 𝕜 (Set.range v)).topologicalClosure) (i : ι) :
                .linearIsometryEquiv.symm (lp.single 2 i 1) = v i
                @[simp]
                theorem HilbertBasis.coe_mk {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {v : ιE} (hv : Orthonormal 𝕜 v) (hsp : (Submodule.span 𝕜 (Set.range v)).topologicalClosure) :
                (fun (i : ι) => (HilbertBasis.mk hv hsp).repr.symm (lp.single 2 i 1)) = v
                def HilbertBasis.mkOfOrthogonalEqBot {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {v : ιE} (hv : Orthonormal 𝕜 v) (hsp : (Submodule.span 𝕜 (Set.range v)) = ) :
                HilbertBasis ι 𝕜 E

                An orthonormal family of vectors whose span has trivial orthogonal complement is a Hilbert basis.

                Equations
                Instances For
                  @[simp]
                  theorem HilbertBasis.coe_mkOfOrthogonalEqBot {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {v : ιE} (hv : Orthonormal 𝕜 v) (hsp : (Submodule.span 𝕜 (Set.range v)) = ) :
                  (fun (i : ι) => (HilbertBasis.mkOfOrthogonalEqBot hv hsp).repr.symm (lp.single 2 i 1)) = v
                  def OrthonormalBasis.toHilbertBasis {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) :
                  HilbertBasis ι 𝕜 E

                  An orthonormal basis is a Hilbert basis.

                  Equations
                  Instances For
                    @[simp]
                    theorem OrthonormalBasis.coe_toHilbertBasis {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) :
                    (fun (i : ι) => b.toHilbertBasis.repr.symm (lp.single 2 i 1)) = b
                    theorem Orthonormal.exists_hilbertBasis_extension {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {s : Set E} (hs : Orthonormal 𝕜 Subtype.val) :
                    ∃ (w : Set E) (b : HilbertBasis (↑w) 𝕜 E), s w (fun (i : w) => b.repr.symm (lp.single 2 i 1)) = Subtype.val

                    A Hilbert space admits a Hilbert basis extending a given orthonormal subset.

                    theorem exists_hilbertBasis (𝕜 : Type u_2) [RCLike 𝕜] (E : Type u_3) [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] :
                    ∃ (w : Set E) (b : HilbertBasis (↑w) 𝕜 E), (fun (i : w) => b.repr.symm (lp.single 2 i 1)) = Subtype.val

                    A Hilbert space admits a Hilbert basis.