lemma A.586 Gaussian integral with a complex linear term
open in the book ·
appendices/A-long-proofs.tex:28041
· p. 3073
Rests on
- 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 ¶
Supports
- depends_on proposition A.592 The vacuum of the Schrödinger system ¶
-
depends_on
theorem A.587
The Gaussian average is a non-zero projector that
absorbs the Weyl operators
¶
-
depends_on
lemma A.590
The Gram matrix is universal
¶
- depends_on proposition A.591 Any two irreducible Weyl systems are equivalent ¶
-
depends_on
proposition A.589
Cyclic subspaces and the rank of the average
¶
- depends_on lemma A.590 The Gram matrix is universal ¶ ↺
- depends_on proposition A.591 Any two irreducible Weyl systems are equivalent ¶ ↺
- depends_on proposition A.592 The vacuum of the Schrödinger system ¶ ↺
-
depends_on
lemma A.590
The Gram matrix is universal
¶
Neighborhood
Every logical edge within two steps of this node.
- declared and complete
- partly declared
- a check failed
- not graded
- declared in the source
- inferred from structure
Edges
| type | direction | node | provenance | where |
|---|---|---|---|---|
depends_on |
→ | eq:ana-iterated | declared | appendices/A-long-proofs.tex:28050 |
depends_on |
→ | eq:ft-gaussian | declared | appendices/A-long-proofs.tex:28050 |
depends_on |
→ | eq:ft-translation | declared | appendices/A-long-proofs.tex:28050 |
depends_on |
← | The vacuum of the Schrödinger system | declared | appendices/A-long-proofs.tex:28407 |
depends_on |
← | The Gaussian average is a non-zero projector that absorbs the Weyl operators | declared | appendices/A-long-proofs.tex:28082 |
proves |
← | app:A-long-proofs@proof-351 | declared | appendices/A-long-proofs.tex:28053 |