OAI/MathematicalPhysics/Heisenberg/ReturnConditioning.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Heisenberg.Return.HasHit line 23
  2. lemma OAI.Heisenberg.Return.hasHit_iff_cycle line 25
  3. lemma OAI.Heisenberg.Return.hasHit_apply line 34
  4. lemma OAI.Heisenberg.Return.hasHit_of_mem line 38
  5. def OAI.Heisenberg.Return.hitTime line 41
  6. def OAI.Heisenberg.Return.hitPoint line 43
  7. lemma OAI.Heisenberg.Return.hitPoint_mem line 46
  8. lemma OAI.Heisenberg.Return.hitTime_le line 49
  9. lemma OAI.Heisenberg.Return.hitTime_zero line 52
  10. lemma OAI.Heisenberg.Return.hitTime_pos line 56
  11. lemma OAI.Heisenberg.Return.hitTime_step line 65
  12. def OAI.Heisenberg.Return.firstValue line 79
  13. lemma OAI.Heisenberg.Return.firstValue_of_mem line 83
  14. lemma OAI.Heisenberg.Return.firstValue_step line 88
  15. lemma OAI.Heisenberg.Return.harmonic_firstHit line 98
  16. lemma OAI.Heisenberg.Return.firstValue_unique line 115
  17. lemma OAI.Heisenberg.Return.firstValue_splice_step line 125
  18. lemma OAI.Heisenberg.Return.firstValue_spliced_harmonic line 135
  19. theorem OAI.Heisenberg.Return.nextValue_splice line 142
  20. def OAI.Heisenberg.Return.nextTime line 153
  21. def OAI.Heisenberg.Return.nextPoint line 156
  22. lemma OAI.Heisenberg.Return.nextTime_pos line 160
  23. lemma OAI.Heisenberg.Return.nextPoint_spec line 162
  24. lemma OAI.Heisenberg.Return.nextTime_min line 166
  25. lemma OAI.Heisenberg.Return.nextPoint_injective line 174
  26. def OAI.Heisenberg.Return.nextPermutation line 201
  27. lemma OAI.Heisenberg.Return.nextValue_eq_nextPoint line 204
  28. lemma OAI.Heisenberg.Exposure.semiconj_perm_pow line 215
  29. theorem OAI.Heisenberg.Exposure.split_nextPin_eq line 221
  30. def OAI.Heisenberg.Conditioning.mass line 261
  31. def OAI.Heisenberg.Conditioning.conditional line 264
  32. lemma OAI.Heisenberg.Conditioning.mass_nonneg line 267
  33. lemma OAI.Heisenberg.Conditioning.mass_eq line 270
  34. lemma OAI.Heisenberg.Conditioning.weight_le_mass line 277
  35. theorem OAI.Heisenberg.Conditioning.tower line 283
  36. theorem OAI.Heisenberg.Conditioning.expected_le line 307