OAI/Analysis/HardSphere/Bridges/IncrementMoment.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.Wiener.incrementMap line 11
  2. lemma OAI.HardSphere.Wiener.incrementMap_apply line 12
  3. lemma OAI.HardSphere.Wiener.suffix_wiener_law line 14
  4. lemma OAI.HardSphere.Wiener.increment_wiener_mean line 18
  5. lemma OAI.HardSphere.Wiener.increment_center_norm line 28
  6. lemma OAI.HardSphere.Wiener.increment_bridge_mean line 47
  7. def OAI.HardSphere.Bridge.incrementSize line 78
  8. lemma OAI.HardSphere.Bridge.incrementSize_nonneg line 79
  9. lemma OAI.HardSphere.Bridge.incrementSize_continuous line 80
  10. lemma OAI.HardSphere.Bridge.incrementSize_smul line 81
  11. lemma OAI.HardSphere.Bridge.incrementSize_memLp line 84
  12. lemma OAI.HardSphere.Bridge.incrementSize_cube_integrable line 90
  13. lemma OAI.HardSphere.Bridge.incrementSize_cube_mean line 94
  14. def OAI.HardSphere.Bridge.incrementFluctuation line 116
  15. lemma OAI.HardSphere.Bridge.incrementFluctuation_continuous line 117
  16. lemma OAI.HardSphere.Bridge.incrementFluctuation_nonneg line 119
  17. lemma OAI.HardSphere.Bridge.incrementFluctuation_memLp line 121
  18. lemma OAI.HardSphere.Bridge.incrementFluctuation_mean line 124
  19. lemma OAI.HardSphere.Bridge.incrementFluctuation_eval line 147