OAI/Analysis/HardSphere/Geometry/ConfigurationPath.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.HardSphere.configurationBorel line 20
  2. abbrev OAI.HardSphere.ConfigurationPath line 24
  3. instance OAI.HardSphere.configurationPathMeasurable line 25
  4. instance OAI.HardSphere.configurationPathBorel line 26
  5. def OAI.HardSphere.staysAllowed line 28
  6. lemma OAI.HardSphere.staysAllowed_open line 31
  7. lemma OAI.HardSphere.staysAllowed_antitone line 34
  8. lemma OAI.HardSphere.staysAllowed_innerRadius line 38
  9. abbrev OAI.HardSphere.CoordinatePaths line 50
  10. def OAI.HardSphere.coordinateWiener line 52
  11. instance OAI.HardSphere.coordinateWiener_probability line 53
  12. def OAI.HardSphere.freeTrajectory line 57
  13. lemma OAI.HardSphere.freeTrajectory_continuous line 62
  14. def OAI.HardSphere.freePathLaw line 70
  15. lemma OAI.HardSphere.freeTrajectory_marginal line 74
  16. lemma OAI.HardSphere.freePathLaw_marginal line 93
  17. def OAI.HardSphere.killedPathLaw line 101
  18. def OAI.L2Multiplier.apply line 109
  19. lemma OAI.L2Multiplier.coe_apply line 112
  20. def OAI.L2Multiplier.linearMap line 116
  21. lemma OAI.L2Multiplier.norm_apply_le line 130
  22. def OAI.L2Multiplier.clm line 137
  23. lemma OAI.L2Multiplier.coe_clm line 140
  24. lemma OAI.L2Multiplier.clm_mul line 143
  25. lemma OAI.L2Multiplier.inner_clm_right line 150
  26. abbrev OAI.HardSphere.FreePathL2 line 164
  27. def OAI.HardSphere.endpointPull line 167
  28. lemma OAI.HardSphere.endpointPull_ae line 172
  29. lemma OAI.HardSphere.avoidanceIndicator_memLp line 176
  30. def OAI.HardSphere.avoidanceMultiplier line 180
  31. lemma OAI.HardSphere.avoidanceMultiplier_ae line 183
  32. lemma OAI.HardSphere.avoidanceMultiplier_contraction line 189
  33. lemma OAI.HardSphere.avoidanceMultiplier_norm_le line 196
  34. lemma OAI.HardSphere.integrable_killed_endpoints line 201
  35. def OAI.HardSphere.killedTransition line 208
  36. lemma OAI.HardSphere.killedTransition_pairing line 212
  37. lemma OAI.HardSphere.killedTransition_norm_le line 228
  38. lemma OAI.HardSphere.killedTransition_apply_contraction line 243