OAI/Analysis/HardSphere/Bridges/LocalReference.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.Bridge.targetUniform line 18
  2. lemma OAI.HardSphere.Bridge.targetUniform_probability line 19
  3. def OAI.HardSphere.Bridge.midpointLower line 24
  4. lemma OAI.HardSphere.Bridge.midpointLower_pos line 25
  5. lemma OAI.HardSphere.Bridge.midpointLower_ne_top line 27
  6. lemma OAI.HardSphere.Bridge.targetUniform_le_midpoint line 29
  7. def OAI.HardSphere.Bridge.individualReference line 43
  8. lemma OAI.HardSphere.Bridge.physical_trial_le_reference line 46
  9. lemma OAI.HardSphere.Bridge.individualReference_probability line 77
  10. def OAI.HardSphere.Bridge.pairedTrialLaw line 94
  11. lemma OAI.HardSphere.Bridge.pairedTrialLaw_probability line 100
  12. lemma OAI.HardSphere.Bridge.pairedTrialLaw_fst line 112
  13. lemma OAI.HardSphere.Bridge.pairedTrialLaw_midpoint line 126
  14. lemma OAI.HardSphere.Bridge.pairedTrial_auxiliary line 136