proposition A.591 Any two irreducible Weyl systems are equivalent

Rests on

• depends_on lemma A.590 The Gram matrix is universal ¶
  • depends_on lemma A.581 Composition law ¶
    • depends_on definition A.580 Weyl operator ¶
      • depends_on definition 12.64 Strongly continuous one-parameter unitary group ¶
        • depends_on definition 12.41 The operator classes ¶
        • depends_on definition 6.6 Continuous map ¶
      • depends_on definition 12.109 Weyl system ¶
        • depends_on definition 12.64 Strongly continuous one-parameter unitary group ¶ ↺
        • depends_on theorem 12.75 The canonical commutation relation admits no bounded solution ¶
        • depends_on theorem 12.66 Stone ¶
      • depends_on equation 12.71 eq:hilbert-weyl-relation ¶
    • depends_on definition 12.64 Strongly continuous one-parameter unitary group ¶ ↺
    • depends_on equation 12.71 eq:hilbert-weyl-relation ¶ ↺
    • proves proof app:A-long-proofs@proof-347 ¶
  • depends_on proposition A.589 Cyclic subspaces and the rank of the average ¶
    • depends_on definition 12.90 Self-adjoint family; commutant; irreducibility ¶
      • depends_on definition 12.41 The operator classes ¶ ↺
      • depends_on definition 12.88 Reducing subspace ¶
        • depends_on definition 12.35 Bounded operator; operator norm ¶
        • depends_on definition 12.20 Orthogonal projection operator ¶
    • depends_on proposition 12.89 Reduction is commutation ¶
      • depends_on definition 12.88 Reducing subspace ¶ ↺
      • depends_on proposition 12.21 Characterization of orthogonal projections ¶
        • depends_on definition 12.20 Orthogonal projection operator ¶ ↺
        • depends_on theorem 12.18 Projection theorem ¶
        • proves proof ch:10-hilbert-spaces@proof-11 ¶
      • proves proof ch:10-hilbert-spaces@proof-43 ¶
    • depends_on theorem A.587 The Gaussian average is a non-zero projector that absorbs the Weyl operators ¶
      • depends_on definition A.585 The Gaussian average of the Weyl operators ¶
        • depends_on definition A.580 Weyl operator ¶ ↺
        • depends_on lemma A.583 Absolutely convergent operator-valued integrals ¶
      • depends_on lemma A.584 Fourier injectivity in $n$ variables ¶
        • depends_on definition 17.29 Fourier transform; the treatise convention ¶
        • depends_on equation 17.42 eq:ft-gaussian ¶
        • depends_on theorem 17.32 Fourier inversion ¶
        • proves proof app:A-long-proofs@proof-350 ¶
      • depends_on lemma A.586 Gaussian integral with a complex linear term ¶
        • depends_on equation 7.151 eq:ana-iterated ¶
        • depends_on equation 17.42 eq:ft-gaussian ¶ ↺
        • depends_on equation 17.35 eq:ft-translation ¶
        • proves proof app:A-long-proofs@proof-351 ¶
      • proves proof app:A-long-proofs@proof-352 ¶
    • proves proof app:A-long-proofs@proof-353 ¶
  • depends_on theorem A.587 The Gaussian average is a non-zero projector that absorbs the Weyl operators ¶ ↺
  • proves proof app:A-long-proofs@proof-354 ¶
• depends_on proposition A.589 Cyclic subspaces and the rank of the average ¶ ↺
• depends_on theorem 12.91 Schur's lemma, commutant form ¶
  • depends_on definition 12.90 Self-adjoint family; commutant; irreducibility ¶ ↺
  • depends_on proposition 12.89 Reduction is commutation ¶ ↺
  • depends_on theorem 12.59 Spectral theorem for a bounded self-adjoint operator ¶
    • depends_on definition 12.58 Projection-valued measure ¶
      • depends_on definition 12.41 The operator classes ¶ ↺
      • depends_on proposition 12.21 Characterization of orthogonal projections ¶ ↺
    • depends_on proposition 12.43 Norm of a self-adjoint operator ¶
      • depends_on proposition 12.42 Elementary consequences ¶
        • depends_on definition 12.41 The operator classes ¶ ↺
        • depends_on proposition 12.39 Algebra of the adjoint; the $C^{\ast}$ identity ¶
        • proves proof ch:10-hilbert-spaces@proof-22 ¶
      • depends_on proposition 12.39 Algebra of the adjoint; the $C^{\ast}$ identity ¶ ↺
      • proves proof ch:10-hilbert-spaces@proof-23 ¶
    • depends_on theorem 12.55 The spectrum of a self-adjoint operator is real ¶
      • depends_on corollary 12.19 Double complement; the density criterion ¶
        • depends_on proposition 12.17 The complement is always a closed subspace ¶
        • depends_on theorem 12.18 Projection theorem ¶ ↺
        • proves proof ch:10-hilbert-spaces@proof-10 ¶
      • depends_on definition 12.41 The operator classes ¶ ↺
      • depends_on theorem 12.54 The spectrum is compact and non-empty ¶
        • depends_on proposition 12.52 Neumann series; the spectrum is bounded ¶
        • depends_on proposition 12.53 The resolvent set is open, the resolvent analytic ¶
        • depends_on theorem 8.18 Liouville ¶
        • proves proof ch:10-hilbert-spaces@proof-29 ¶
      • proves proof ch:10-hilbert-spaces@proof-30 ¶
    • proves proof ch:10-hilbert-spaces@prooflink-2 ¶
  • proves proof ch:10-hilbert-spaces@proof-44 ¶
• proves proof app:A-long-proofs@proof-355 ¶

Supports

Nothing declares a dependency on this node yet.