OAI/Analysis/HardSphere/Bridges/BridgeStrongRegular.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.Bridge.LegMeshRegular line 15
  2. lemma OAI.HardSphere.Bridge.legMeshRegular_measurable line 19
  3. lemma OAI.HardSphere.Bridge.strong_mesh_of_free line 40
  4. lemma OAI.HardSphere.Bridge.raw_norm_tail line 68
  5. lemma OAI.HardSphere.Bridge.strong_leg_mesh_tail line 85
  6. def OAI.HardSphere.Bridge.projectCurve line 121
  7. lemma OAI.HardSphere.Bridge.projectCurve_lift line 123
  8. lemma OAI.HardSphere.Bridge.projectCurve_continuous line 126
  9. lemma OAI.HardSphere.Bridge.trial_left line 131
  10. lemma OAI.HardSphere.Bridge.trial_right line 144
  11. lemma OAI.HardSphere.Bridge.mesh_first_half line 157
  12. lemma OAI.HardSphere.Bridge.mesh_second_half line 162
  13. lemma OAI.HardSphere.Bridge.trial_mesh_left line 170
  14. lemma OAI.HardSphere.Bridge.trial_mesh_right line 177
  15. lemma OAI.HardSphere.Bridge.project_leg_mesh_regular line 185
  16. lemma OAI.HardSphere.Bridge.trial_mesh_regular line 197