OAI/Analysis/Unitarizability/InvariantProjection.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A unitarizing similarity gives a bounded commuting projection onto every closed invariant subspace.

  1. theorem OAI.Dixmier.InvariantProjection.rep_inv line 15
  2. theorem OAI.Dixmier.InvariantProjection.orthogonal_projection_commutes line 19
  3. def OAI.Dixmier.InvariantProjection.conjugated line 36
  4. theorem OAI.Dixmier.InvariantProjection.conjugated_apply line 42
  5. theorem OAI.Dixmier.InvariantProjection.exists_commuting_projection line 47

    Source documentation

    The conclusion supplies one bounded projection; it assumes only the actual similarity and closed invariance, not a cocycle implementer.

    theorem exists_commuting_projection (π : G →* (H →L[ℂ] H))
    (hπ : SimilarToUnitary π) (M : ClosedSubmodule ℂ H)
    (hM : ∀ g x, x ∈ M → π g x ∈ M) :
    ∃ P : H →L[ℂ] H, (∀ x, P x ∈ M) ∧
      (∀ x, x ∈ M → P x = x) ∧ ∀ g, Commute P (π g) := by
…

    Mentions: OAI.Dixmier.SimilarToUnitary