Transport of Hilbert-space range projections

This module records the operator algebra transporting I I† through linear isometric equivalences. It also specializes the result to an operator pulled back along an equivalence.

theorem LiebThirring.projection_conj_eq_of_intertwining {E : Type u_1} {H : Type u_2} {Y : Type u_3} {X : Type u_4} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup Y] [InnerProductSpace ℂ Y] [CompleteSpace Y] [NormedAddCommGroup X] [InnerProductSpace ℂ X] [CompleteSpace X] (C : E ≃ₗᵢ[ℂ] Y) (R : H ≃ₗᵢ[ℂ] X) (I : H →L[ℂ] E) (A : X →L[ℂ] Y) (h : ↑↑C ∘SL I = A ∘SL ↑↑R) : ↑↑C ∘SL (I ∘SL ContinuousLinearMap.adjoint I) ∘SL ContinuousLinearMap.adjoint ↑↑C = A ∘SL ContinuousLinearMap.adjoint A

theorem LiebThirring.projection_transport_apply {E : Type u_1} {H : Type u_2} {Y : Type u_3} {X : Type u_4} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup Y] [InnerProductSpace ℂ Y] [CompleteSpace Y] [NormedAddCommGroup X] [InnerProductSpace ℂ X] [CompleteSpace X] (C : E ≃ₗᵢ[ℂ] Y) (R : H ≃ₗᵢ[ℂ] X) (I : H →L[ℂ] E) (A : X →L[ℂ] Y) (h : ↑↑C ∘SL I = A ∘SL ↑↑R) (ψ : E) : ↑↑C ((I ∘SL ContinuousLinearMap.adjoint I) ψ) = (A ∘SL ContinuousLinearMap.adjoint A) (↑↑C ψ)

theorem LiebThirring.projection_symm_comp {E : Type u_1} {H : Type u_2} {Y : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup Y] [InnerProductSpace ℂ Y] [CompleteSpace Y] (C : E ≃ₗᵢ[ℂ] Y) (D : H →L[ℂ] Y) : (↑↑C.symm ∘SL D) ∘SL ContinuousLinearMap.adjoint (↑↑C.symm ∘SL D) = ↑↑C.symm ∘SL (D ∘SL ContinuousLinearMap.adjoint D) ∘SL ↑↑C

theorem LiebThirring.projection_conj_symm_comp {E : Type u_1} {H : Type u_2} {Y : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup Y] [InnerProductSpace ℂ Y] [CompleteSpace Y] (C : E ≃ₗᵢ[ℂ] Y) (D : H →L[ℂ] Y) : ↑↑C ∘SL ((↑↑C.symm ∘SL D) ∘SL ContinuousLinearMap.adjoint (↑↑C.symm ∘SL D)) ∘SL ContinuousLinearMap.adjoint ↑↑C = D ∘SL ContinuousLinearMap.adjoint D

theorem LiebThirring.projection_pullback_apply {E : Type u_1} {H : Type u_2} {Y : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup Y] [InnerProductSpace ℂ Y] [CompleteSpace Y] (C : E ≃ₗᵢ[ℂ] Y) (D : H →L[ℂ] Y) (ψ : E) : ↑↑C (((↑↑C.symm ∘SL D) ∘SL ContinuousLinearMap.adjoint (↑↑C.symm ∘SL D)) ψ) = (D ∘SL ContinuousLinearMap.adjoint D) (↑↑C ψ)