OAI/MathematicalPhysics/Heisenberg/FirstReturns.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Heisenberg.Exposure.restrictPerm line 15
  2. def OAI.Heisenberg.Exposure.AllHit line 20
  3. lemma OAI.Heisenberg.Exposure.cycle_hit_of_walk_none line 24
  4. lemma OAI.Heisenberg.Exposure.escapes_of_pow_hit line 43
  5. lemma OAI.Heisenberg.Exposure.escapes_restrictPerm_iff line 57
  6. lemma OAI.Heisenberg.Exposure.allHit_iff_escapes line 67
  7. def OAI.Heisenberg.Exposure.columnPerm line 77
  8. lemma OAI.Heisenberg.Exposure.columnPerm_QQ line 81
  9. theorem OAI.Heisenberg.Exposure.det_one_sub_columnPerm_QQ line 93
  10. def OAI.Heisenberg.Exposure.pinTestMatrix line 99
  11. theorem OAI.Heisenberg.Exposure.det_pinTest_of_not_allHit line 102
  12. def OAI.Heisenberg.Exposure.hittingResolvent line 134
  13. lemma OAI.Heisenberg.Exposure.pinTest_block_form line 137
  14. theorem OAI.Heisenberg.Exposure.det_pinTest_schur line 149
  15. theorem OAI.Heisenberg.Exposure.det_pinTest_zero line 160
  16. theorem OAI.Heisenberg.Exposure.det_pinTest_allHit line 166
  17. def OAI.Heisenberg.Exposure.hitWeight line 182
  18. theorem OAI.Heisenberg.Exposure.allHit_determinant line 185
  19. theorem OAI.Heisenberg.Exposure.allHit_determinant_before_division line 199
  20. theorem OAI.Heisenberg.Exposure.conditional_resolvent_determinant line 211
  21. lemma OAI.Heisenberg.Exposure.det_one_sub_single_mul line 236