OAI/Geometry/Relativity/CKS/TailDifferentiation.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CKSADM.unitVector_ne line 11
  2. lemma OAI.CKSADM.unitVector_component line 16
  3. lemma OAI.CKSADM.fderiv_unitVector_component line 19
  4. lemma OAI.CKSADM.joint_fderiv_split line 32
  5. def OAI.CKSADM.radialHeat line 48
  6. lemma OAI.CKSADM.radialHeat_smooth line 51
  7. lemma OAI.CKSADM.pd_log_norm line 63
  8. lemma OAI.CKSADM.pd_norm_rpow line 71
  9. lemma OAI.CKSADM.pd_heat_pullback line 80
  10. def OAI.CKSADM.radialNext line 112
  11. lemma OAI.CKSADM.pd_radialHeat line 116
  12. lemma OAI.CKSADM.HeatGenerated.radialNext line 137
  13. def OAI.CKSADM.cartWord line 146
  14. lemma OAI.CKSADM.pd_congr_on line 150
  15. lemma OAI.CKSADM.cartWord_congr_on line 156
  16. lemma OAI.CKSADM.pd_smooth_on line 162
  17. lemma OAI.CKSADM.cartWord_smooth_on line 166
  18. theorem OAI.CKSADM.radialHeat_word line 172
  19. theorem OAI.CKSADM.radialHeat_word_decay line 191