OAI/Geometry/Relativity/CKS/RadialProfiles.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CKSBending.paddingWeight line 12
  2. def OAI.CKSBending.paddingMass line 13
  3. def OAI.CKSBending.heatDensity line 14
  4. def OAI.CKSBending.heatTime line 15
  5. lemma OAI.CKSBending.paddingWeight_smooth line 17
  6. lemma OAI.CKSBending.paddingWeight_nonneg line 20
  7. lemma OAI.CKSBending.paddingWeight_le_one line 21
  8. lemma OAI.CKSBending.paddingWeight_monotone line 22
  9. lemma OAI.CKSBending.paddingWeight_zero line 25
  10. lemma OAI.CKSBending.paddingWeight_one line 29
  11. lemma OAI.CKSBending.paddingIntegrand_smooth line 33
  12. lemma OAI.CKSBending.paddingMass_smooth line 36
  13. lemma OAI.CKSBending.paddingMass_hasDerivAt line 38
  14. lemma OAI.CKSBending.paddingMass_initial line 41
  15. lemma OAI.CKSBending.paddingMass_nonneg line 46
  16. lemma OAI.CKSBending.paddingMass_weighted_bound line 53
  17. lemma OAI.CKSBending.paddingMass_bound line 68
  18. lemma OAI.CKSBending.heatDensity_smooth line 75
  19. lemma OAI.CKSBending.heatDensity_nonneg line 80
  20. lemma OAI.CKSBending.heatTime_smooth line 82
  21. lemma OAI.CKSBending.heatTime_hasDerivAt line 84
  22. lemma OAI.CKSBending.heatTime_initial line 87
  23. lemma OAI.CKSBending.heatTime_nonneg line 93