OAI/MathematicalPhysics/Heisenberg/CyclicEnergy.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Heisenberg.MeshPair.indicatorVector line 11
  2. lemma OAI.Heisenberg.MeshPair.indicatorVector_sq line 14
  3. lemma OAI.Heisenberg.MeshPair.indicatorVector_orth line 18
  4. lemma OAI.Heisenberg.MeshPair.euclideanMap_single line 27
  5. lemma OAI.Heisenberg.MeshPair.indicatorVector_pairing line 31
  6. lemma OAI.Heisenberg.Exposure.exposedPrefix_column_support line 43
  7. def OAI.Heisenberg.Serial.product line 72
  8. def OAI.Heisenberg.Serial.split line 76
  9. theorem OAI.Heisenberg.Serial.mean_product line 82
  10. def OAI.Heisenberg.Serial.follow line 103
  11. def OAI.Heisenberg.Serial.survives line 107
  12. def OAI.Heisenberg.Serial.projection line 111
  13. def OAI.Heisenberg.Serial.walkKernel line 113
  14. lemma OAI.Heisenberg.Serial.projection_mul line 116
  15. lemma OAI.Heisenberg.Serial.walkKernel_succ line 126
  16. theorem OAI.Heisenberg.Serial.walkKernel_apply line 142
  17. lemma OAI.Heisenberg.Serial.backward_profile line 170
  18. def OAI.Heisenberg.Serial.cyclicKernel line 182
  19. lemma OAI.Heisenberg.Serial.cyclicKernel_backward line 187
  20. lemma OAI.Heisenberg.Serial.cyclicKernel_substochastic line 199
  21. lemma OAI.Heisenberg.Serial.cyclic_backward_return line 225
  22. def OAI.Heisenberg.Serial.cutTargets line 237
  23. lemma OAI.Heisenberg.Serial.mem_cutTargets line 241
  24. theorem OAI.Heisenberg.Serial.cyclic_hitting_energy line 244