OAI/Analysis/Hyperinvariant/Transport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Hyperinvariant.norm_conjugate_le line 13
2. theorem OAI.Hyperinvariant.norm_conjugate line 21
3. theorem OAI.Hyperinvariant.transitiveCommutant_conjugate line 32

   Source documentation

   Hyperinvariance is transported through a genuine surjective complex-linear isometry.

   theorem transitiveCommutant_conjugate (e : H ≃ₗᵢ[ℂ] K) (T : H →L[ℂ] H)
       (hT : TransitiveCommutant T) : TransitiveCommutant (e.conjStarAlgEquiv T) := by
   …

   Mentions: OAI.Hyperinvariant.TransitiveCommutant

4. theorem OAI.Hyperinvariant.mainClaim_transport line 62

   Source documentation

   Nonzero and the exact norm-root limit are both preserved by unitary conjugation.

   theorem mainClaim_transport (e : H ≃ₗᵢ[ℂ] K) (h : MainClaim (H := H)) :
   …

   Mentions: OAI.Hyperinvariant.MainClaim