OAI/MathematicalPhysics/Heisenberg/HittingEnergy.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Heisenberg.Hitting.DoublySubstochastic line 22
  2. def OAI.Heisenberg.Hitting.backward line 27
  3. def OAI.Heisenberg.Hitting.hitStep line 29
  4. def OAI.Heisenberg.Hitting.hitIter line 32
  5. lemma OAI.Heisenberg.Hitting.backward_mono line 36
  6. lemma OAI.Heisenberg.Hitting.backward_nonneg line 43
  7. lemma OAI.Heisenberg.Hitting.backward_le_one line 48
  8. lemma OAI.Heisenberg.Hitting.hitStep_mono line 54
  9. lemma OAI.Heisenberg.Hitting.hitIter_bounds line 62
  10. lemma OAI.Heisenberg.Hitting.hitIter_mono line 73
  11. def OAI.Heisenberg.Hitting.hitting line 86
  12. lemma OAI.Heisenberg.Hitting.hitIter_bdd line 89
  13. lemma OAI.Heisenberg.Hitting.hitIter_tendsto line 93
  14. lemma OAI.Heisenberg.Hitting.hitting_bounds line 98
  15. lemma OAI.Heisenberg.Hitting.hitting_on line 106
  16. lemma OAI.Heisenberg.Hitting.hitting_harmonic line 112
  17. theorem OAI.Heisenberg.Hitting.hitting_minimal line 126
  18. def OAI.Heisenberg.Hitting.energy line 143
  19. lemma OAI.Heisenberg.Hitting.energy_transpose line 146
  20. theorem OAI.Heisenberg.Hitting.hitting_energy line 157
  21. def OAI.Heisenberg.Exposure.killedMean line 174
  22. lemma OAI.Heisenberg.Exposure.killedMean_substochastic line 177
  23. lemma OAI.Heisenberg.Exposure.killedMean_backward line 221
  24. lemma OAI.Heisenberg.Exposure.killed_hitting_supported line 240
  25. theorem OAI.Heisenberg.Exposure.split_conditional_return_energy line 247