OAI/MathematicalPhysics/Heisenberg/ConditionalMoments.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Heisenberg.Exposure.conditional_hitWeight_sum line 20
  2. theorem OAI.Heisenberg.Exposure.conditional_resolvent_first_moment line 27
  3. lemma OAI.Heisenberg.Exposure.reachesPin line 59
  4. def OAI.Heisenberg.Exposure.firstPinTime line 65
  5. def OAI.Heisenberg.Exposure.firstPin line 68
  6. lemma OAI.Heisenberg.Exposure.firstPin_spec line 71
  7. lemma OAI.Heisenberg.Exposure.firstPinTime_min line 75
  8. lemma OAI.Heisenberg.Exposure.firstPinTime_inl line 79
  9. lemma OAI.Heisenberg.Exposure.firstPin_inl line 84
  10. lemma OAI.Heisenberg.Exposure.firstPinTime_inr_pos line 89
  11. lemma OAI.Heisenberg.Exposure.firstPinTime_step line 96
  12. lemma OAI.Heisenberg.Exposure.firstPin_step line 110
  13. def OAI.Heisenberg.Exposure.nextPin line 116
  14. lemma OAI.Heisenberg.Exposure.nextPin_spec line 119
  15. lemma OAI.Heisenberg.Exposure.nextPin_is_first line 125
  16. def OAI.Heisenberg.Exposure.firstPinMatrix line 140
  17. def OAI.Heisenberg.Exposure.nextPinMatrix line 143
  18. lemma OAI.Heisenberg.Exposure.firstPinMatrix_boundary line 147
  19. lemma OAI.Heisenberg.Exposure.firstPinMatrix_step line 152
  20. theorem OAI.Heisenberg.Exposure.nextPinMatrix_eq_resolvent line 165
  21. lemma OAI.Heisenberg.Exposure.nextPin_injective line 198
  22. def OAI.Heisenberg.Exposure.nextPinEquiv line 229
  23. theorem OAI.Heisenberg.Exposure.conditional_nextPin_first_moment line 239