OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean

GitHub source file

235 declarations, 0 contain sorry, 0 declared as axioms

Area-controlled end replacement and Schwarzschild equality examples.

  1. abbrev OAI.CKSMetricGluing.InnerField line 110

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:110 (same declaration text).

  2. abbrev OAI.CKSMetricGluing.SmoothMetric line 115

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:115 (same declaration text).

  3. def OAI.CKSMetricGluing.innerSection line 117

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:117 (same declaration text).

  4. abbrev OAI.CKSAngularGeometry.I line 131

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:131 (same declaration text).

  5. def OAI.CKSCalculus.D line 143

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:143 (same declaration text).

  6. abbrev OAI.CKSRound.Idx line 153

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:153 (same declaration text).

  7. abbrev OAI.CKSRound.Mat line 155

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:155 (same declaration text).

  8. structure OAI.CKSRound.MetricJet line 157

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:157 (same declaration text).

  9. def OAI.CKSRound.MetricJet.gamma line 170

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:170 (same declaration text).

  10. def OAI.CKSRound.MetricJet.dInv line 173

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:173 (same declaration text).

  11. def OAI.CKSRound.MetricJet.dGamma line 176

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:176 (same declaration text).

  12. def OAI.CKSRound.MetricJet.ricci line 180

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:180 (same declaration text).

  13. def OAI.CKSRound.MetricJet.scalar line 184

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:184 (same declaration text).

  14. structure OAI.CKSRound.TensorJet line 194

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:194 (same declaration text).

  15. def OAI.CKSRound.MetricJet.trace line 206

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:206 (same declaration text).

  16. def OAI.CKSRound.MetricJet.normSq line 209

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:209 (same declaration text).

  17. def OAI.CKSRound.MetricJet.dTrace line 212

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:212 (same declaration text).

  18. def OAI.CKSRound.MetricJet.tensorDivergence line 215

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:215 (same declaration text).

  19. def OAI.CKSRound.MetricJet.energy line 219

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:219 (same declaration text).

  20. def OAI.CKSRound.MetricJet.momentum line 222

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:222 (same declaration text).

  21. abbrev OAI.CKSRealizedRound.Point line 234

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:234 (same declaration text).

  22. def OAI.CKSRealizedRound.basis line 236

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:236 (same declaration text).

  23. def OAI.CKSLocalBending.momentumSq line 246

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:246 (same declaration text).

  24. def OAI.CKSLocalBending.DEC line 249

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:249 (same declaration text).

  25. abbrev OAI.CKSAngularGeometry.Point line 261

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:261 (same declaration text).

  26. def OAI.CKSAngularGeometry.basis line 263

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:263 (same declaration text).

  27. abbrev OAI.CKSAngularGeometry.AmbientMat line 274

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:274 (same declaration text).

  28. abbrev OAI.CKSAngularGeometry.PhysicalPoint line 285

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:285 (same declaration text).

  29. abbrev OAI.CKSMixedGeometry.I line 296

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:296 (same declaration text).

  30. abbrev OAI.CKSMixedGeometry.A line 298

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:298 (same declaration text).

  31. abbrev OAI.CKSMixedGeometry.Point line 300

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:300 (same declaration text).

  32. def OAI.CKSMixedGeometry.basis line 302

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:302 (same declaration text).

  33. def OAI.CKSMixedGeometry.radialFactor line 315

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:315 (same declaration text).

  34. def OAI.CKSMixedGeometry.scaledD line 319

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:319 (same declaration text).

  35. def OAI.CKSMixedGeometry.scaledIter line 322

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:322 (same declaration text).

  36. abbrev OAI.CKSMixedGeometry.Angle line 335

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:335 (same declaration text).

  37. def OAI.CKSMixedGeometry.angularProjection line 337

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:337 (same declaration text).

  38. def OAI.CKSMixedGeometry.ScaledComponentBound line 340

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:340 (same declaration text).

  39. abbrev OAI.CKSInducedSphere.Ix line 352

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:352 (same declaration text).

  40. abbrev OAI.CKSSphericalHarmonics.Ambient line 362

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:362 (same declaration text).

  41. abbrev OAI.CKSSphericalHarmonics.Sphere line 364

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:364 (same declaration text).

  42. abbrev OAI.CKSSphericalHarmonics.surfaceMeasure line 375

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:375 (same declaration text).

  43. def OAI.CKSSphericalHarmonics.SmoothSphere line 389

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:389 (same declaration text).

  44. abbrev OAI.CKSInducedSphere.E line 410

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:410 (same declaration text).

  45. def OAI.CKSInducedSphere.e line 423

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:423 (same declaration text).

  46. def OAI.CKSInducedSphere.pd line 425

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:425 (same declaration text).

  47. abbrev OAI.CKSLorentz.E line 436

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:436 (same declaration text).

  48. abbrev OAI.CKSLorentz.V line 438

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:438 (same declaration text).

  49. abbrev OAI.CKSLorentz.Sphere line 440

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:440 (same declaration text).

  50. def OAI.CKSLorentz.ordinaryLeadingComponent line 453

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:453 (same declaration text).

  51. structure OAI.CKSMixedGeometry.SourceRemainderOn line 466

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:466 (same declaration text).

  52. structure OAI.CKSLorentz.SourceCKSComponents line 479

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:479 (same declaration text).

  53. def OAI.CKSLorentz.angularRadialTail line 494

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:494 (same declaration text).

  54. structure OAI.CKSLorentz.SmoothAngularPatch line 507

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:507 (same declaration text).

  55. def OAI.CKSLorentz.SmoothAngularPatch.param line 526

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:526 (same declaration text).

  56. def OAI.CKSLorentz.SmoothAngularPatch.sphereRegion line 528

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:528 (same declaration text).

  57. structure OAI.CKSLorentz.CKSTensorPatch line 540

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:540 (same declaration text).

  58. abbrev OAI.CKSLorentz.SpatialBilinear line 585

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:585 (same declaration text).

  59. abbrev OAI.CKSLorentz.SpatialTensor line 590

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:590 (same declaration text).

  60. def OAI.CKSLorentz.polarParam line 594

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:594 (same declaration text).

  61. def OAI.CKSLorentz.polarTensorComponents line 598

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:598 (same declaration text).

  62. def OAI.CKSLorentz.CKSTensorPatch.Realizes line 603

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:603 (same declaration text).

  63. abbrev OAI.CKSLorentz.AngularMatrix line 616

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:616 (same declaration text).

  64. def OAI.CKSLorentz.angularMetricTrace line 618

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:618 (same declaration text).

  65. def OAI.CKSLorentz.angularRoundMetric line 620

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:620 (same declaration text).

  66. def OAI.CKSLorentz.nullDirection line 639

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:639 (same declaration text).

  67. def OAI.CKSLorentz.rawCharge line 641

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:641 (same declaration text).

  68. def OAI.CKSLorentz.bondiCharge line 643

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:643 (same declaration text).

  69. def OAI.CKSLorentz.hyperbolicField line 670

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:670 (same declaration text).

  70. def OAI.CKSLorentz.sourceSpatial line 683

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:683 (same declaration text).

  71. def OAI.CKSADM.normal line 730

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:730 (same declaration text).

  72. def OAI.CKSADM.spatialInfinity line 741

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:741 (same declaration text).

  73. def OAI.CKSADM.TailRegular line 743

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:743 (same declaration text).

  74. def OAI.CKSADM.Decay line 746

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:746 (same declaration text).

  75. def OAI.CKSADM.SymbolN line 749

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:749 (same declaration text).

  76. def OAI.CKSADM.Symbol line 753

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:753 (same declaration text).

  77. def OAI.CKSAngularGeometry.physicalMetricJet line 765

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:765 (same declaration text).

  78. def OAI.CKSAngularGeometry.physicalTensorJet line 770

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:770 (same declaration text).

  79. abbrev OAI.CKSCartesianOuter.toPoint line 784

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:784 (same declaration text).

  80. def OAI.CKSLorentz.cksChartMassAspect line 794

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:794 (same declaration text).

  81. def OAI.CKSLorentz.spatialCoefficients line 808

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:808 (same declaration text).

  82. def OAI.CKSLorentz.spatialDEC line 813

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:813 (same declaration text).

  83. def OAI.CKSLorentz.CKSTensorPatch.RepresentsMassAspect line 825

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:825 (same declaration text).

  84. def OAI.CKSLorentz.spatialCartesian line 837

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:837 (same declaration text).

  85. def OAI.CKSLorentz.spatialADMEnergy line 852

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:852 (same declaration text).

  86. def OAI.CKSLorentz.spatialADMMomentum line 859

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:859 (same declaration text).

  87. def OAI.CKSLorentz.spatialEnergy line 874

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:874 (same declaration text).

  88. abbrev OAI.CKSReplacementCompleteness.Metric line 890

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:890 (same declaration text).

  89. def OAI.CKSReplacementCompleteness.metricSpace line 896

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:896 (same declaration text).

  90. def OAI.CKSReplacementCompleteness.IsComplete line 901

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:901 (same declaration text).

  91. abbrev OAI.CKSGeometricCuts.E3 line 913

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:913 (same declaration text).

  92. abbrev OAI.CKSGeometricCuts.H3 line 917

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:917 (same declaration text).

  93. abbrev OAI.CKSGeometricCuts.I3 line 919

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:919 (same declaration text).

  94. structure OAI.CKSGeometricCuts.OuterDomain line 931

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:931 (same declaration text).

  95. def OAI.CKSSpatialManifold.endInner line 976

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:976 (same declaration text).

  96. def OAI.CKSSpatialManifold.PhysicalDECAt line 998

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:998 (same declaration text).

  97. def OAI.CKSSpatialManifold.PhysicalDEC line 1009

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1009 (same declaration text).

  98. abbrev OAI.CKSIntrinsicGeometry.H3 line 1023

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1023 (same declaration text).

  99. abbrev OAI.CKSIntrinsicGeometry.I3 line 1025

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1025 (same declaration text).

  100. abbrev OAI.CKSBoundarySurface.E2 line 1036

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1036 (same declaration text).

  101. abbrev OAI.CKSBoundarySurface.E3 line 1038

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1038 (same declaration text).

  102. abbrev OAI.CKSBoundarySurface.H3 line 1042

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1042 (same declaration text).

  103. abbrev OAI.CKSBoundarySurface.I2 line 1044

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1044 (same declaration text).

  104. abbrev OAI.CKSBoundarySurface.I3 line 1046

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1046 (same declaration text).

  105. def OAI.CKSBoundarySurface.insertNormalZero line 1061

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1061 (same declaration text).

  106. def OAI.CKSBoundarySurface.liftPlane line 1063

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1063 (same declaration text).

  107. def OAI.CKSBoundarySurface.tangentialCoordinates line 1086

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1086 (same declaration text).

  108. def OAI.CKSBoundarySurface.dropPlane line 1088

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1088 (same declaration text).

  109. def OAI.CKSBoundarySurface.liftHalf line 1117

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1117 (same declaration text).

  110. abbrev OAI.CKSSchwarzschild.Radial line 1132

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1132 (same declaration text).

  111. abbrev OAI.CKSSchwarzschild.Sphere line 1134

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1134 (same declaration text).

  112. abbrev OAI.CKSSchwarzschild.Exterior line 1136

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1136 (same declaration text).

  113. def OAI.CKSSchwarzschild.join line 1152

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1152 (same declaration text).

  114. def OAI.CKSSchwarzschild.halfProduct line 1162

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1162 (same declaration text).

  115. def OAI.CKSSchwarzschild.productChart line 1178

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1178 (same declaration text).

  116. instance OAI.CKSSchwarzschild.exteriorChartedSpace line 1181

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1181 (same declaration text).

  117. instance OAI.CKSSchwarzschild.exteriorIsManifold line 1206

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1206 (same declaration text).

  118. def OAI.CKSSchwarzschild.height line 1267

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1267 (same declaration text).

  119. def OAI.CKSSchwarzschild.radius line 1280

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1280 (same declaration text).

  120. def OAI.CKSSchwarzschild.directionAmbient line 1284

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1284 (same declaration text).

  121. def OAI.CKSSchwarzschild.position line 1286

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1286 (same declaration text).

  122. def OAI.CKSSchwarzschild.velocity line 1297

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1297 (same declaration text).

  123. def OAI.CKSSchwarzschild.lapseSquared line 1301

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1301 (same declaration text).

  124. def OAI.CKSSchwarzschild.lapse line 1305

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1305 (same declaration text).

  125. def OAI.CKSSchwarzschild.euclideanForm line 1317

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1317 (same declaration text).

  126. def OAI.CKSSchwarzschild.radialUnit line 1319

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1319 (same declaration text).

  127. def OAI.CKSSchwarzschild.radialForm line 1323

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1323 (same declaration text).

  128. def OAI.CKSSchwarzschild.cartMetric line 1337

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1337 (same declaration text).

  129. def OAI.CKSSchwarzschild.cartTensor line 1346

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1346 (same declaration text).

  130. def OAI.CKSSchwarzschild.metricInner line 1356

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1356 (same declaration text).

  131. def OAI.CKSSchwarzschild.tensorInner line 1358

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1358 (same declaration text).

  132. abbrev OAI.CKSIntrinsicConstraints.E line 1369

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1369 (same declaration text).

  133. abbrev OAI.CKSIntrinsicConstraints.H line 1373

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1373 (same declaration text).

  134. abbrev OAI.CKSIntrinsicConstraints.I line 1375

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1375 (same declaration text).

  135. def OAI.CKSIntrinsicConstraints.coordinateMomentumNorm line 1389

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1389 (same declaration text).

  136. structure OAI.CKSIntrinsicConstraints.ConstraintChart line 1406

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1406 (same declaration text).

  137. def OAI.CKSIntrinsicConstraints.ConstraintChart.energy line 1428

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1428 (same declaration text).

  138. def OAI.CKSIntrinsicConstraints.ConstraintChart.momentumNorm line 1431

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1431 (same declaration text).

  139. abbrev OAI.CKSIntrinsicVolume.E line 1445

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1445 (same declaration text).

  140. abbrev OAI.CKSIntrinsicVolume.H line 1447

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1447 (same declaration text).

  141. abbrev OAI.CKSIntrinsicVolume.I line 1449

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1449 (same declaration text).

  142. abbrev OAI.CKSIntrinsicVolume.basis line 1451

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1451 (same declaration text).

  143. abbrev OAI.CKSIntrinsicVolume.Metric line 1480

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1480 (same declaration text).

  144. def OAI.CKSIntrinsicVolume.chartFrame line 1482

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1482 (same declaration text).

  145. def OAI.CKSIntrinsicVolume.chartMatrix line 1485

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1485 (same declaration text).

  146. def OAI.CKSIntrinsicVolume.chartDensity line 1494

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1494 (same declaration text).

  147. def OAI.CKSIntrinsicVolume.localVolume line 1509

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1509 (same declaration text).

  148. def OAI.CKSIntrinsicVolume.IsVolume line 1514

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1514 (same declaration text).

  149. def OAI.CKSIntrinsicVolume.riemannianVolume line 1530

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1530 (same declaration text).

  150. abbrev OAI.CKSBoundarySurface.Boundary line 1545

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1545 (same declaration text).

  151. def OAI.CKSBoundarySurface.boundaryInverse line 1562

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1562 (same declaration text).

  152. def OAI.CKSBoundarySurface.boundaryChart line 1612

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1612 (same declaration text).

  153. instance OAI.CKSBoundarySurface.boundaryChartedSpace line 1713

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1713 (same declaration text).

  154. instance OAI.CKSBoundarySurface.boundaryIsManifold line 1729

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1729 (same declaration text).

  155. abbrev OAI.CKSSurfaceVolume.E line 1833

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1833 (same declaration text).

  156. abbrev OAI.CKSSurfaceVolume.H line 1835

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1835 (same declaration text).

  157. abbrev OAI.CKSSurfaceVolume.I line 1837

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1837 (same declaration text).

  158. abbrev OAI.CKSSurfaceVolume.basis line 1839

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1839 (same declaration text).

  159. abbrev OAI.CKSSurfaceVolume.Metric line 1851

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1851 (same declaration text).

  160. def OAI.CKSSurfaceVolume.chartFrame line 1883

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1883 (same declaration text).

  161. def OAI.CKSSurfaceVolume.chartMatrix line 1886

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1886 (same declaration text).

  162. def OAI.CKSSurfaceVolume.chartDensity line 1896

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1896 (same declaration text).

  163. def OAI.CKSSurfaceVolume.localVolume line 1910

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1910 (same declaration text).

  164. def OAI.CKSSurfaceVolume.IsVolume line 1915

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1915 (same declaration text).

  165. def OAI.CKSSurfaceVolume.riemannianVolume line 1927

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1927 (same declaration text).

  166. abbrev OAI.CKSInducedArea.E2 line 1941

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1941 (same declaration text).

  167. abbrev OAI.CKSInducedArea.I2 line 1943

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1943 (same declaration text).

  168. abbrev OAI.CKSInducedArea.E3 line 1945

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1945 (same declaration text).

  169. abbrev OAI.CKSInducedArea.Inner2 line 1988

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:1988 (same declaration text).

  170. abbrev OAI.CKSInducedArea.Smooth3 line 2006

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:2006 (same declaration text).

  171. abbrev OAI.CKSInducedArea.Bil2 line 2022

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:2022 (same declaration text).

  172. abbrev OAI.CKSInducedArea.Bil3 line 2026

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:2026 (same declaration text).

  173. def OAI.CKSInducedArea.inducedInner line 2044

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:2044 (same declaration text).

  174. def OAI.CKSInducedArea.bilinearTriv line 2324

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:2324 (same declaration text).

  175. instance OAI.CKSInducedArea.bilinearTriv_atlas line 2332

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:2332 (same declaration text).

  176. def OAI.CKSInducedArea.inducedMetric line 2541

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:2541 (same declaration text).

  177. abbrev OAI.CKSEmbeddingDerivative.E line 2701

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:2701 (same declaration text).

  178. abbrev OAI.CKSEmbeddingDerivative.H line 2705

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:2705 (same declaration text).

  179. abbrev OAI.CKSEmbeddingDerivative.I line 2707

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:2707 (same declaration text).

  180. instance OAI.CKSFullCutArea.domainTopology line 2721

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:2721 (same declaration text).

  181. instance OAI.CKSFullCutArea.domainCharts line 2723

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:2723 (same declaration text).

  182. instance OAI.CKSFullCutArea.domainSmooth line 2725

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:2725 (same declaration text).

  183. abbrev OAI.CKSFullCutArea.Surface line 2727

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:2727 (same declaration text).

  184. def OAI.CKSFullCutArea.cutInclusion line 2729

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:2729 (same declaration text).

  185. instance OAI.CKSFullCutArea.domainSecondCountable line 2745

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:2745 (same declaration text).

  186. abbrev OAI.CKSFullCutArea.SmoothMetric line 2748

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:2748 (same declaration text).

  187. def OAI.CKSFullCutArea.cutMetric line 2753

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:2753 (same declaration text).

  188. def OAI.CKSFullCutArea.area line 2915

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:2915 (same declaration text).

  189. def OAI.CKSFullCutArea.minEnclosingArea line 2920

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:2920 (same declaration text).

  190. def OAI.CKSIntrinsicConstraints.IntegrableConstraints line 2949

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:2949 (same declaration text).

  191. def OAI.CKSSourceExterior.Orientable line 3000

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3000 (same declaration text).

  192. structure OAI.CKSSourceExterior.CoordinateEnd line 3010

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3010 (same declaration text).

  193. structure OAI.CKSSourceExterior.CKSData line 3025

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3025 (same declaration text).

  194. instance OAI.CKSSchwarzschild.exteriorConnected line 3051

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3051 (same declaration text).

  195. def OAI.CKSSourceExterior.cutArea line 3070

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3070 (same declaration text).

  196. def OAI.CKSSourceExterior.minimumEnclosingArea line 3075

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3075 (same declaration text).

  197. def OAI.CKSSourceExterior.constraintsIntegrable line 3080

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3080 (same declaration text).

  198. def OAI.CKSSchwarzschild.covariantPair line 3096

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3096 (same declaration text).

  199. abbrev OAI.CKSSchwarzschild.Spacetime line 3118

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3118 (same declaration text).

  200. abbrev OAI.CKSSchwarzschild.SpacetimeBilinear line 3120

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3120 (same declaration text).

  201. def OAI.CKSSchwarzschild.timeForm line 3126

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3126 (same declaration text).

  202. def OAI.CKSSchwarzschild.spacePart line 3128

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3128 (same declaration text).

  203. def OAI.CKSSchwarzschild.radiusForm line 3130

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3130 (same declaration text).

  204. def OAI.CKSSchwarzschild.schwarzschildH line 3132

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3132 (same declaration text).

  205. def OAI.CKSSchwarzschild.advancedMetric line 3150

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3150 (same declaration text).

  206. def OAI.CKSSchwarzschild.advancedSlope line 3169

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3169 (same declaration text).

  207. def OAI.CKSSchwarzschild.advancedTime line 3171

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3171 (same declaration text).

  208. def OAI.CKSSchwarzschild.advancedGraph line 3175

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3175 (same declaration text).

  209. def OAI.CKSSchwarzschild.futureNormal line 3177

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3177 (same declaration text).

  210. def OAI.CKSSchwarzschild.graphTangent line 3180

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3180 (same declaration text).

  211. structure OAI.CKSSchwarzschild.HorizonRegularGraph line 3198

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3198 (same declaration text).

  212. def OAI.CKSSchwarzschild.christoffelPair line 3251

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3251 (same declaration text).

  213. def OAI.CKSSchwarzschild.firstFrame line 3255

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3255 (same declaration text).

  214. def OAI.CKSSchwarzschild.secondResidual line 3259

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3259 (same declaration text).

  215. def OAI.CKSSchwarzschild.secondFrame line 3264

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3264 (same declaration text).

  216. def OAI.CKSMain.secondForm line 3326

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3367 (same declaration text).

  217. def OAI.CKSMain.meanCurvature line 3331

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3372 (same declaration text).

  218. def OAI.CKSMain.tangentialTrace line 3336

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3377 (same declaration text).

  219. structure OAI.CKSMain.BoundaryGeometry line 3353

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3394 (same declaration text).

  220. def OAI.CKSMain.BoundaryGeometry.parameter line 3363

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3404 (same declaration text).

  221. def OAI.CKSMain.BoundaryGeometry.thetaPlus line 3367

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3408 (same declaration text).

  222. def OAI.CKSMain.MarginalBoundary line 3375

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3416 (same declaration text).

  223. def OAI.CKSMain.bondiMass line 3378

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3419 (same declaration text).

  224. abbrev OAI.CKSMain.CoefficientAtlas line 3406

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3447 (same declaration text).

  225. structure OAI.CKSMain.InteriorSurface line 3425

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3466 (same declaration text).

  226. def OAI.CKSMain.InteriorSurface.parameter line 3454

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3495 (same declaration text).

  227. def OAI.CKSMain.InteriorSurface.mean line 3457

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3498 (same declaration text).

  228. def OAI.CKSMain.InteriorSurface.trace line 3462

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3503 (same declaration text).

  229. def OAI.CKSMain.InteriorSurface.thetaPlus line 3466

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3507 (same declaration text).

  230. def OAI.CKSMain.InteriorSurface.thetaMinus line 3468

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3509 (same declaration text).

  231. def OAI.CKSMain.InteriorSurface.SeparatesAway line 3470

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3511 (same declaration text).

  232. def OAI.CKSMain.InteriorSurface.ComponentwiseApparent line 3475

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3516 (same declaration text).

  233. def OAI.CKSMain.NoAdditionalHorizons line 3491

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3532 (same declaration text).

  234. structure OAI.CKSMain.MainHypotheses line 3497

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3538 (same declaration text).

  235. def OAI.CKSMain.SchwarzschildExample line 3527

    Also declared: ComparatorChallenges/CKSBondiPenrose.lean:3568 (same declaration text).