OAI/Geometry/Relativity/CKS/BoostDivergence.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CKSSphericalHarmonics.boostField line 11
2. def OAI.CKSSphericalHarmonics.coordinateCM line 13
3. lemma OAI.CKSSphericalHarmonics.smoothRotation_coordinate line 16
4. lemma OAI.CKSSphericalHarmonics.sphereIntegral_coordinate_rotation line 23
5. lemma OAI.CKSSphericalHarmonics.boostField_decomposition line 48
6. theorem OAI.CKSSphericalHarmonics.sphereIntegral_boostField line 61