Documentation

Mathlib.Analysis.InnerProductSpace.Adjoint

Adjoint of operators on Hilbert spaces #

Given an operator A : E →L[𝕜] F, where E and F are Hilbert spaces, its adjoint adjoint A : F →L[𝕜] E is the unique operator such that ⟪x, A y⟫ = ⟪adjoint A x, y⟫ for all x and y.

We then use this to put a C⋆-algebra structure on E →L[𝕜] E with the adjoint as the star operation.

This construction is used to define an adjoint for linear maps (i.e. not continuous) between finite dimensional spaces.

Main definitions #

Implementation notes #

Tags #

adjoint

Adjoint operator #

noncomputable def ContinuousLinearMap.adjointAux {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] :
(E →L[𝕜] F) →L⋆[𝕜] F →L[𝕜] E

The adjoint, as a continuous conjugate-linear map. This is only meant as an auxiliary definition for the main definition adjoint, where this is bundled as a conjugate-linear isometric equivalence.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem ContinuousLinearMap.adjointAux_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] (A : E →L[𝕜] F) (x : F) :
    (ContinuousLinearMap.adjointAux A) x = (LinearIsometryEquiv.symm (InnerProductSpace.toDual 𝕜 E)) ((ContinuousLinearMap.toSesqForm A) x)
    theorem ContinuousLinearMap.adjointAux_inner_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] (A : E →L[𝕜] F) (x : E) (y : F) :
    (ContinuousLinearMap.adjointAux A) y, x⟫_𝕜 = y, A x⟫_𝕜
    theorem ContinuousLinearMap.adjointAux_inner_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] (A : E →L[𝕜] F) (x : E) (y : F) :
    x, (ContinuousLinearMap.adjointAux A) y⟫_𝕜 = A x, y⟫_𝕜
    theorem ContinuousLinearMap.adjointAux_adjointAux {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (A : E →L[𝕜] F) :
    ContinuousLinearMap.adjointAux (ContinuousLinearMap.adjointAux A) = A
    @[simp]
    theorem ContinuousLinearMap.adjointAux_norm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (A : E →L[𝕜] F) :
    ContinuousLinearMap.adjointAux A = A
    def ContinuousLinearMap.adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] :
    (E →L[𝕜] F) ≃ₗᵢ⋆[𝕜] F →L[𝕜] E

    The adjoint of a bounded operator from Hilbert space E to Hilbert space F.

    Equations
    Instances For
      theorem ContinuousLinearMap.adjoint_inner_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (A : E →L[𝕜] F) (x : E) (y : F) :
      (ContinuousLinearMap.adjoint A) y, x⟫_𝕜 = y, A x⟫_𝕜

      The fundamental property of the adjoint.

      theorem ContinuousLinearMap.adjoint_inner_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (A : E →L[𝕜] F) (x : E) (y : F) :
      x, (ContinuousLinearMap.adjoint A) y⟫_𝕜 = A x, y⟫_𝕜

      The fundamental property of the adjoint.

      @[simp]
      theorem ContinuousLinearMap.adjoint_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (A : E →L[𝕜] F) :
      ContinuousLinearMap.adjoint (ContinuousLinearMap.adjoint A) = A

      The adjoint is involutive.

      @[simp]
      theorem ContinuousLinearMap.adjoint_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [InnerProductSpace 𝕜 G] [CompleteSpace E] [CompleteSpace G] [CompleteSpace F] (A : F →L[𝕜] G) (B : E →L[𝕜] F) :
      ContinuousLinearMap.adjoint (ContinuousLinearMap.comp A B) = ContinuousLinearMap.comp (ContinuousLinearMap.adjoint B) (ContinuousLinearMap.adjoint A)

      The adjoint of the composition of two operators is the composition of the two adjoints in reverse order.

      theorem ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (A : E →L[𝕜] F) (x : E) :
      A x ^ 2 = RCLike.re (ContinuousLinearMap.comp (ContinuousLinearMap.adjoint A) A) x, x⟫_𝕜
      theorem ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (A : E →L[𝕜] F) (x : E) :
      A x = Real.sqrt (RCLike.re (ContinuousLinearMap.comp (ContinuousLinearMap.adjoint A) A) x, x⟫_𝕜)
      theorem ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (A : E →L[𝕜] F) (x : E) :
      A x ^ 2 = RCLike.re x, (ContinuousLinearMap.comp (ContinuousLinearMap.adjoint A) A) x⟫_𝕜
      theorem ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (A : E →L[𝕜] F) (x : E) :
      A x = Real.sqrt (RCLike.re x, (ContinuousLinearMap.comp (ContinuousLinearMap.adjoint A) A) x⟫_𝕜)
      theorem ContinuousLinearMap.eq_adjoint_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (A : E →L[𝕜] F) (B : F →L[𝕜] E) :
      A = ContinuousLinearMap.adjoint B ∀ (x : E) (y : F), A x, y⟫_𝕜 = x, B y⟫_𝕜

      The adjoint is unique: a map A is the adjoint of B iff it satisfies ⟪A x, y⟫ = ⟪x, B y⟫ for all x and y.

      @[simp]
      theorem ContinuousLinearMap.adjoint_id {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] :
      ContinuousLinearMap.adjoint (ContinuousLinearMap.id 𝕜 E) = ContinuousLinearMap.id 𝕜 E
      theorem Submodule.adjoint_subtypeL {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U : Submodule 𝕜 E) [CompleteSpace U] :
      ContinuousLinearMap.adjoint (Submodule.subtypeL U) = orthogonalProjection U
      theorem Submodule.adjoint_orthogonalProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U : Submodule 𝕜 E) [CompleteSpace U] :
      ContinuousLinearMap.adjoint (orthogonalProjection U) = Submodule.subtypeL U
      theorem ContinuousLinearMap.star_eq_adjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (A : E →L[𝕜] E) :
      star A = ContinuousLinearMap.adjoint A
      theorem ContinuousLinearMap.isSelfAdjoint_iff' {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {A : E →L[𝕜] E} :
      IsSelfAdjoint A ContinuousLinearMap.adjoint A = A

      A continuous linear operator is self-adjoint iff it is equal to its adjoint.

      theorem ContinuousLinearMap.norm_adjoint_comp_self {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (A : E →L[𝕜] F) :
      ContinuousLinearMap.comp (ContinuousLinearMap.adjoint A) A = A * A
      theorem ContinuousLinearMap.isAdjointPair_inner {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (A : E →L[𝕜] F) :
      LinearMap.IsAdjointPair sesqFormOfInner sesqFormOfInner A (ContinuousLinearMap.adjoint A)

      Self-adjoint operators #

      theorem IsSelfAdjoint.adjoint_eq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {A : E →L[𝕜] E} (hA : IsSelfAdjoint A) :
      ContinuousLinearMap.adjoint A = A
      theorem IsSelfAdjoint.isSymmetric {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {A : E →L[𝕜] E} (hA : IsSelfAdjoint A) :

      Every self-adjoint operator on an inner product space is symmetric.

      theorem IsSelfAdjoint.conj_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] {T : E →L[𝕜] E} (hT : IsSelfAdjoint T) (S : E →L[𝕜] F) :
      IsSelfAdjoint (ContinuousLinearMap.comp S (ContinuousLinearMap.comp T (ContinuousLinearMap.adjoint S)))

      Conjugating preserves self-adjointness.

      theorem IsSelfAdjoint.adjoint_conj {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] {T : E →L[𝕜] E} (hT : IsSelfAdjoint T) (S : F →L[𝕜] E) :
      IsSelfAdjoint (ContinuousLinearMap.comp (ContinuousLinearMap.adjoint S) (ContinuousLinearMap.comp T S))

      Conjugating preserves self-adjointness.

      The orthogonal projection is self-adjoint.

      def LinearMap.IsSymmetric.toSelfAdjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →ₗ[𝕜] E} (hT : LinearMap.IsSymmetric T) :
      (selfAdjoint (E →L[𝕜] E))

      The Hellinger--Toeplitz theorem: Construct a self-adjoint operator from an everywhere defined symmetric operator.

      Equations
      Instances For
        def LinearMap.adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] :
        (E →ₗ[𝕜] F) ≃ₗ⋆[𝕜] F →ₗ[𝕜] E

        The adjoint of an operator from the finite-dimensional inner product space E to the finite-dimensional inner product space F.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          theorem LinearMap.adjoint_toContinuousLinearMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) :
          LinearMap.toContinuousLinearMap (LinearMap.adjoint A) = ContinuousLinearMap.adjoint (LinearMap.toContinuousLinearMap A)
          theorem LinearMap.adjoint_eq_toCLM_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) :
          LinearMap.adjoint A = (ContinuousLinearMap.adjoint (LinearMap.toContinuousLinearMap A))
          theorem LinearMap.adjoint_inner_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (x : E) (y : F) :
          (LinearMap.adjoint A) y, x⟫_𝕜 = y, A x⟫_𝕜

          The fundamental property of the adjoint.

          theorem LinearMap.adjoint_inner_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (x : E) (y : F) :
          x, (LinearMap.adjoint A) y⟫_𝕜 = A x, y⟫_𝕜

          The fundamental property of the adjoint.

          @[simp]
          theorem LinearMap.adjoint_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) :
          LinearMap.adjoint (LinearMap.adjoint A) = A

          The adjoint is involutive.

          @[simp]
          theorem LinearMap.adjoint_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [InnerProductSpace 𝕜 G] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] [FiniteDimensional 𝕜 G] (A : F →ₗ[𝕜] G) (B : E →ₗ[𝕜] F) :
          LinearMap.adjoint (A ∘ₗ B) = LinearMap.adjoint B ∘ₗ LinearMap.adjoint A

          The adjoint of the composition of two operators is the composition of the two adjoints in reverse order.

          theorem LinearMap.eq_adjoint_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (B : F →ₗ[𝕜] E) :
          A = LinearMap.adjoint B ∀ (x : E) (y : F), A x, y⟫_𝕜 = x, B y⟫_𝕜

          The adjoint is unique: a map A is the adjoint of B iff it satisfies ⟪A x, y⟫ = ⟪x, B y⟫ for all x and y.

          theorem LinearMap.eq_adjoint_iff_basis {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {ι₁ : Type u_5} {ι₂ : Type u_6} (b₁ : Basis ι₁ 𝕜 E) (b₂ : Basis ι₂ 𝕜 F) (A : E →ₗ[𝕜] F) (B : F →ₗ[𝕜] E) :
          A = LinearMap.adjoint B ∀ (i₁ : ι₁) (i₂ : ι₂), A (b₁ i₁), b₂ i₂⟫_𝕜 = b₁ i₁, B (b₂ i₂)⟫_𝕜

          The adjoint is unique: a map A is the adjoint of B iff it satisfies ⟪A x, y⟫ = ⟪x, B y⟫ for all basis vectors x and y.

          theorem LinearMap.eq_adjoint_iff_basis_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {ι : Type u_5} (b : Basis ι 𝕜 E) (A : E →ₗ[𝕜] F) (B : F →ₗ[𝕜] E) :
          A = LinearMap.adjoint B ∀ (i : ι) (y : F), A (b i), y⟫_𝕜 = b i, B y⟫_𝕜
          theorem LinearMap.eq_adjoint_iff_basis_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {ι : Type u_5} (b : Basis ι 𝕜 F) (A : E →ₗ[𝕜] F) (B : F →ₗ[𝕜] E) :
          A = LinearMap.adjoint B ∀ (i : ι) (x : E), A x, b i⟫_𝕜 = x, B (b i)⟫_𝕜

          E →ₗ[𝕜] E is a star algebra with the adjoint as the star operation.

          Equations
          • One or more equations did not get rendered due to their size.
          theorem LinearMap.star_eq_adjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (A : E →ₗ[𝕜] E) :
          star A = LinearMap.adjoint A
          theorem LinearMap.isSelfAdjoint_iff' {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {A : E →ₗ[𝕜] E} :
          IsSelfAdjoint A LinearMap.adjoint A = A

          A continuous linear operator is self-adjoint iff it is equal to its adjoint.

          theorem LinearMap.isAdjointPair_inner {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) :
          LinearMap.IsAdjointPair sesqFormOfInner sesqFormOfInner A (LinearMap.adjoint A)
          theorem LinearMap.isSymmetric_adjoint_mul_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) :
          LinearMap.IsSymmetric (LinearMap.adjoint T * T)

          The Gram operator T†T is symmetric.

          theorem LinearMap.re_inner_adjoint_mul_self_nonneg {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) (x : E) :
          0 RCLike.re x, (LinearMap.adjoint T * T) x⟫_𝕜

          The Gram operator T†T is a positive operator.

          @[simp]
          theorem LinearMap.im_inner_adjoint_mul_self_eq_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) (x : E) :
          RCLike.im x, (LinearMap.adjoint T) (T x)⟫_𝕜 = 0
          theorem ContinuousLinearMap.inner_map_map_iff_adjoint_comp_self {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] {K : Type u_6} [NormedAddCommGroup K] [InnerProductSpace 𝕜 K] [CompleteSpace K] (u : H →L[𝕜] K) :
          (∀ (x y : H), u x, u y⟫_𝕜 = x, y⟫_𝕜) ContinuousLinearMap.comp (ContinuousLinearMap.adjoint u) u = 1
          theorem ContinuousLinearMap.norm_map_iff_adjoint_comp_self {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] {K : Type u_6} [NormedAddCommGroup K] [InnerProductSpace 𝕜 K] [CompleteSpace K] (u : H →L[𝕜] K) :
          (∀ (x : H), u x = x) ContinuousLinearMap.comp (ContinuousLinearMap.adjoint u) u = 1
          @[simp]
          theorem LinearIsometryEquiv.adjoint_eq_symm {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] {K : Type u_6} [NormedAddCommGroup K] [InnerProductSpace 𝕜 K] [CompleteSpace K] (e : H ≃ₗᵢ[𝕜] K) :
          ContinuousLinearMap.adjoint { toLinearEquiv := e.toLinearEquiv, continuous_toFun := , continuous_invFun := } = { toLinearEquiv := (LinearIsometryEquiv.symm e).toLinearEquiv, continuous_toFun := , continuous_invFun := }
          @[simp]
          theorem LinearIsometryEquiv.star_eq_symm {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] (e : H ≃ₗᵢ[𝕜] H) :
          star { toLinearEquiv := e.toLinearEquiv, continuous_toFun := , continuous_invFun := } = { toLinearEquiv := (LinearIsometryEquiv.symm e).toLinearEquiv, continuous_toFun := , continuous_invFun := }
          theorem ContinuousLinearMap.norm_map_of_mem_unitary {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] {u : H →L[𝕜] H} (hu : u unitary (H →L[𝕜] H)) (x : H) :
          theorem ContinuousLinearMap.inner_map_map_of_mem_unitary {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] {u : H →L[𝕜] H} (hu : u unitary (H →L[𝕜] H)) (x : H) (y : H) :
          u x, u y⟫_𝕜 = x, y⟫_𝕜
          theorem unitary.norm_map {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] (u : (unitary (H →L[𝕜] H))) (x : H) :
          u x = x
          theorem unitary.inner_map_map {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] (u : (unitary (H →L[𝕜] H))) (x : H) (y : H) :
          u x, u y⟫_𝕜 = x, y⟫_𝕜
          noncomputable def unitary.linearIsometryEquiv {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] :
          (unitary (H →L[𝕜] H)) ≃* (H ≃ₗᵢ[𝕜] H)

          The unitary elements of continuous linear maps on a Hilbert space coincide with the linear isometric equivalences on that Hilbert space.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem unitary.linearIsometryEquiv_coe_apply {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] (u : (unitary (H →L[𝕜] H))) :
            { toLinearEquiv := (unitary.linearIsometryEquiv u).toLinearEquiv, continuous_toFun := , continuous_invFun := } = u
            @[simp]
            theorem unitary.linearIsometryEquiv_coe_symm_apply {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] (e : H ≃ₗᵢ[𝕜] H) :
            ((MulEquiv.symm unitary.linearIsometryEquiv) e) = { toLinearEquiv := e.toLinearEquiv, continuous_toFun := , continuous_invFun := }
            theorem Matrix.toLin_conjTranspose {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] {m : Type u_5} {n : Type u_6} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (v₁ : OrthonormalBasis n 𝕜 E) (v₂ : OrthonormalBasis m 𝕜 F) (A : Matrix m n 𝕜) :

            The linear map associated to the conjugate transpose of a matrix corresponding to two orthonormal bases is the adjoint of the linear map associated to the matrix.

            theorem LinearMap.toMatrix_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] {m : Type u_5} {n : Type u_6} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (v₁ : OrthonormalBasis n 𝕜 E) (v₂ : OrthonormalBasis m 𝕜 F) (f : E →ₗ[𝕜] F) :

            The matrix associated to the adjoint of a linear map corresponding to two orthonormal bases is the conjugate tranpose of the matrix associated to the linear map.

            @[simp]
            theorem LinearMap.toMatrixOrthonormal_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : Type u_6} [Fintype n] [DecidableEq n] [FiniteDimensional 𝕜 E] (v₁ : OrthonormalBasis n 𝕜 E) :
            def LinearMap.toMatrixOrthonormal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : Type u_6} [Fintype n] [DecidableEq n] [FiniteDimensional 𝕜 E] (v₁ : OrthonormalBasis n 𝕜 E) :
            (E →ₗ[𝕜] E) ≃⋆ₐ[𝕜] Matrix n n 𝕜

            The star algebra equivalence between the linear endomorphisms of finite-dimensional inner product space and square matrices induced by the choice of an orthonormal basis.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              theorem Matrix.toEuclideanLin_conjTranspose_eq_adjoint {𝕜 : Type u_1} [RCLike 𝕜] {m : Type u_5} {n : Type u_6} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (A : Matrix m n 𝕜) :
              Matrix.toEuclideanLin (Matrix.conjTranspose A) = LinearMap.adjoint (Matrix.toEuclideanLin A)

              The adjoint of the linear map associated to a matrix is the linear map associated to the conjugate transpose of that matrix.