OAI/Geometry/Relativity/CKS/SourceCollarBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CKSMixedGeometry.source_tensor_log_bounds line 12
2. lemma OAI.CKSMixedGeometry.source_tensor_log_positive line 26
3. theorem OAI.CKSMixedGeometry.source_actual_collar_coordinate_DEC line 33