OAI/Geometry/Relativity/CKS/CovariantHeat.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CKSInducedSphere.HeatGenerated.neg line 13
  2. lemma OAI.CKSInducedSphere.HeatGenerated.sub line 17
  3. lemma OAI.CKSInducedSphere.HeatGenerated.joint_sphere_smooth line 22
  4. lemma OAI.CKSInducedSphere.heatTensor_generated line 33
  5. abbrev OAI.CKSInducedSphere.TensorFamily line 58
  6. def OAI.CKSInducedSphere.scalarTensor line 60
  7. def OAI.CKSInducedSphere.matrixTensor line 62
  8. def OAI.CKSInducedSphere.covariantD line 64
  9. def OAI.CKSInducedSphere.covariantIterate line 69
  10. def OAI.CKSInducedSphere.timeIterate line 73
  11. def OAI.CKSInducedSphere.covariantTimeJet line 77
  12. lemma OAI.CKSInducedSphere.covariantD_generated line 80
  13. lemma OAI.CKSInducedSphere.covariantIterate_generated line 92
  14. lemma OAI.CKSInducedSphere.timeIterate_generated line 99
  15. lemma OAI.CKSInducedSphere.covariantTimeJet_generated line 106
  16. def OAI.CKSInducedSphere.tensorNorm line 111
  17. lemma OAI.CKSInducedSphere.euclidean_norm_le_sum_norm line 114
  18. lemma OAI.CKSInducedSphere.generated_tensor_decay line 124
  19. theorem OAI.CKSInducedSphere.heat_covariant_estimates line 134