OAI/Geometry/Relativity/CKS/JointJets.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CKSSphericalHarmonics.eigenvalue_shift line 11
  2. lemma OAI.CKSSphericalHarmonics.radialExtension_norm_bound line 15
  3. def OAI.CKSSphericalHarmonics.angularField line 22
  4. lemma OAI.CKSSphericalHarmonics.angularField_smooth line 25
  5. lemma OAI.CKSSphericalHarmonics.radial_polynomial_hasFDerivAt line 32
  6. def OAI.CKSSphericalHarmonics.temporalJet line 49
  7. lemma OAI.CKSSphericalHarmonics.temporalJet_smooth line 53
  8. lemma OAI.CKSSphericalHarmonics.temporalJet_hasDerivAt line 60
  9. lemma OAI.CKSSphericalHarmonics.temporalJet_bound line 70
  10. abbrev OAI.CKSSphericalHarmonics.SpaceTime line 79
  11. def OAI.CKSSphericalHarmonics.heatDomain line 81
  12. lemma OAI.CKSSphericalHarmonics.heatDomain_open line 83
  13. def OAI.CKSSphericalHarmonics.heatField line 86
  14. lemma OAI.CKSSphericalHarmonics.heatField_smooth line 90
  15. abbrev OAI.CKSSphericalHarmonics.HeatJet line 97
  16. def OAI.CKSSphericalHarmonics.heatNext line 99
  17. def OAI.CKSSphericalHarmonics.heatTerm line 103
  18. lemma OAI.CKSSphericalHarmonics.heatTerm_derivative_identity line 106
  19. lemma OAI.CKSSphericalHarmonics.heatTerm_hasFDerivAt line 125