proposition A.263 The two constructions are inverse

Rests on

• depends_on proposition A.259 The generator is self-adjoint ¶
  • depends_on proposition A.258 The generator is closed ¶
    • depends_on equation A.470 eq:app-stone-domain ¶
    • depends_on lemma A.257 Integrated form of the equation of motion ¶
      • depends_on lemma A.254 Riemann integral of a continuous curve ¶
        • depends_on definition 12.2 Hilbert space ¶
        • depends_on proposition 12.4 Cauchy–Schwarz and continuity of the inner product ¶
        • proves proof app:A-long-proofs@proof-157 ¶
      • depends_on proposition 12.67 The generator is symmetric, and generates the motion ¶
        • depends_on definition 12.64 Strongly continuous one-parameter unitary group ¶
        • depends_on theorem 12.66 Stone ¶
        • proves proof ch:10-hilbert-spaces@proof-34 ¶
      • proves proof app:A-long-proofs@proof-160 ¶
    • proves proof app:A-long-proofs@proof-161 ¶
  • depends_on proposition A.256 Density ¶
    • depends_on definition 12.64 Strongly continuous one-parameter unitary group ¶ ↺
    • depends_on lemma A.255 Smoothed vectors lie in the domain ¶
      • depends_on definition 12.64 Strongly continuous one-parameter unitary group ¶ ↺
      • depends_on equation A.470 eq:app-stone-domain ¶ ↺
      • depends_on lemma A.254 Riemann integral of a continuous curve ¶ ↺
      • proves proof app:A-long-proofs@proof-158 ¶
    • proves proof app:A-long-proofs@proof-159 ¶
  • depends_on proposition 12.67 The generator is symmetric, and generates the motion ¶ ↺
  • proves proof app:A-long-proofs@proof-162 ¶
• depends_on proposition 12.67 The generator is symmetric, and generates the motion ¶ ↺
• depends_on theorem A.253 Stone ¶
  • depends_on definition 12.64 Strongly continuous one-parameter unitary group ¶ ↺
  • depends_on proposition 12.67 The generator is symmetric, and generates the motion ¶ ↺
  • depends_on theorem A.238 Spectral theorem, both forms ¶
    • depends_on definition 12.58 Projection-valued measure ¶
      • depends_on definition 12.41 The operator classes ¶
        • depends_on definition 6.9 Compact set ¶
        • depends_on proposition 12.21 Characterization of orthogonal projections ¶
        • depends_on theorem 12.38 Existence and uniqueness of the adjoint ¶
      • 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 app:A-long-proofs@proof-151 ¶
    • proves proof app:A-long-proofs@proof-153 ¶
    • proves proof app:A-long-proofs@proof-156 ¶
  • proves proof app:A-long-proofs@proof-166 ¶
• proves proof app:A-long-proofs@proof-167 ¶

Supports

Nothing declares a dependency on this node yet.