OAI/Analysis/HardSphere/Bridges/TrialCutoff.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.Bridge.trial_reverse line 16
  2. lemma OAI.HardSphere.Bridge.trial_initial_diameter line 36
  3. lemma OAI.HardSphere.Bridge.trial_endpoint_regular line 51
  4. lemma OAI.HardSphere.Bridge.prefix_or_suffix line 64
  5. def OAI.HardSphere.Bridge.TrialConfined line 76
  6. lemma OAI.HardSphere.Bridge.trial_confined line 79
  7. lemma OAI.HardSphere.Bridge.trialConfined_measurable line 91
  8. def OAI.HardSphere.Bridge.TrialCutoff line 104
  9. lemma OAI.HardSphere.Bridge.trialCutoff_measurable line 107
  10. lemma OAI.HardSphere.Bridge.trial_cutoff_of_legs line 111
  11. lemma OAI.HardSphere.Bridge.mesh_interval_time line 136
  12. lemma OAI.HardSphere.Bridge.prefix_representation line 142
  13. def OAI.HardSphere.Bridge.meshLocalLift line 149
  14. lemma OAI.HardSphere.Bridge.meshLocalLift_zero line 154
  15. lemma OAI.HardSphere.Bridge.meshLocalLift_project line 159
  16. lemma OAI.HardSphere.Bridge.meshLocalLift_increment line 169
  17. lemma OAI.HardSphere.Bridge.mesh_torus_hit_local line 189