OAI/Geometry/Relativity/CKS/BendingProfiles.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CKSBending.phi line 11
  2. def OAI.CKSBending.xi line 14
  3. def OAI.CKSBending.zeta line 15
  4. def OAI.CKSBending.beta line 16
  5. def OAI.CKSBending.bendingV line 18
  6. def OAI.CKSBending.bendingZeta line 19
  7. def OAI.CKSBending.bendingBeta line 20
  8. lemma OAI.CKSBending.phi_one line 22
  9. lemma OAI.CKSBending.phi_tail line 24
  10. lemma OAI.CKSBending.phi_pos line 26
  11. lemma OAI.CKSBending.phi_le_one line 34
  12. lemma OAI.CKSBending.phi_smooth line 45
  13. lemma OAI.CKSBending.xi_smooth line 50
  14. lemma OAI.CKSBending.zeta_smooth line 51
  15. lemma OAI.CKSBending.beta_smooth line 52
  16. lemma OAI.CKSBending.xi_nonneg line 54
  17. lemma OAI.CKSBending.xi_le_one line 55
  18. lemma OAI.CKSBending.xi_one line 56
  19. lemma OAI.CKSBending.xi_zero line 58
  20. lemma OAI.CKSBending.zeta_nonneg line 60
  21. lemma OAI.CKSBending.zeta_le_one line 61
  22. lemma OAI.CKSBending.zeta_zero line 62
  23. lemma OAI.CKSBending.zeta_one line 64
  24. lemma OAI.CKSBending.beta_nonneg line 66
  25. lemma OAI.CKSBending.beta_le_one line 67
  26. lemma OAI.CKSBending.beta_one line 68
  27. lemma OAI.CKSBending.beta_one_near line 70
  28. lemma OAI.CKSBending.beta_zero line 72
  29. lemma OAI.CKSBending.bendingV_smooth line 75
  30. lemma OAI.CKSBending.bendingZeta_smooth line 82
  31. lemma OAI.CKSBending.bendingBeta_smooth line 84
  32. lemma OAI.CKSBending.bendingV_nonneg line 87
  33. lemma OAI.CKSBending.bendingV_le_radius line 89
  34. lemma OAI.CKSBending.bendingV_initial line 95
  35. lemma OAI.CKSBending.bendingV_tail line 100
  36. lemma OAI.CKSBending.beta_support line 104
  37. lemma OAI.CKSBending.zeta_support line 112