OAI/Analysis/HardSphere/Geometry/CoordinateLine.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.project_representative line 15
  2. lemma OAI.HardSphere.project_add line 20
  3. lemma OAI.HardSphere.project_sub line 25
  4. lemma OAI.HardSphere.continuous_project line 30
  5. lemma OAI.HardSphere.isQuotientMap_project line 38
  6. lemma OAI.HardSphere.continuous_of_continuous_lift line 55
  7. lemma OAI.HardSphere.fderiv_lift_eq line 61
  8. lemma OAI.HardSphere.coordDerivative_project line 75
  9. lemma OAI.HardSphere.continuous_coordDerivative line 83
  10. lemma OAI.HardSphere.SmoothTest.continuous line 91
  11. lemma OAI.HardSphere.SmoothTest.continuous_partial line 94
  12. def OAI.HardSphere.coordinateLine line 98
  13. lemma OAI.HardSphere.project_coordinateLine line 102
  14. lemma OAI.HardSphere.hasDerivAt_coordinateLine line 112
  15. lemma OAI.HardSphere.continuous_coordinateLine line 132
  16. lemma OAI.HardSphere.integral_partial_coordinateLine line 145
  17. lemma OAI.HardSphere.integral_coordDerivative line 160
  18. lemma OAI.HardSphere.coordDerivative_mul line 204
  19. lemma OAI.HardSphere.coordDerivative_conj line 216
  20. def OAI.HardSphere.smoothAlgebra line 234
  21. def OAI.HardSphere.coordinateCharacter line 262
  22. lemma OAI.HardSphere.coordinateCharacter_smooth line 266
  23. lemma OAI.HardSphere.smoothAlgebra_separatesPoints line 275
  24. lemma OAI.HardSphere.smoothAlgebra_dense line 287
  25. lemma OAI.HardSphere.smoothAlgebra_toLp_dense line 294
  26. lemma OAI.HardSphere.integral_integration_by_parts line 300
  27. def OAI.HardSphere.smoothPartial line 325
  28. lemma OAI.HardSphere.SmoothTest.weak_derivative line 334
  29. lemma OAI.HardSphere.weak_derivative line 357
  30. lemma OAI.HardSphere.derivative_zero_of_scalar_zero line 370