OAI/Geometry/Relativity/CKS/BondiBalance.lean

GitHub source file

134 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CKSLorentz.boost_to_rest line 18
  2. lemma OAI.CKSLorentz.charge_energy line 25
  3. lemma OAI.CKSLorentz.charge_momentum line 33
  4. def OAI.CKSLorentz.heatDatum line 41
  5. lemma OAI.CKSLorentz.heatDatum_smooth line 44
  6. lemma OAI.CKSLorentz.heatDatum_balanced line 47
  7. theorem OAI.CKSLorentz.balanced_charge_and_heat line 75
  8. def OAI.CKSLorentz.polarInverse line 106
  9. lemma OAI.CKSLorentz.normalizeAmbient_polarParam line 118
  10. lemma OAI.CKSLorentz.slice_projection line 121
  11. lemma OAI.CKSLorentz.polarInverse_param line 126
  12. lemma OAI.CKSLorentz.polarInverse_smoothAt_param line 131
  13. lemma OAI.CKSLorentz.polarInverse_fderiv_left line 144
  14. lemma OAI.CKSLorentz.polarParam_fderiv_injective line 156
  15. lemma OAI.CKSLorentz.polarParam_fderiv_surjective line 163
  16. theorem OAI.CKSLorentz.polar_inverse_differentials line 168
  17. structure OAI.CKSMetricGluing.CompatibleLocalMetrics line 198
  18. def OAI.CKSMetricGluing.CompatibleLocalMetrics.gluedInner line 210
  19. lemma OAI.CKSMetricGluing.CompatibleLocalMetrics.gluedInner_eq line 225
  20. lemma OAI.CKSMetricGluing.CompatibleLocalMetrics.gluedInner_smooth line 229
  21. theorem OAI.CKSMetricGluing.CompatibleLocalMetrics.exists_smoothMetric line 239
  22. abbrev OAI.CKSTangentCoefficients.V line 259
  23. abbrev OAI.CKSTangentCoefficients.Mat line 260
  24. abbrev OAI.CKSTangentCoefficients.Bil line 261
  25. def OAI.CKSTangentCoefficients.matrixBilinear line 263
  26. abbrev OAI.CKSTangentCoefficients.TangentTriv line 268
  27. def OAI.CKSTangentCoefficients.bilinearTriv line 271
  28. def OAI.CKSTangentCoefficients.liftedInner line 276
  29. lemma OAI.CKSTangentCoefficients.matrixBilinear_apply line 289
  30. lemma OAI.CKSTangentCoefficients.matrixBilinear_symm line 292
  31. lemma OAI.CKSTangentCoefficients.matrixBilinear_pos line 307
  32. instance OAI.CKSTangentCoefficients.bilinearTriv_atlas line 315
  33. lemma OAI.CKSTangentCoefficients.bilinearTriv_baseSet line 317
  34. lemma OAI.CKSTangentCoefficients.bilinearTriv_pair line 319
  35. lemma OAI.CKSTangentCoefficients.liftedInner_pair line 334
  36. def OAI.CKSLorentz.polarLift line 354
  37. lemma OAI.CKSLorentz.bilinear_eq_of_coordinate_basis line 367
  38. lemma OAI.CKSLorentz.polarLift_components line 372
  39. lemma OAI.CKSLorentz.polarTensor_ext line 383
  40. theorem OAI.CKSLorentz.polarLift_reconstruction line 395
  41. theorem OAI.CKSLorentz.polarLift_overlap line 415
  42. lemma OAI.CKSAngularGeometry.fderiv_angularChange_entries line 441
  43. lemma OAI.CKSAngularGeometry.coordinateTensorPullback_angularBlock line 452
  44. theorem OAI.CKSLorentz.physicalCollar_lift_angular_covariant line 480
  45. lemma OAI.CKSLorentz.matrixBilinear_contDiff line 524
  46. lemma OAI.CKSLorentz.polarLift_smoothAt line 532
  47. lemma OAI.CKSLorentz.polarLift_smooth_positive line 549
  48. lemma OAI.CKSMixedGeometry.source_cksLeading_smoothAt line 580
  49. theorem OAI.CKSMixedGeometry.sourceCollarData_smoothAt line 593
  50. lemma OAI.CKSMixedGeometry.sourceAspect_smoothAt line 651
  51. lemma OAI.CKSMixedGeometry.sourceCollar_sigma_radial line 661
  52. lemma OAI.CKSMixedGeometry.sourceCollar_sigma_radial_eventually line 670
  53. lemma OAI.CKSMixedGeometry.sourceCollar_fstar_radial line 678
  54. lemma OAI.CKSMixedGeometry.sourceCollar_sigma_hermitian line 691
  55. lemma OAI.CKSMixedGeometry.sourceCollar_metricError_hermitian line 695
  56. lemma OAI.CKSMixedGeometry.sourceCollar_tau_hermitian line 706
  57. lemma OAI.CKSMixedGeometry.sourceCollar_symmetries line 720
  58. def OAI.CKSAngularGeometry.rawFutureDomain line 747
  59. lemma OAI.CKSAngularGeometry.rawFutureDomain_open line 750
  60. lemma OAI.CKSAngularGeometry.rawFutureFamily_regular line 760
  61. lemma OAI.CKSAngularGeometry.field_future_regular line 769
  62. theorem OAI.CKSAngularGeometry.bounded_thin_future_field_regions line 788
  63. theorem OAI.CKSMixedGeometry.cks_collar_future_regions line 832
  64. theorem OAI.CKSMixedGeometry.source_actual_collar_future_regions line 878
  65. lemma OAI.CKSAngularGeometry.physicalCollarQ_hermitian line 924
  66. lemma OAI.CKSAngularGeometry.physical_collar_pivots line 935
  67. lemma OAI.CKSMixedGeometry.logRadiusChart_slice line 968
  68. lemma OAI.CKSMixedGeometry.physical_source_collar_old_DEC line 975
  69. theorem OAI.CKSMixedGeometry.source_actual_collar_physical_DEC line 1030
  70. structure OAI.CKSAngularGeometry.PhysicalRegularAt line 1083
  71. lemma OAI.CKSAngularGeometry.foliationTensor_contDiffAt line 1099
  72. lemma OAI.CKSAngularGeometry.physical_collar_regularAt line 1131
  73. theorem OAI.CKSMixedGeometry.source_actual_collar_regular line 1159
  74. structure OAI.CKSLorentz.CollarSourcePatch line 1204
  75. def OAI.CKSLorentz.CollarSourcePatch.fields line 1218
  76. def OAI.CKSLorentz.CollarSourcePatch.metric line 1221
  77. def OAI.CKSLorentz.CollarSourcePatch.tensor line 1223
  78. theorem OAI.CKSLorentz.actual_collar_lift_eq line 1235
  79. def OAI.CKSLorentz.spatialDirection line 1291
  80. def OAI.CKSLorentz.polarCone line 1297
  81. lemma OAI.CKSLorentz.spatialDirection_val line 1309
  82. lemma OAI.CKSLorentz.spatialDirection_continuousAt line 1311
  83. lemma OAI.CKSLorentz.spatialDirection_polarParam line 1317
  84. theorem OAI.CKSLorentz.polarCone_open line 1323
  85. lemma OAI.CKSLorentz.polarInverse_direction line 1330
  86. theorem OAI.CKSLorentz.polarCone_inverse line 1335
  87. theorem OAI.CKSLorentz.polarCone_param line 1348
  88. structure OAI.CKSLorentz.SourceCollarAtlas line 1365
  89. def OAI.CKSLorentz.collarAnnulus line 1383
  90. def OAI.CKSLorentz.SourceCollarAtlas.localIndex line 1385
  91. def OAI.CKSLorentz.SourceCollarAtlas.metric line 1387
  92. def OAI.CKSLorentz.SourceCollarAtlas.tensor line 1389
  93. lemma OAI.CKSLorentz.CollarSourcePatch.sigma_eventually line 1401
  94. lemma OAI.CKSLorentz.SourceCollarAtlas.positive_eventually line 1407
  95. lemma OAI.CKSLorentz.SourceCollarAtlas.symmetric_eventually line 1413
  96. lemma OAI.CKSLorentz.slice_exp_log_projection line 1419
  97. lemma OAI.CKSLorentz.logRadiusChart_slice_exp line 1422
  98. theorem OAI.CKSLorentz.SourceCollarAtlas.eventually_pointwise line 1429
  99. lemma OAI.CKSLorentz.polarCone_overlap line 1480
  100. lemma OAI.CKSLorentz.physicalCollarGamma_pos_of_metric line 1495
  101. lemma OAI.CKSLorentz.SourceCollarAtlas.compatible line 1502
  102. lemma OAI.CKSLorentz.SourceCollarAtlas.local_eq line 1528
  103. lemma OAI.CKSLorentz.collarAnnulus_open line 1551
  104. lemma OAI.CKSLorentz.polarLift_symmetric line 1553
  105. theorem OAI.CKSLorentz.actual_global_collar line 1561
  106. lemma OAI.CKSLorentz.cksSourceFields_gamma line 1651
  107. lemma OAI.CKSLorentz.cksSourceFields_tangential line 1661
  108. lemma OAI.CKSLorentz.cksSourceFields_radial line 1671
  109. lemma OAI.CKSLorentz.metricBlock_add_perturbation line 1677
  110. theorem OAI.CKSLorentz.cksSourceFields_reconstruct line 1686
  111. lemma OAI.CKSMixedGeometry.matrixThreeJets_value_bound line 1711
  112. lemma OAI.CKSMixedGeometry.actualScalarJet_value_bound line 1719
  113. theorem OAI.CKSMixedGeometry.source_collar_metric_comparison line 1723
  114. lemma OAI.CKSAngularGeometry.physicalCollarMetric_normalized line 1795
  115. theorem OAI.CKSMixedGeometry.source_physical_collar_metric_comparison line 1828
  116. lemma OAI.CKSLorentz.hyperbolicField_apply line 1895
  117. lemma OAI.CKSLorentz.polarParam_fderiv line 1899
  118. lemma OAI.CKSLorentz.polarParam_fderiv_radial line 1911
  119. lemma OAI.CKSLorentz.polarParam_fderiv_angular line 1918
  120. lemma OAI.CKSLorentz.hyperbolicField_polar line 1927
  121. lemma OAI.CKSLorentz.polarTensorComponents_hermitian line 1976
  122. lemma OAI.CKSLorentz.polar_sourceSpatial line 1983
  123. theorem OAI.CKSLorentz.spatial_source_reconstruction line 1990
  124. lemma OAI.CKSLorentz.SourceCollarAtlas.eventually_local_lower line 2022
  125. lemma OAI.CKSLorentz.polarLift_quadratic line 2054
  126. theorem OAI.CKSLorentz.actual_global_collar_source_lower line 2064
  127. lemma OAI.CKSMixedGeometry.source_rounding_initial_fields line 2108
  128. lemma OAI.CKSMixedGeometry.source_rounding_initial_fields_eventually line 2130
  129. lemma OAI.CKSMixedGeometry.source_inner_collar_lapse_closed line 2141
  130. theorem OAI.CKSMixedGeometry.source_inner_collar_recovery_closed line 2157
  131. lemma OAI.CKSMixedGeometry.sourceExpansion_of_old_future line 2193
  132. lemma OAI.CKSLorentz.SourceCollarAtlas.eventually_sourceExpansion line 2235
  133. lemma OAI.CKSLorentz.polarLift_congr_point line 2279
  134. theorem OAI.CKSLorentz.SourceCollarAtlas.eventually_inner_recovery line 2284