OAI/Analysis/HardSphere/PathBounds/ConfigurationTailLp.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.configurationTail_preserving line 25
  2. lemma OAI.HardSphere.configurationTail_quasiPreserving line 34
  3. lemma OAI.HardSphere.memLp_configurationTail line 41
  4. def OAI.HardSphere.configurationTailLp line 45
  5. lemma OAI.HardSphere.coe_configurationTailLp line 48
  6. def OAI.HardSphere.configurationTailLinear line 51
  7. lemma OAI.HardSphere.norm_configurationTailLp line 68
  8. def OAI.HardSphere.configurationTailCLM line 81
  9. lemma OAI.HardSphere.coe_configurationTailCLM line 86
  10. def OAI.HardSphere.tailLift line 97
  11. lemma OAI.HardSphere.tailLift_direction_zero line 100
  12. lemma OAI.HardSphere.tailLift_direction_succ line 105
  13. lemma OAI.HardSphere.smooth_tail line 112
  14. lemma OAI.HardSphere.coordDerivative_tail_zero line 118
  15. lemma OAI.HardSphere.coordDerivative_tail_succ line 128
  16. lemma OAI.HardSphere.allowed_of_tail line 141
  17. def OAI.HardSphere.InsertionClearance line 153
  18. def OAI.HardSphere.SmoothTest.insert line 156
  19. def OAI.HardSphere.insertionParentDerivative line 184
  20. def OAI.HardSphere.SmoothMultiplier.insertionScalar line 188
  21. def OAI.HardSphere.SmoothMultiplier.insertionJet line 192
  22. lemma OAI.HardSphere.coe_insertionScalar line 198
  23. lemma OAI.HardSphere.coe_insertionParentDerivative line 204
  24. lemma OAI.HardSphere.coe_insertionJet_zero line 209
  25. lemma OAI.HardSphere.coe_insertionJet_succ line 220
  26. lemma OAI.HardSphere.SmoothTest.jet_insert line 234
  27. lemma OAI.HardSphere.SmoothMultiplier.insertionJet_mem_domain line 281