Documentation

Mathlib.Analysis.InnerProductSpace.Projection

The orthogonal projection #

Given a nonempty complete subspace K of an inner product space E, this file constructs orthogonalProjection K : E โ†’L[๐•œ] K, the orthogonal projection of E onto K. This map satisfies: for any point u in E, the point v = orthogonalProjection K u in K minimizes the distance โ€–u - vโ€– to u.

Also a linear isometry equivalence reflection K : E โ‰ƒโ‚—แตข[๐•œ] E is constructed, by choosing, for each u : E, the point reflection K u to satisfy u + (reflection K u) = 2 โ€ข orthogonalProjection K u.

Basic API for orthogonalProjection and reflection is developed.

Next, the orthogonal projection is used to prove a series of more subtle lemmas about the orthogonal complement of complete subspaces of E (the orthogonal complement itself was defined in Analysis.InnerProductSpace.Orthogonal); the lemma Submodule.sup_orthogonal_of_completeSpace, stating that for a complete subspace K of E we have K โŠ” Kแ—ฎ = โŠค, is a typical example.

References #

The orthogonal projection construction is adapted from

The Coq code is available at the following address: http://www.lri.fr/~sboldo/elfic/index.html

Orthogonal projection in inner product spaces #

theorem exists_norm_eq_iInf_of_complete_convex {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace โ„ F] {K : Set F} (ne : K.Nonempty) (hโ‚ : IsComplete K) (hโ‚‚ : Convex โ„ K) (u : F) :
โˆƒ v โˆˆ K, โ€–u - vโ€– = โจ… (w : โ†‘K), โ€–u - โ†‘wโ€–

Existence of minimizers Let u be a point in a real inner product space, and let K be a nonempty complete convex subset. Then there exists a (unique) v in K that minimizes the distance โ€–u - vโ€– to u.

theorem norm_eq_iInf_iff_real_inner_le_zero {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace โ„ F] {K : Set F} (h : Convex โ„ K) {u : F} {v : F} (hv : v โˆˆ K) :
โ€–u - vโ€– = โจ… (w : โ†‘K), โ€–u - โ†‘wโ€– โ†” โˆ€ w โˆˆ K, inner (u - v) (w - v) โ‰ค 0

Characterization of minimizers for the projection on a convex set in a real inner product space.

theorem exists_norm_eq_iInf_of_complete_subspace {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] (K : Submodule ๐•œ E) (h : IsComplete โ†‘K) (u : E) :
โˆƒ v โˆˆ K, โ€–u - vโ€– = โจ… (w : โ†‘โ†‘K), โ€–u - โ†‘wโ€–

Existence of projections on complete subspaces. Let u be a point in an inner product space, and let K be a nonempty complete subspace. Then there exists a (unique) v in K that minimizes the distance โ€–u - vโ€– to u. This point v is usually called the orthogonal projection of u onto K.

theorem norm_eq_iInf_iff_real_inner_eq_zero {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace โ„ F] (K : Submodule โ„ F) {u : F} {v : F} (hv : v โˆˆ K) :
โ€–u - vโ€– = โจ… (w : โ†‘โ†‘K), โ€–u - โ†‘wโ€– โ†” โˆ€ w โˆˆ K, inner (u - v) w = 0

Characterization of minimizers in the projection on a subspace, in the real case. Let u be a point in a real inner product space, and let K be a nonempty subspace. Then point v minimizes the distance โ€–u - vโ€– over points in K if and only if for all w โˆˆ K, โŸชu - v, wโŸซ = 0 (i.e., u - v is orthogonal to the subspace K). This is superseded by norm_eq_iInf_iff_inner_eq_zero that gives the same conclusion over any RCLike field.

theorem norm_eq_iInf_iff_inner_eq_zero {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] (K : Submodule ๐•œ E) {u : E} {v : E} (hv : v โˆˆ K) :
โ€–u - vโ€– = โจ… (w : โ†ฅK), โ€–u - โ†‘wโ€– โ†” โˆ€ w โˆˆ K, inner (u - v) w = 0

Characterization of minimizers in the projection on a subspace. Let u be a point in an inner product space, and let K be a nonempty subspace. Then point v minimizes the distance โ€–u - vโ€– over points in K if and only if for all w โˆˆ K, โŸชu - v, wโŸซ = 0 (i.e., u - v is orthogonal to the subspace K)

class HasOrthogonalProjection {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] (K : Submodule ๐•œ E) :

A subspace K : Submodule ๐•œ E has an orthogonal projection if every vector v : E admits an orthogonal projection to K.

  • exists_orthogonal : โˆ€ (v : E), โˆƒ w โˆˆ K, v - w โˆˆ Kแ—ฎ
Instances
    theorem HasOrthogonalProjection.exists_orthogonal {๐•œ : Type u_1} {E : Type u_2} :
    โˆ€ {inst : RCLike ๐•œ} {inst_1 : NormedAddCommGroup E} {inst_2 : InnerProductSpace ๐•œ E} {K : Submodule ๐•œ E} [self : HasOrthogonalProjection K] (v : E), โˆƒ w โˆˆ K, v - w โˆˆ Kแ—ฎ
    @[instance 100]
    instance HasOrthogonalProjection.ofCompleteSpace {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] (K : Submodule ๐•œ E) [CompleteSpace โ†ฅK] :
    Equations
    • โ‹ฏ = โ‹ฏ
    instance instHasOrthogonalProjectionOrthogonal {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] (K : Submodule ๐•œ E) [HasOrthogonalProjection K] :
    Equations
    • โ‹ฏ = โ‹ฏ
    instance HasOrthogonalProjection.map_linearIsometryEquiv {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] (K : Submodule ๐•œ E) [HasOrthogonalProjection K] {E' : Type u_4} [NormedAddCommGroup E'] [InnerProductSpace ๐•œ E'] (f : E โ‰ƒโ‚—แตข[๐•œ] E') :
    HasOrthogonalProjection (Submodule.map (โ†‘f.toLinearEquiv) K)
    Equations
    • โ‹ฏ = โ‹ฏ
    instance HasOrthogonalProjection.map_linearIsometryEquiv' {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] (K : Submodule ๐•œ E) [HasOrthogonalProjection K] {E' : Type u_4} [NormedAddCommGroup E'] [InnerProductSpace ๐•œ E'] (f : E โ‰ƒโ‚—แตข[๐•œ] E') :
    HasOrthogonalProjection (Submodule.map f.toLinearIsometry K)
    Equations
    • โ‹ฏ = โ‹ฏ
    Equations
    • โ‹ฏ = โ‹ฏ
    def orthogonalProjectionFn {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] (K : Submodule ๐•œ E) [HasOrthogonalProjection K] (v : E) :
    E

    The orthogonal projection onto a complete subspace, as an unbundled function. This definition is only intended for use in setting up the bundled version orthogonalProjection and should not be used once that is defined.

    Equations
    Instances For
      theorem orthogonalProjectionFn_mem {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} [HasOrthogonalProjection K] (v : E) :

      The unbundled orthogonal projection is in the given subspace. This lemma is only intended for use in setting up the bundled version and should not be used once that is defined.

      theorem orthogonalProjectionFn_inner_eq_zero {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} [HasOrthogonalProjection K] (v : E) (w : E) :
      w โˆˆ K โ†’ inner (v - orthogonalProjectionFn K v) w = 0

      The characterization of the unbundled orthogonal projection. This lemma is only intended for use in setting up the bundled version and should not be used once that is defined.

      theorem eq_orthogonalProjectionFn_of_mem_of_inner_eq_zero {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} [HasOrthogonalProjection K] {u : E} {v : E} (hvm : v โˆˆ K) (hvo : โˆ€ w โˆˆ K, inner (u - v) w = 0) :

      The unbundled orthogonal projection is the unique point in K with the orthogonality property. This lemma is only intended for use in setting up the bundled version and should not be used once that is defined.

      def orthogonalProjection {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] (K : Submodule ๐•œ E) [HasOrthogonalProjection K] :
      E โ†’L[๐•œ] โ†ฅK

      The orthogonal projection onto a complete subspace.

      Equations
      Instances For
        @[simp]
        theorem orthogonalProjectionFn_eq {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} [HasOrthogonalProjection K] (v : E) :
        @[simp]
        theorem orthogonalProjection_inner_eq_zero {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} [HasOrthogonalProjection K] (v : E) (w : E) :
        w โˆˆ K โ†’ inner (v - โ†‘((orthogonalProjection K) v)) w = 0

        The characterization of the orthogonal projection.

        @[simp]
        theorem sub_orthogonalProjection_mem_orthogonal {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} [HasOrthogonalProjection K] (v : E) :

        The difference of v from its orthogonal projection onto K is in Kแ—ฎ.

        theorem eq_orthogonalProjection_of_mem_of_inner_eq_zero {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} [HasOrthogonalProjection K] {u : E} {v : E} (hvm : v โˆˆ K) (hvo : โˆ€ w โˆˆ K, inner (u - v) w = 0) :
        โ†‘((orthogonalProjection K) u) = v

        The orthogonal projection is the unique point in K with the orthogonality property.

        theorem eq_orthogonalProjection_of_mem_orthogonal {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} [HasOrthogonalProjection K] {u : E} {v : E} (hv : v โˆˆ K) (hvo : u - v โˆˆ Kแ—ฎ) :
        โ†‘((orthogonalProjection K) u) = v

        A point in K with the orthogonality property (here characterized in terms of Kแ—ฎ) must be the orthogonal projection.

        theorem eq_orthogonalProjection_of_mem_orthogonal' {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} [HasOrthogonalProjection K] {u : E} {v : E} {z : E} (hv : v โˆˆ K) (hz : z โˆˆ Kแ—ฎ) (hu : u = v + z) :
        โ†‘((orthogonalProjection K) u) = v

        A point in K with the orthogonality property (here characterized in terms of Kแ—ฎ) must be the orthogonal projection.

        @[simp]
        theorem orthogonalProjection_orthogonal_val {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} [HasOrthogonalProjection K] (u : E) :
        โ†‘((orthogonalProjection Kแ—ฎ) u) = u - โ†‘((orthogonalProjection K) u)
        theorem orthogonalProjection_orthogonal {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} [HasOrthogonalProjection K] (u : E) :
        (orthogonalProjection Kแ—ฎ) u = โŸจu - โ†‘((orthogonalProjection K) u), โ‹ฏโŸฉ
        theorem orthogonalProjection_minimal {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {U : Submodule ๐•œ E} [HasOrthogonalProjection U] (y : E) :
        โ€–y - โ†‘((orthogonalProjection U) y)โ€– = โจ… (x : โ†ฅU), โ€–y - โ†‘xโ€–

        The orthogonal projection of y on U minimizes the distance โ€–y - xโ€– for x โˆˆ U.

        theorem eq_orthogonalProjection_of_eq_submodule {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} [HasOrthogonalProjection K] {K' : Submodule ๐•œ E} [HasOrthogonalProjection K'] (h : K = K') (u : E) :
        โ†‘((orthogonalProjection K) u) = โ†‘((orthogonalProjection K') u)

        The orthogonal projections onto equal subspaces are coerced back to the same point in E.

        @[simp]
        theorem orthogonalProjection_mem_subspace_eq_self {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} [HasOrthogonalProjection K] (v : โ†ฅK) :
        (orthogonalProjection K) โ†‘v = v

        The orthogonal projection sends elements of K to themselves.

        theorem orthogonalProjection_eq_self_iff {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} [HasOrthogonalProjection K] {v : E} :
        โ†‘((orthogonalProjection K) v) = v โ†” v โˆˆ K

        A point equals its orthogonal projection if and only if it lies in the subspace.

        @[simp]
        theorem orthogonalProjection_eq_zero_iff {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} [HasOrthogonalProjection K] {v : E} :
        @[simp]
        theorem ker_orthogonalProjection {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} [HasOrthogonalProjection K] :
        theorem LinearIsometry.map_orthogonalProjection {๐•œ : Type u_1} [RCLike ๐•œ] {E : Type u_4} {E' : Type u_5} [NormedAddCommGroup E] [NormedAddCommGroup E'] [InnerProductSpace ๐•œ E] [InnerProductSpace ๐•œ E'] (f : E โ†’โ‚—แตข[๐•œ] E') (p : Submodule ๐•œ E) [HasOrthogonalProjection p] [HasOrthogonalProjection (Submodule.map f.toLinearMap p)] (x : E) :
        f โ†‘((orthogonalProjection p) x) = โ†‘((orthogonalProjection (Submodule.map f.toLinearMap p)) (f x))
        theorem LinearIsometry.map_orthogonalProjection' {๐•œ : Type u_1} [RCLike ๐•œ] {E : Type u_4} {E' : Type u_5} [NormedAddCommGroup E] [NormedAddCommGroup E'] [InnerProductSpace ๐•œ E] [InnerProductSpace ๐•œ E'] (f : E โ†’โ‚—แตข[๐•œ] E') (p : Submodule ๐•œ E) [HasOrthogonalProjection p] [HasOrthogonalProjection (Submodule.map f p)] (x : E) :
        f โ†‘((orthogonalProjection p) x) = โ†‘((orthogonalProjection (Submodule.map f p)) (f x))
        theorem orthogonalProjection_map_apply {๐•œ : Type u_1} [RCLike ๐•œ] {E : Type u_4} {E' : Type u_5} [NormedAddCommGroup E] [NormedAddCommGroup E'] [InnerProductSpace ๐•œ E] [InnerProductSpace ๐•œ E'] (f : E โ‰ƒโ‚—แตข[๐•œ] E') (p : Submodule ๐•œ E) [HasOrthogonalProjection p] (x : E') :
        โ†‘((orthogonalProjection (Submodule.map (โ†‘f.toLinearEquiv) p)) x) = f โ†‘((orthogonalProjection p) (f.symm x))

        Orthogonal projection onto the Submodule.map of a subspace.

        @[simp]
        theorem orthogonalProjection_bot {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] :

        The orthogonal projection onto the trivial submodule is the zero map.

        theorem orthogonalProjection_norm_le {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] (K : Submodule ๐•œ E) [HasOrthogonalProjection K] :

        The orthogonal projection has norm โ‰ค 1.

        theorem smul_orthogonalProjection_singleton (๐•œ : Type u_1) {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {v : E} (w : E) :
        โ†‘(โ€–vโ€– ^ 2) โ€ข โ†‘((orthogonalProjection (Submodule.span ๐•œ {v})) w) = inner v w โ€ข v
        theorem orthogonalProjection_singleton (๐•œ : Type u_1) {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {v : E} (w : E) :
        โ†‘((orthogonalProjection (Submodule.span ๐•œ {v})) w) = (inner v w / โ†‘(โ€–vโ€– ^ 2)) โ€ข v

        Formula for orthogonal projection onto a single vector.

        theorem orthogonalProjection_unit_singleton (๐•œ : Type u_1) {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {v : E} (hv : โ€–vโ€– = 1) (w : E) :
        โ†‘((orthogonalProjection (Submodule.span ๐•œ {v})) w) = inner v w โ€ข v

        Formula for orthogonal projection onto a single unit vector.

        def reflectionLinearEquiv {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] (K : Submodule ๐•œ E) [HasOrthogonalProjection K] :
        E โ‰ƒโ‚—[๐•œ] E

        Auxiliary definition for reflection: the reflection as a linear equivalence.

        Equations
        Instances For
          def reflection {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] (K : Submodule ๐•œ E) [HasOrthogonalProjection K] :

          Reflection in a complete subspace of an inner product space. The word "reflection" is sometimes understood to mean specifically reflection in a codimension-one subspace, and sometimes more generally to cover operations such as reflection in a point. The definition here, of reflection in a subspace, is a more general sense of the word that includes both those common cases.

          Equations
          Instances For
            theorem reflection_apply {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} [HasOrthogonalProjection K] (p : E) :
            (reflection K) p = 2 โ€ข โ†‘((orthogonalProjection K) p) - p

            The result of reflecting.

            @[simp]
            theorem reflection_symm {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} [HasOrthogonalProjection K] :

            Reflection is its own inverse.

            @[simp]
            theorem reflection_inv {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} [HasOrthogonalProjection K] :

            Reflection is its own inverse.

            @[simp]
            theorem reflection_reflection {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] (K : Submodule ๐•œ E) [HasOrthogonalProjection K] (p : E) :
            (reflection K) ((reflection K) p) = p

            Reflecting twice in the same subspace.

            theorem reflection_involutive {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] (K : Submodule ๐•œ E) [HasOrthogonalProjection K] :

            Reflection is involutive.

            @[simp]
            theorem reflection_trans_reflection {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] (K : Submodule ๐•œ E) [HasOrthogonalProjection K] :

            Reflection is involutive.

            @[simp]
            theorem reflection_mul_reflection {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] (K : Submodule ๐•œ E) [HasOrthogonalProjection K] :

            Reflection is involutive.

            theorem reflection_orthogonal_apply {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] (K : Submodule ๐•œ E) [HasOrthogonalProjection K] (v : E) :
            theorem reflection_orthogonal {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] (K : Submodule ๐•œ E) [HasOrthogonalProjection K] :
            theorem reflection_singleton_apply {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] (u : E) (v : E) :
            (reflection (Submodule.span ๐•œ {u})) v = 2 โ€ข (inner u v / โ†‘โ€–uโ€– ^ 2) โ€ข u - v
            theorem reflection_eq_self_iff {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} [HasOrthogonalProjection K] (x : E) :

            A point is its own reflection if and only if it is in the subspace.

            theorem reflection_mem_subspace_eq_self {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} [HasOrthogonalProjection K] {x : E} (hx : x โˆˆ K) :
            (reflection K) x = x
            theorem reflection_map_apply {๐•œ : Type u_1} [RCLike ๐•œ] {E : Type u_4} {E' : Type u_5} [NormedAddCommGroup E] [NormedAddCommGroup E'] [InnerProductSpace ๐•œ E] [InnerProductSpace ๐•œ E'] (f : E โ‰ƒโ‚—แตข[๐•œ] E') (K : Submodule ๐•œ E) [HasOrthogonalProjection K] (x : E') :
            (reflection (Submodule.map (โ†‘f.toLinearEquiv) K)) x = f ((reflection K) (f.symm x))

            Reflection in the Submodule.map of a subspace.

            theorem reflection_map {๐•œ : Type u_1} [RCLike ๐•œ] {E : Type u_4} {E' : Type u_5} [NormedAddCommGroup E] [NormedAddCommGroup E'] [InnerProductSpace ๐•œ E] [InnerProductSpace ๐•œ E'] (f : E โ‰ƒโ‚—แตข[๐•œ] E') (K : Submodule ๐•œ E) [HasOrthogonalProjection K] :
            reflection (Submodule.map (โ†‘f.toLinearEquiv) K) = f.symm.trans ((reflection K).trans f)

            Reflection in the Submodule.map of a subspace.

            @[simp]
            theorem reflection_bot {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] :

            Reflection through the trivial subspace {0} is just negation.

            theorem Submodule.sup_orthogonal_inf_of_completeSpace {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {Kโ‚ : Submodule ๐•œ E} {Kโ‚‚ : Submodule ๐•œ E} (h : Kโ‚ โ‰ค Kโ‚‚) [HasOrthogonalProjection Kโ‚] :
            Kโ‚ โŠ” Kโ‚แ—ฎ โŠ“ Kโ‚‚ = Kโ‚‚

            If Kโ‚ is complete and contained in Kโ‚‚, Kโ‚ and Kโ‚แ—ฎ โŠ“ Kโ‚‚ span Kโ‚‚.

            theorem Submodule.sup_orthogonal_of_completeSpace {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} [HasOrthogonalProjection K] :

            If K is complete, K and Kแ—ฎ span the whole space.

            theorem Submodule.exists_add_mem_mem_orthogonal {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] (K : Submodule ๐•œ E) [HasOrthogonalProjection K] (v : E) :
            โˆƒ y โˆˆ K, โˆƒ z โˆˆ Kแ—ฎ, v = y + z

            If K is complete, any v in E can be expressed as a sum of elements of K and Kแ—ฎ.

            @[simp]
            theorem Submodule.orthogonal_orthogonal {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] (K : Submodule ๐•œ E) [HasOrthogonalProjection K] :

            If K admits an orthogonal projection, then the orthogonal complement of its orthogonal complement is itself.

            theorem Submodule.orthogonal_orthogonal_eq_closure {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] (K : Submodule ๐•œ E) [CompleteSpace E] :
            Kแ—ฎแ—ฎ = K.topologicalClosure

            In a Hilbert space, the orthogonal complement of the orthogonal complement of a subspace K is the topological closure of K.

            Note that the completeness assumption is necessary. Let E be the space โ„• โ†’โ‚€ โ„ with inner space structure inherited from PiLp 2 (fun _ : โ„• โ†ฆ โ„). Let K be the subspace of sequences with the sum of all elements equal to zero. Then Kแ—ฎ = โŠฅ, Kแ—ฎแ—ฎ = โŠค.

            theorem Submodule.isCompl_orthogonal_of_completeSpace {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} [HasOrthogonalProjection K] :

            If K admits an orthogonal projection, K and Kแ—ฎ are complements of each other.

            @[simp]
            theorem orthogonalComplement_eq_orthogonalComplement {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} {L : Submodule ๐•œ E} [HasOrthogonalProjection K] [HasOrthogonalProjection L] :
            @[simp]
            theorem Submodule.orthogonal_eq_bot_iff {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} [HasOrthogonalProjection K] :
            theorem orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} [HasOrthogonalProjection K] {v : E} (hv : v โˆˆ Kแ—ฎ) :

            The orthogonal projection onto K of an element of Kแ—ฎ is zero.

            theorem Submodule.IsOrtho.orthogonalProjection_comp_subtypeL {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {U : Submodule ๐•œ E} {V : Submodule ๐•œ E} [HasOrthogonalProjection U] (h : U โŸ‚ V) :
            (orthogonalProjection U).comp V.subtypeL = 0

            The projection into U from an orthogonal submodule V is the zero map.

            theorem orthogonalProjection_comp_subtypeL_eq_zero_iff {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {U : Submodule ๐•œ E} {V : Submodule ๐•œ E} [HasOrthogonalProjection U] :
            (orthogonalProjection U).comp V.subtypeL = 0 โ†” U โŸ‚ V

            The projection into U from V is the zero map if and only if U and V are orthogonal.

            theorem orthogonalProjection_eq_linear_proj {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} [HasOrthogonalProjection K] (x : E) :
            (orthogonalProjection K) x = (K.linearProjOfIsCompl Kแ—ฎ โ‹ฏ) x
            theorem orthogonalProjection_coe_linearMap_eq_linearProj {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} [HasOrthogonalProjection K] :
            โ†‘(orthogonalProjection K) = K.linearProjOfIsCompl Kแ—ฎ โ‹ฏ
            theorem reflection_mem_subspace_orthogonalComplement_eq_neg {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} [HasOrthogonalProjection K] {v : E} (hv : v โˆˆ Kแ—ฎ) :
            (reflection K) v = -v

            The reflection in K of an element of Kแ—ฎ is its negation.

            The orthogonal projection onto Kแ—ฎ of an element of K is zero.

            theorem orthogonalProjection_orthogonalProjection_of_le {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {U : Submodule ๐•œ E} {V : Submodule ๐•œ E} [HasOrthogonalProjection U] [HasOrthogonalProjection V] (h : U โ‰ค V) (x : E) :

            If U โ‰ค V, then projecting on V and then on U is the same as projecting on U.

            theorem orthogonalProjection_tendsto_closure_iSup {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] [CompleteSpace E] {ฮน : Type u_4} [SemilatticeSup ฮน] (U : ฮน โ†’ Submodule ๐•œ E) [โˆ€ (i : ฮน), CompleteSpace โ†ฅ(U i)] (hU : Monotone U) (x : E) :
            Filter.Tendsto (fun (i : ฮน) => โ†‘((orthogonalProjection (U i)) x)) Filter.atTop (nhds โ†‘((orthogonalProjection (โจ† (i : ฮน), U i).topologicalClosure) x))

            Given a monotone family U of complete submodules of E and a fixed x : E, the orthogonal projection of x on U i tends to the orthogonal projection of x on (โจ† i, U i).topologicalClosure along atTop.

            theorem orthogonalProjection_tendsto_self {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] [CompleteSpace E] {ฮน : Type u_4} [SemilatticeSup ฮน] (U : ฮน โ†’ Submodule ๐•œ E) [โˆ€ (t : ฮน), CompleteSpace โ†ฅ(U t)] (hU : Monotone U) (x : E) (hU' : โŠค โ‰ค (โจ† (t : ฮน), U t).topologicalClosure) :
            Filter.Tendsto (fun (t : ฮน) => โ†‘((orthogonalProjection (U t)) x)) Filter.atTop (nhds x)

            Given a monotone family U of complete submodules of E with dense span supremum, and a fixed x : E, the orthogonal projection of x on U i tends to x along at_top.

            theorem Submodule.triorthogonal_eq_orthogonal {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} [CompleteSpace E] :

            The orthogonal complement satisfies Kแ—ฎแ—ฎแ—ฎ = Kแ—ฎ.

            theorem Submodule.topologicalClosure_eq_top_iff {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} [CompleteSpace E] :
            K.topologicalClosure = โŠค โ†” Kแ—ฎ = โŠฅ

            The closure of K is the full space iff Kแ—ฎ is trivial.

            theorem Dense.eq_zero_of_inner_left {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} {x : E} (hK : Dense โ†‘K) (h : โˆ€ (v : โ†ฅK), inner x โ†‘v = 0) :
            x = 0
            theorem Dense.eq_zero_of_mem_orthogonal {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} {x : E} (hK : Dense โ†‘K) (h : x โˆˆ Kแ—ฎ) :
            x = 0
            theorem Dense.eq_of_sub_mem_orthogonal {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} {x : E} {y : E} (hK : Dense โ†‘K) (h : x - y โˆˆ Kแ—ฎ) :
            x = y

            If S is dense and x - y โˆˆ Kแ—ฎ, then x = y.

            theorem Dense.eq_of_inner_left {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} {x : E} {y : E} (hK : Dense โ†‘K) (h : โˆ€ (v : โ†ฅK), inner x โ†‘v = inner y โ†‘v) :
            x = y
            theorem Dense.eq_of_inner_right {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} {x : E} {y : E} (hK : Dense โ†‘K) (h : โˆ€ (v : โ†ฅK), inner (โ†‘v) x = inner (โ†‘v) y) :
            x = y
            theorem Dense.eq_zero_of_inner_right {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} {x : E} (hK : Dense โ†‘K) (h : โˆ€ (v : โ†ฅK), inner (โ†‘v) x = 0) :
            x = 0
            theorem reflection_mem_subspace_orthogonal_precomplement_eq_neg {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {K : Submodule ๐•œ E} [HasOrthogonalProjection K] {v : E} (hv : v โˆˆ K) :

            The reflection in Kแ—ฎ of an element of K is its negation.

            theorem orthogonalProjection_orthogonalComplement_singleton_eq_zero {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] (v : E) :

            The orthogonal projection onto (๐•œ โˆ™ v)แ—ฎ of v is zero.

            theorem reflection_orthogonalComplement_singleton_eq_neg {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] (v : E) :
            (reflection (Submodule.span ๐•œ {v})แ—ฎ) v = -v

            The reflection in (๐•œ โˆ™ v)แ—ฎ of v is -v.

            theorem orthogonalProjection_add_orthogonalProjection_orthogonal {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] (K : Submodule ๐•œ E) [HasOrthogonalProjection K] (w : E) :
            โ†‘((orthogonalProjection K) w) + โ†‘((orthogonalProjection Kแ—ฎ) w) = w

            If the orthogonal projection to K is well-defined, then a vector splits as the sum of its orthogonal projections onto a complete submodule K and onto the orthogonal complement of K.

            The Pythagorean theorem, for an orthogonal projection.

            theorem id_eq_sum_orthogonalProjection_self_orthogonalComplement {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] (K : Submodule ๐•œ E) [HasOrthogonalProjection K] :
            ContinuousLinearMap.id ๐•œ E = K.subtypeL.comp (orthogonalProjection K) + Kแ—ฎ.subtypeL.comp (orthogonalProjection Kแ—ฎ)

            In a complete space E, the projection maps onto a complete subspace K and its orthogonal complement sum to the identity.

            @[simp]
            theorem inner_orthogonalProjection_eq_of_mem_right {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] (K : Submodule ๐•œ E) [HasOrthogonalProjection K] (u : โ†ฅK) (v : E) :
            inner ((orthogonalProjection K) v) u = inner v โ†‘u
            @[simp]
            theorem inner_orthogonalProjection_eq_of_mem_left {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] (K : Submodule ๐•œ E) [HasOrthogonalProjection K] (u : โ†ฅK) (v : E) :
            inner u ((orthogonalProjection K) v) = inner (โ†‘u) v
            theorem inner_orthogonalProjection_left_eq_right {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] (K : Submodule ๐•œ E) [HasOrthogonalProjection K] (u : E) (v : E) :
            inner (โ†‘((orthogonalProjection K) u)) v = inner u โ†‘((orthogonalProjection K) v)

            The orthogonal projection is self-adjoint.

            theorem orthogonalProjection_isSymmetric {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] (K : Submodule ๐•œ E) [HasOrthogonalProjection K] :
            (โ†‘(K.subtypeL.comp (orthogonalProjection K))).IsSymmetric

            The orthogonal projection is symmetric.

            theorem Submodule.finrank_add_inf_finrank_orthogonal {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {Kโ‚ : Submodule ๐•œ E} {Kโ‚‚ : Submodule ๐•œ E} [FiniteDimensional ๐•œ โ†ฅKโ‚‚] (h : Kโ‚ โ‰ค Kโ‚‚) :
            Module.finrank ๐•œ โ†ฅKโ‚ + Module.finrank ๐•œ โ†ฅ(Kโ‚แ—ฎ โŠ“ Kโ‚‚) = Module.finrank ๐•œ โ†ฅKโ‚‚

            Given a finite-dimensional subspace Kโ‚‚, and a subspace Kโ‚ contained in it, the dimensions of Kโ‚ and the intersection of its orthogonal subspace with Kโ‚‚ add to that of Kโ‚‚.

            theorem Submodule.finrank_add_inf_finrank_orthogonal' {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {Kโ‚ : Submodule ๐•œ E} {Kโ‚‚ : Submodule ๐•œ E} [FiniteDimensional ๐•œ โ†ฅKโ‚‚] (h : Kโ‚ โ‰ค Kโ‚‚) {n : โ„•} (h_dim : Module.finrank ๐•œ โ†ฅKโ‚ + n = Module.finrank ๐•œ โ†ฅKโ‚‚) :
            Module.finrank ๐•œ โ†ฅ(Kโ‚แ—ฎ โŠ“ Kโ‚‚) = n

            Given a finite-dimensional subspace Kโ‚‚, and a subspace Kโ‚ contained in it, the dimensions of Kโ‚ and the intersection of its orthogonal subspace with Kโ‚‚ add to that of Kโ‚‚.

            theorem Submodule.finrank_add_finrank_orthogonal {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] [FiniteDimensional ๐•œ E] (K : Submodule ๐•œ E) :
            Module.finrank ๐•œ โ†ฅK + Module.finrank ๐•œ โ†ฅKแ—ฎ = Module.finrank ๐•œ E

            Given a finite-dimensional space E and subspace K, the dimensions of K and Kแ—ฎ add to that of E.

            theorem Submodule.finrank_add_finrank_orthogonal' {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] [FiniteDimensional ๐•œ E] {K : Submodule ๐•œ E} {n : โ„•} (h_dim : Module.finrank ๐•œ โ†ฅK + n = Module.finrank ๐•œ E) :
            Module.finrank ๐•œ โ†ฅKแ—ฎ = n

            Given a finite-dimensional space E and subspace K, the dimensions of K and Kแ—ฎ add to that of E.

            theorem finrank_orthogonal_span_singleton {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {n : โ„•} [_i : Fact (Module.finrank ๐•œ E = n + 1)] {v : E} (hv : v โ‰  0) :
            Module.finrank ๐•œ โ†ฅ(Submodule.span ๐•œ {v})แ—ฎ = n

            In a finite-dimensional inner product space, the dimension of the orthogonal complement of the span of a nonzero vector is one less than the dimension of the space.

            theorem LinearIsometryEquiv.reflections_generate_dim_aux {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace โ„ F] [FiniteDimensional โ„ F] {n : โ„•} (ฯ† : F โ‰ƒโ‚—แตข[โ„] F) (hn : Module.finrank โ„ โ†ฅ(LinearMap.ker (ContinuousLinearMap.id โ„ F - โ†‘{ toLinearEquiv := ฯ†.toLinearEquiv, continuous_toFun := โ‹ฏ, continuous_invFun := โ‹ฏ }))แ—ฎ โ‰ค n) :
            โˆƒ (l : List F), l.length โ‰ค n โˆง ฯ† = (List.map (fun (v : F) => reflection (Submodule.span โ„ {v})แ—ฎ) l).prod

            An element ฯ† of the orthogonal group of F can be factored as a product of reflections, and specifically at most as many reflections as the dimension of the complement of the fixed subspace of ฯ†.

            The orthogonal group of F is generated by reflections; specifically each element ฯ† of the orthogonal group is a product of at most as many reflections as the dimension of F.

            Special case of the Cartanโ€“Dieudonnรฉ theorem.

            theorem OrthogonalFamily.isInternal_iff_of_isComplete {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_4} [DecidableEq ฮน] {V : ฮน โ†’ Submodule ๐•œ E} (hV : OrthogonalFamily ๐•œ (fun (i : ฮน) => โ†ฅ(V i)) fun (i : ฮน) => (V i).subtypeโ‚—แตข) (hc : IsComplete โ†‘(iSup V)) :

            An orthogonal family of subspaces of E satisfies DirectSum.IsInternal (that is, they provide an internal direct sum decomposition of E) if and only if their span has trivial orthogonal complement.

            theorem OrthogonalFamily.isInternal_iff {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_4} [DecidableEq ฮน] [FiniteDimensional ๐•œ E] {V : ฮน โ†’ Submodule ๐•œ E} (hV : OrthogonalFamily ๐•œ (fun (i : ฮน) => โ†ฅ(V i)) fun (i : ฮน) => (V i).subtypeโ‚—แตข) :

            An orthogonal family of subspaces of E satisfies DirectSum.IsInternal (that is, they provide an internal direct sum decomposition of E) if and only if their span has trivial orthogonal complement.

            theorem OrthogonalFamily.sum_projection_of_mem_iSup {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_4} [Fintype ฮน] {V : ฮน โ†’ Submodule ๐•œ E} [โˆ€ (i : ฮน), CompleteSpace โ†ฅ(V i)] (hV : OrthogonalFamily ๐•œ (fun (i : ฮน) => โ†ฅ(V i)) fun (i : ฮน) => (V i).subtypeโ‚—แตข) (x : E) (hx : x โˆˆ iSup V) :
            โˆ‘ i : ฮน, โ†‘((orthogonalProjection (V i)) x) = x

            If x lies within an orthogonal family v, it can be expressed as a sum of projections.

            theorem OrthogonalFamily.projection_directSum_coeAddHom {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_4} [DecidableEq ฮน] {V : ฮน โ†’ Submodule ๐•œ E} (hV : OrthogonalFamily ๐•œ (fun (i : ฮน) => โ†ฅ(V i)) fun (i : ฮน) => (V i).subtypeโ‚—แตข) (x : DirectSum ฮน fun (i : ฮน) => โ†ฅ(V i)) (i : ฮน) [CompleteSpace โ†ฅ(V i)] :

            If a family of submodules is orthogonal, then the orthogonalProjection on a direct sum is just the coefficient of that direct sum.

            @[reducible, inline]
            abbrev OrthogonalFamily.decomposition {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_4} [DecidableEq ฮน] [Fintype ฮน] {V : ฮน โ†’ Submodule ๐•œ E} [โˆ€ (i : ฮน), CompleteSpace โ†ฅ(V i)] (hV : OrthogonalFamily ๐•œ (fun (i : ฮน) => โ†ฅ(V i)) fun (i : ฮน) => (V i).subtypeโ‚—แตข) (h : iSup V = โŠค) :

            If a family of submodules is orthogonal and they span the whole space, then the orthogonal projection provides a means to decompose the space into its submodules.

            The projection function is decompose V x i = orthogonalProjection (V i) x.

            See note [reducible non-instances].

            Equations
            • hV.decomposition h = { decompose' := fun (x : E) => DFinsupp.equivFunOnFintype.symm fun (i : ฮน) => (orthogonalProjection (V i)) x, left_inv := โ‹ฏ, right_inv := โ‹ฏ }
            Instances For
              theorem maximal_orthonormal_iff_orthogonalComplement_eq_bot {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {v : Set E} (hv : Orthonormal ๐•œ Subtype.val) :
              (โˆ€ u โŠ‡ v, Orthonormal ๐•œ Subtype.val โ†’ u = v) โ†” (Submodule.span ๐•œ v)แ—ฎ = โŠฅ

              An orthonormal set in an InnerProductSpace is maximal, if and only if the orthogonal complement of its span is empty.

              theorem maximal_orthonormal_iff_basis_of_finiteDimensional {๐•œ : Type u_1} {E : Type u_2} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {v : Set E} [FiniteDimensional ๐•œ E] (hv : Orthonormal ๐•œ Subtype.val) :
              (โˆ€ u โŠ‡ v, Orthonormal ๐•œ Subtype.val โ†’ u = v) โ†” โˆƒ (b : Basis (โ†‘v) ๐•œ E), โ‡‘b = Subtype.val

              An orthonormal set in a finite-dimensional InnerProductSpace is maximal, if and only if it is a basis.