OAI/Analysis/HardSphere/Bridges/GaussianMixture.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.GaussianPacking.gaussian_sum_density line 15
  2. lemma OAI.HardSphere.GaussianPacking.gaussian_sum_le line 29
  3. lemma OAI.HardSphere.GaussianPacking.scaled_separated line 38
  4. def OAI.HardSphere.Bridge.mean line 64
  5. def OAI.HardSphere.Bridge.leg line 65
  6. lemma OAI.HardSphere.Bridge.leg_continuous line 67
  7. lemma OAI.HardSphere.Bridge.leg_eval_measurable line 72
  8. def OAI.HardSphere.Bridge.legVariance line 75
  9. lemma OAI.HardSphere.Bridge.variance_val line 76
  10. lemma OAI.HardSphere.Bridge.legVariance_val line 80
  11. lemma OAI.HardSphere.Bridge.legVariance_pos line 84
  12. lemma OAI.HardSphere.Bridge.position_law line 89
  13. lemma OAI.HardSphere.Bridge.position_independent line 103
  14. lemma OAI.HardSphere.Bridge.position_joint line 109
  15. lemma OAI.HardSphere.Bridge.mean_separated line 115
  16. instance OAI.HardSphere.Bridge.(instance at line 132) line 132
  17. instance OAI.HardSphere.Bridge.(instance at line 133) line 133
  18. def OAI.HardSphere.Bridge.center line 135
  19. lemma OAI.HardSphere.Bridge.center_continuous line 136
  20. lemma OAI.HardSphere.Bridge.center_zero line 137
  21. lemma OAI.HardSphere.Bridge.center_one line 138
  22. lemma OAI.HardSphere.Bridge.center_eq line 139
  23. def OAI.HardSphere.Bridge.pinned line 140
  24. lemma OAI.HardSphere.Bridge.pinned_continuous line 141
  25. lemma OAI.HardSphere.Bridge.pinned_law line 142
  26. lemma OAI.HardSphere.Bridge.pinned_leg_zero line 151
  27. lemma OAI.HardSphere.Bridge.pinned_leg_one line 154
  28. def OAI.HardSphere.Bridge.leftTime line 158
  29. def OAI.HardSphere.Bridge.rightTime line 162
  30. lemma OAI.HardSphere.Bridge.leftTime_continuous line 167
  31. lemma OAI.HardSphere.Bridge.rightTime_continuous line 168
  32. def OAI.HardSphere.Bridge.midpointTime line 170
  33. def OAI.HardSphere.Bridge.trialPath line 172
  34. lemma OAI.HardSphere.Bridge.trial_zero line 180
  35. lemma OAI.HardSphere.Bridge.trial_one line 184
  36. lemma OAI.HardSphere.Bridge.trial_midpoint line 189
  37. lemma OAI.HardSphere.Bridge.trialPath_continuous line 194
  38. def OAI.HardSphere.Bridge.trialKernel line 206
  39. instance OAI.HardSphere.Bridge.trialKernel_markov line 209
  40. lemma OAI.HardSphere.Bridge.trialKernel_apply line 213