OAI/Analysis/HardSphere/Bridges/PhysicalInsertion.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.Bridge.referenceOn line 18
  2. lemma OAI.HardSphere.Bridge.referenceOn_map line 21
  3. lemma OAI.HardSphere.Bridge.referenceOn_collision line 25
  4. lemma OAI.HardSphere.Bridge.referenceOn_probability line 33
  5. def OAI.HardSphere.Bridge.referenceChecks line 50
  6. lemma OAI.HardSphere.Bridge.physical_check_failure line 54
  7. lemma OAI.HardSphere.Bridge.physical_reference_insertion line 81
  8. def OAI.HardSphere.Bridge.fixedEndpoints line 112
  9. lemma OAI.HardSphere.Bridge.fixedEndpoints_measurable line 113
  10. lemma OAI.HardSphere.Bridge.full_bridge_fixedEndpoints line 117
  11. lemma OAI.HardSphere.Bridge.trial_fixedEndpoints line 122
  12. lemma OAI.HardSphere.Bridge.restrict_inter_ae_full line 129
  13. lemma OAI.HardSphere.Bridge.measure_inter_ae_full line 137
  14. lemma OAI.HardSphere.Bridge.individualReference_pin line 145
  15. lemma OAI.HardSphere.Bridge.trialKernel_pin line 151