OAI/MathematicalPhysics/Heisenberg/HittingKernels.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Heisenberg.Hitting.affineIter line 20
  2. lemma OAI.Heisenberg.Hitting.mulVec_mono line 25
  3. lemma OAI.Heisenberg.Hitting.affineIter_mono line 30
  4. lemma OAI.Heisenberg.Hitting.affineIter_nonneg line 38
  5. lemma OAI.Heisenberg.Hitting.affineIter_super line 42
  6. def OAI.Heisenberg.Hitting.affineHit line 49
  7. lemma OAI.Heisenberg.Hitting.affineIter_bdd line 51
  8. lemma OAI.Heisenberg.Hitting.affineIter_tendsto line 56
  9. lemma OAI.Heisenberg.Hitting.affineHit_fixed line 62
  10. lemma OAI.Heisenberg.Hitting.affineHit_super line 73
  11. lemma OAI.Heisenberg.Hitting.affineHit_nonneg line 77
  12. theorem OAI.Heisenberg.Hitting.affineHit_inverse line 85
  13. lemma OAI.Heisenberg.Exposure.backward_split_left line 103
  14. lemma OAI.Heisenberg.Exposure.backward_split_right line 110
  15. lemma OAI.Heisenberg.Exposure.resolvent_backward line 117
  16. theorem OAI.Heisenberg.Exposure.resolvent_le_supersolution line 126
  17. lemma OAI.Heisenberg.Exposure.columnPerm_nonneg line 161
  18. lemma OAI.Heisenberg.Exposure.nextPinMatrix_backward line 167
  19. theorem OAI.Heisenberg.Exposure.conditional_return_le line 172
  20. lemma OAI.Heisenberg.Exposure.mean_perm_backward line 226
  21. lemma OAI.Heisenberg.Exposure.split_mean_backward line 232
  22. theorem OAI.Heisenberg.Exposure.split_conditional_return_le line 248