OAI/MathematicalPhysics/Heisenberg/BoundedStrip.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GibbsStrip.evolve line 18
  2. lemma OAI.GibbsStrip.exp_scalar_add line 21
  3. lemma OAI.GibbsStrip.evolve_add line 26
  4. lemma OAI.GibbsStrip.evolve_differentiable line 34
  5. lemma OAI.GibbsStrip.real_evolve_norm line 45
  6. lemma OAI.GibbsStrip.imaginary_evolve line 56
  7. lemma OAI.GibbsStrip.exp_cancel_left line 61
  8. lemma OAI.GibbsStrip.exp_cancel_right line 66
  9. lemma OAI.GibbsStrip.gibbs_upper_boundary line 71
  10. lemma OAI.GibbsStrip.strip_evolve_bounded line 89
  11. def OAI.HeisenbergStrip.openStrip line 108
  12. def OAI.HeisenbergStrip.closedStrip line 109
  13. theorem OAI.HeisenbergStrip.closure_openStrip line 111
  14. theorem OAI.HeisenbergStrip.isOpen_openStrip line 115
  15. theorem OAI.HeisenbergStrip.bounded_strip_max line 118
  16. def OAI.HeisenbergStrip.gaussian line 132
  17. theorem OAI.HeisenbergStrip.gaussian_differentiable line 134
  18. theorem OAI.HeisenbergStrip.norm_gaussian line 137
  19. theorem OAI.HeisenbergStrip.norm_gaussian_le line 143
  20. theorem OAI.HeisenbergStrip.norm_gaussian_tail line 150
  21. def OAI.HeisenbergStrip.BoundaryCauchy line 160
  22. theorem OAI.HeisenbergStrip.boundary_mem_closedStrip line 165
  23. theorem OAI.HeisenbergStrip.gaussian_uniformCauchy line 169
  24. theorem OAI.HeisenbergStrip.strip_limit_of_boundaryCauchy line 220
  25. theorem OAI.HeisenbergStrip.boundaryCauchy_of_locallyUniform line 269
  26. theorem OAI.HeisenbergStrip.bounded_strip_limit line 294