OAI/Analysis/HardSphere/Paths/Index.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.HardSphere.DyadicSkeleton.Index line 13
  2. abbrev OAI.HardSphere.DyadicSkeleton.Noise line 14
  3. def OAI.HardSphere.DyadicSkeleton.law line 16
  4. instance OAI.HardSphere.DyadicSkeleton.(instance at line 17) line 17
  5. def OAI.HardSphere.DyadicSkeleton.uniform line 19
  6. lemma OAI.HardSphere.DyadicSkeleton.uniform_abs_le line 22
  7. lemma OAI.HardSphere.DyadicSkeleton.measurable_uniform line 28
  8. def OAI.HardSphere.DyadicSkeleton.decay line 33
  9. def OAI.HardSphere.DyadicSkeleton.cvel line 34
  10. lemma OAI.HardSphere.DyadicSkeleton.decay_pos line 36
  11. lemma OAI.HardSphere.DyadicSkeleton.decay_lt_one line 37
  12. lemma OAI.HardSphere.DyadicSkeleton.cvel_pos line 39
  13. def OAI.HardSphere.DyadicSkeleton.velocity line 41
  14. def OAI.HardSphere.DyadicSkeleton.position line 44
  15. lemma OAI.HardSphere.DyadicSkeleton.summable_velocity line 47
  16. lemma OAI.HardSphere.DyadicSkeleton.velocity_abs_le line 54
  17. lemma OAI.HardSphere.DyadicSkeleton.measurable_velocity line 73
  18. lemma OAI.HardSphere.DyadicSkeleton.measurable_position line 79
  19. lemma OAI.HardSphere.DyadicSkeleton.position_succ line 84
  20. lemma OAI.HardSphere.DyadicSkeleton.exists_fresh_block line 88
  21. lemma OAI.HardSphere.DyadicSkeleton.resample_preserving line 113
  22. lemma OAI.HardSphere.DyadicSkeleton.lintegral_resample line 150
  23. lemma OAI.HardSphere.DyadicSkeleton.velocity_update_sub line 156
  24. lemma OAI.HardSphere.DyadicSkeleton.position_update_past line 178
  25. lemma OAI.HardSphere.DyadicSkeleton.block_filter line 194
  26. lemma OAI.HardSphere.DyadicSkeleton.position_update_future line 211
  27. lemma OAI.HardSphere.DyadicSkeleton.position_update_other line 224
  28. lemma OAI.HardSphere.DyadicSkeleton.affine_interval_volume line 237
  29. def OAI.HardSphere.DyadicSkeleton.coordinateTest line 255
  30. lemma OAI.HardSphere.DyadicSkeleton.measurable_coordinateTest line 258
  31. lemma OAI.HardSphere.DyadicSkeleton.coordinateTest_update_other line 263
  32. lemma OAI.HardSphere.DyadicSkeleton.coordinateTest_update_past line 270
  33. def OAI.HardSphere.DyadicSkeleton.freshScale line 280
  34. lemma OAI.HardSphere.DyadicSkeleton.freshScale_pos line 281
  35. lemma OAI.HardSphere.DyadicSkeleton.fresh_coordinate_integral line 285
  36. lemma OAI.HardSphere.DyadicSkeleton.fresh_weighted_coordinate line 310
  37. def OAI.HardSphere.DyadicSkeleton.nearTest line 331
  38. lemma OAI.HardSphere.DyadicSkeleton.measurable_nearTest line 334
  39. lemma OAI.HardSphere.DyadicSkeleton.nearTest_le_one line 338
  40. def OAI.HardSphere.DyadicSkeleton.PastInvariant line 344
  41. lemma OAI.HardSphere.DyadicSkeleton.nearTest_pastInvariant line 348
  42. lemma OAI.HardSphere.DyadicSkeleton.fresh_weighted_pair line 354
  43. lemma OAI.HardSphere.DyadicSkeleton.freshScale_eq_rpow line 373
  44. lemma OAI.HardSphere.DyadicSkeleton.freshScale_sq line 388
  45. lemma OAI.HardSphere.DyadicSkeleton.freshScale_gap_bound line 393