OAI/MathematicalPhysics/Heisenberg/SpinAverageBoundary.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Heisenberg.dynamics_norm line 12
2. lemma OAI.Heisenberg.dynamics_continuous line 19
3. lemma OAI.Heisenberg.state_limit_locallyUniform line 23
4. def OAI.Heisenberg.cubeBoundary line 39
5. lemma OAI.Heisenberg.translated_state_difference line 44
6. lemma OAI.Heisenberg.cubeBoundary_error line 52
7. lemma OAI.Heisenberg.scaled_quarter line 72
8. theorem OAI.Heisenberg.cubeBoundary_locallyUniform line 79