Documentation

Mathlib.Analysis.InnerProductSpace.Orthogonal

Orthogonal complements of submodules #

In this file, the orthogonal complement of a submodule K is defined, and basic API established. Some of the more subtle results about the orthogonal complement are delayed to Analysis.InnerProductSpace.Projection.

See also BilinForm.orthogonal for orthogonality with respect to a general bilinear form.

Notation #

The orthogonal complement of a submodule K is denoted by Kᗮ.

The proposition that two submodules are orthogonal, Submodule.IsOrtho, is denoted by U ⟂ V. Note this is not the same unicode symbol as (Bot).

def Submodule.orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) :
Submodule 𝕜 E

The subspace of vectors orthogonal to a given subspace.

Equations
  • K = { carrier := {v : E | uK, inner u v = 0}, add_mem' := , zero_mem' := , smul_mem' := }
Instances For

    The subspace of vectors orthogonal to a given subspace.

    Equations
    Instances For
      theorem Submodule.mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) (v : E) :
      v K uK, inner u v = 0

      When a vector is in Kᗮ.

      theorem Submodule.mem_orthogonal' {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) (v : E) :
      v K uK, inner v u = 0

      When a vector is in Kᗮ, with the inner product the other way round.

      theorem Submodule.inner_right_of_mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} {u : E} {v : E} (hu : u K) (hv : v K) :
      inner u v = 0

      A vector in K is orthogonal to one in Kᗮ.

      theorem Submodule.inner_left_of_mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} {u : E} {v : E} (hu : u K) (hv : v K) :
      inner v u = 0

      A vector in Kᗮ is orthogonal to one in K.

      theorem Submodule.mem_orthogonal_singleton_iff_inner_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {u : E} {v : E} :
      v (Submodule.span 𝕜 {u}) inner u v = 0

      A vector is in (𝕜 ∙ u)ᗮ iff it is orthogonal to u.

      theorem Submodule.mem_orthogonal_singleton_iff_inner_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {u : E} {v : E} :
      v (Submodule.span 𝕜 {u}) inner v u = 0

      A vector in (𝕜 ∙ u)ᗮ is orthogonal to u.

      theorem Submodule.sub_mem_orthogonal_of_inner_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} {x : E} {y : E} (h : ∀ (v : K), inner x v = inner y v) :
      x - y K
      theorem Submodule.sub_mem_orthogonal_of_inner_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} {x : E} {y : E} (h : ∀ (v : K), inner (↑v) x = inner (↑v) y) :
      x - y K
      theorem Submodule.inf_orthogonal_eq_bot {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) :

      K and Kᗮ have trivial intersection.

      theorem Submodule.orthogonal_disjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) :

      K and Kᗮ have trivial intersection.

      theorem Submodule.orthogonal_eq_inter {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) :
      K = ⨅ (v : K), LinearMap.ker ((innerSL 𝕜) v)

      Kᗮ can be characterized as the intersection of the kernels of the operations of inner product with each of the elements of K.

      theorem Submodule.isClosed_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) :

      The orthogonal complement of any submodule K is closed.

      instance Submodule.instOrthogonalCompleteSpace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [CompleteSpace E] :

      In a complete space, the orthogonal complement of any submodule K is complete.

      Equations
      • =
      theorem Submodule.orthogonal_gc (𝕜 : Type u_1) (E : Type u_2) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] :
      GaloisConnection Submodule.orthogonal Submodule.orthogonal

      orthogonal gives a GaloisConnection between Submodule 𝕜 E and its OrderDual.

      theorem Submodule.orthogonal_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K₁ : Submodule 𝕜 E} {K₂ : Submodule 𝕜 E} (h : K₁ K₂) :
      K₂ K₁

      orthogonal reverses the ordering of two subspaces.

      theorem Submodule.orthogonal_orthogonal_monotone {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K₁ : Submodule 𝕜 E} {K₂ : Submodule 𝕜 E} (h : K₁ K₂) :
      K₁ K₂

      orthogonal.orthogonal preserves the ordering of two subspaces.

      theorem Submodule.le_orthogonal_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) :

      K is contained in Kᗮᗮ.

      theorem Submodule.inf_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K₁ : Submodule 𝕜 E) (K₂ : Submodule 𝕜 E) :
      K₁ K₂ = (K₁ K₂)

      The inf of two orthogonal subspaces equals the subspace orthogonal to the sup.

      theorem Submodule.iInf_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} (K : ιSubmodule 𝕜 E) :
      ⨅ (i : ι), (K i) = (iSup K)

      The inf of an indexed family of orthogonal subspaces equals the subspace orthogonal to the sup.

      theorem Submodule.sInf_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (s : Set (Submodule 𝕜 E)) :
      Ks, K = (sSup s)

      The inf of a set of orthogonal subspaces equals the subspace orthogonal to the sup.

      @[simp]
      theorem Submodule.top_orthogonal_eq_bot {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] :
      @[simp]
      theorem Submodule.bot_orthogonal_eq_top {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] :
      @[simp]
      theorem Submodule.orthogonal_eq_top_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) :
      theorem Submodule.orthogonalFamily_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) :
      OrthogonalFamily 𝕜 (fun (b : Bool) => (bif b then K else K)) fun (b : Bool) => (bif b then K else K).subtypeₗᵢ
      @[simp]
      theorem bilinFormOfRealInner_orthogonal {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace E] (K : Submodule E) :
      K.orthogonalBilin bilinFormOfRealInner = K

      Orthogonality of submodules #

      In this section we define Submodule.IsOrtho U V, with notation U ⟂ V.

      The API roughly matches that of Disjoint.

      def Submodule.IsOrtho {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) (V : Submodule 𝕜 E) :

      The proposition that two submodules are orthogonal. Has notation U ⟂ V.

      Equations
      Instances For

        The proposition that two submodules are orthogonal. Has notation U ⟂ V.

        Equations
        Instances For
          theorem Submodule.isOrtho_iff_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} {V : Submodule 𝕜 E} :
          U V U V
          theorem Submodule.IsOrtho.symm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} {V : Submodule 𝕜 E} (h : U V) :
          V U
          theorem Submodule.isOrtho_comm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} {V : Submodule 𝕜 E} :
          U V V U
          theorem Submodule.symmetric_isOrtho {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] :
          Symmetric Submodule.IsOrtho
          theorem Submodule.IsOrtho.inner_eq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} {V : Submodule 𝕜 E} (h : U V) {u : E} {v : E} (hu : u U) (hv : v V) :
          inner u v = 0
          theorem Submodule.isOrtho_iff_inner_eq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} {V : Submodule 𝕜 E} :
          U V uU, vV, inner u v = 0
          @[simp]
          theorem Submodule.isOrtho_bot_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {V : Submodule 𝕜 E} :
          @[simp]
          theorem Submodule.isOrtho_bot_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} :
          theorem Submodule.IsOrtho.mono_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U₁ : Submodule 𝕜 E} {U₂ : Submodule 𝕜 E} {V : Submodule 𝕜 E} (hU : U₂ U₁) (h : U₁ V) :
          U₂ V
          theorem Submodule.IsOrtho.mono_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} {V₁ : Submodule 𝕜 E} {V₂ : Submodule 𝕜 E} (hV : V₂ V₁) (h : U V₁) :
          U V₂
          theorem Submodule.IsOrtho.mono {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U₁ : Submodule 𝕜 E} {V₁ : Submodule 𝕜 E} {U₂ : Submodule 𝕜 E} {V₂ : Submodule 𝕜 E} (hU : U₂ U₁) (hV : V₂ V₁) (h : U₁ V₁) :
          U₂ V₂
          @[simp]
          theorem Submodule.isOrtho_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} :
          U U U =
          @[simp]
          theorem Submodule.isOrtho_orthogonal_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) :
          U U
          @[simp]
          theorem Submodule.isOrtho_orthogonal_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) :
          U U
          theorem Submodule.IsOrtho.le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} {V : Submodule 𝕜 E} (h : U V) :
          U V
          theorem Submodule.IsOrtho.ge {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} {V : Submodule 𝕜 E} (h : U V) :
          V U
          @[simp]
          theorem Submodule.isOrtho_top_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} :
          @[simp]
          theorem Submodule.isOrtho_top_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {V : Submodule 𝕜 E} :
          theorem Submodule.IsOrtho.disjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} {V : Submodule 𝕜 E} (h : U V) :

          Orthogonal submodules are disjoint.

          @[simp]
          theorem Submodule.isOrtho_sup_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U₁ : Submodule 𝕜 E} {U₂ : Submodule 𝕜 E} {V : Submodule 𝕜 E} :
          U₁ U₂ V U₁ V U₂ V
          @[simp]
          theorem Submodule.isOrtho_sup_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} {V₁ : Submodule 𝕜 E} {V₂ : Submodule 𝕜 E} :
          U V₁ V₂ U V₁ U V₂
          @[simp]
          theorem Submodule.isOrtho_sSup_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Set (Submodule 𝕜 E)} {V : Submodule 𝕜 E} :
          sSup U V UᵢU, Uᵢ V
          @[simp]
          theorem Submodule.isOrtho_sSup_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} {V : Set (Submodule 𝕜 E)} :
          U sSup V VᵢV, U Vᵢ
          @[simp]
          theorem Submodule.isOrtho_iSup_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Sort u_4} {U : ιSubmodule 𝕜 E} {V : Submodule 𝕜 E} :
          iSup U V ∀ (i : ι), U i V
          @[simp]
          theorem Submodule.isOrtho_iSup_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Sort u_4} {U : Submodule 𝕜 E} {V : ιSubmodule 𝕜 E} :
          U iSup V ∀ (i : ι), U V i
          @[simp]
          theorem Submodule.isOrtho_span {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {s : Set E} {t : Set E} :
          Submodule.span 𝕜 s Submodule.span 𝕜 t ∀ ⦃u : E⦄, u s∀ ⦃v : E⦄, v tinner u v = 0
          theorem Submodule.IsOrtho.map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (f : E →ₗᵢ[𝕜] F) {U : Submodule 𝕜 E} {V : Submodule 𝕜 E} (h : U V) :
          theorem Submodule.IsOrtho.comap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (f : E →ₗᵢ[𝕜] F) {U : Submodule 𝕜 F} {V : Submodule 𝕜 F} (h : U V) :
          @[simp]
          theorem Submodule.IsOrtho.map_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (f : E ≃ₗᵢ[𝕜] F) {U : Submodule 𝕜 E} {V : Submodule 𝕜 E} :
          @[simp]
          theorem Submodule.IsOrtho.comap_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (f : E ≃ₗᵢ[𝕜] F) {U : Submodule 𝕜 F} {V : Submodule 𝕜 F} :
          theorem orthogonalFamily_iff_pairwise {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {V : ιSubmodule 𝕜 E} :
          (OrthogonalFamily 𝕜 (fun (i : ι) => (V i)) fun (i : ι) => (V i).subtypeₗᵢ) Pairwise ((fun (x1 x2 : Submodule 𝕜 E) => x1 x2) on V)
          theorem OrthogonalFamily.pairwise {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {V : ιSubmodule 𝕜 E} :
          (OrthogonalFamily 𝕜 (fun (i : ι) => (V i)) fun (i : ι) => (V i).subtypeₗᵢ)Pairwise ((fun (x1 x2 : Submodule 𝕜 E) => x1 x2) on V)

          Alias of the forward direction of orthogonalFamily_iff_pairwise.

          theorem OrthogonalFamily.of_pairwise {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {V : ιSubmodule 𝕜 E} :
          Pairwise ((fun (x1 x2 : Submodule 𝕜 E) => x1 x2) on V)OrthogonalFamily 𝕜 (fun (i : ι) => (V i)) fun (i : ι) => (V i).subtypeₗᵢ

          Alias of the reverse direction of orthogonalFamily_iff_pairwise.

          theorem OrthogonalFamily.isOrtho {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {V : ιSubmodule 𝕜 E} (hV : OrthogonalFamily 𝕜 (fun (i : ι) => (V i)) fun (i : ι) => (V i).subtypeₗᵢ) {i : ι} {j : ι} (hij : i j) :
          V i V j

          Two submodules in an orthogonal family with different indices are orthogonal.