OAI/Geometry/Relativity/CKS/SmoothOuterDEC.lean

GitHub source file

155 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CKSCalculus.D_congr line 13
  2. lemma OAI.CKSCalculus.D_const line 17
  3. lemma OAI.CKSCalculus.D_add line 18
  4. lemma OAI.CKSCalculus.D_sub line 22
  5. lemma OAI.CKSCalculus.D_mul line 26
  6. lemma OAI.CKSCalculus.D_const_mul line 30
  7. lemma OAI.CKSCalculus.D_clm line 34
  8. lemma OAI.CKSCalculus.contDiffAt_D line 36
  9. lemma OAI.CKSCalculus.D_D line 40
  10. lemma OAI.CKSCalculus.D_comm line 48
  11. lemma OAI.CKSCalculus.D_D_mul line 53
  12. lemma OAI.CKSCalculus.D_inv line 70
  13. lemma OAI.CKSCalculus.D_div line 79
  14. lemma OAI.CKSCalculus.diffAt_div line 88
  15. lemma OAI.CKSCalculus.D_pow line 95
  16. lemma OAI.CKSCalculus.D_inv_sq line 102
  17. lemma OAI.CKSCalculus.D_D_inv_sq line 110
  18. lemma OAI.CKSCalculus.D_sin line 129
  19. lemma OAI.CKSCalculus.D_cos line 136
  20. lemma OAI.CKSCalculus.D_D_sin line 143
  21. lemma OAI.CKSCalculus.D_D_sq line 155
  22. lemma OAI.CKSCalculus.D_D_clm line 161
  23. lemma OAI.CKSCalculus.D_eventuallyEq line 165
  24. lemma OAI.CKSCalculus.D_D_congr line 170
  25. lemma OAI.CKSCalculus.D_D_const line 174
  26. lemma OAI.CKSCalculus.D_D_add line 178
  27. lemma OAI.CKSCalculus.D_D_sub line 189
  28. lemma OAI.CKSCalculus.D_D_const_mul line 200
  29. lemma OAI.CKSCalculus.D_comp_real line 206
  30. lemma OAI.CKSCalculus.D_inv_inv line 214
  31. lemma OAI.CKSCalculus.D_D_inv line 219
  32. lemma OAI.CKSCalculus.D_D_div line 238
  33. lemma OAI.CKSCalculus.D_sqrt line 253
  34. lemma OAI.CKSCalculus.D_D_sqrt line 262
  35. structure OAI.CKSRound.LapseJet line 295
  36. def OAI.CKSRound.LapseJet.first line 309
  37. def OAI.CKSRound.LapseJet.second line 310
  38. def OAI.CKSRound.LapseJet.roundMetric line 313
  39. def OAI.CKSRound.LapseJet.roundGamma line 325
  40. def OAI.CKSRound.LapseJet.roundDInv line 336
  41. lemma OAI.CKSRound.LapseJet.gamma_round line 341
  42. lemma OAI.CKSRound.LapseJet.dInv_round line 349
  43. lemma OAI.CKSRound.LapseJet.ricci00_round line 357
  44. lemma OAI.CKSRound.LapseJet.ricci11_round line 369
  45. lemma OAI.CKSRound.LapseJet.ricci22_round line 379
  46. theorem OAI.CKSRound.LapseJet.scalar_round line 390
  47. structure OAI.CKSRound.RoundTensor line 412
  48. def OAI.CKSRound.RoundTensor.jet line 430
  49. lemma OAI.CKSRound.RoundTensor.trace_round line 444
  50. lemma OAI.CKSRound.RoundTensor.normSq_round line 451
  51. lemma OAI.CKSRound.RoundTensor.energy_round line 460
  52. theorem OAI.CKSRound.RoundTensor.normal_momentum_round line 475
  53. theorem OAI.CKSRound.RoundTensor.theta_momentum_round line 486
  54. theorem OAI.CKSRound.RoundTensor.phi_momentum_round line 499
  55. structure OAI.CKSRound.MassJet line 514
  56. def OAI.CKSRound.MassJet.laplace line 528
  57. def OAI.CKSRound.MassJet.gradientSq line 530
  58. def OAI.CKSRound.MassJet.lapse line 532
  59. lemma OAI.CKSRound.MassJet.lapse_laplacian line 547
  60. theorem OAI.CKSRound.MassJet.energy_mass_form line 559
  61. def OAI.CKSRound.MassJet.correction line 580
  62. theorem OAI.CKSRound.MassJet.gradient_cancellation_theta line 596
  63. theorem OAI.CKSRound.MassJet.gradient_cancellation_phi line 614
  64. lemma OAI.CKSRound.MetricJet.ext_data line 641
  65. def OAI.CKSRealizedRound.coord line 655
  66. lemma OAI.CKSRealizedRound.coord_apply line 657
  67. lemma OAI.CKSRealizedRound.D_coord line 659
  68. lemma OAI.CKSRealizedRound.D_D_coord line 664
  69. def OAI.CKSRealizedRound.lapseJet line 667
  70. lemma OAI.CKSRealizedRound.lapse_first line 679
  71. lemma OAI.CKSRealizedRound.lapse_second line 683
  72. def OAI.CKSRealizedRound.metric line 688
  73. def OAI.CKSRealizedRound.metricJet line 691
  74. lemma OAI.CKSRealizedRound.metric_inv line 696
  75. lemma OAI.CKSRealizedRound.D_r_sq line 705
  76. lemma OAI.CKSRealizedRound.D_D_r_sq line 711
  77. lemma OAI.CKSRealizedRound.D_sin_sq line 718
  78. lemma OAI.CKSRealizedRound.D_D_sin_sq line 725
  79. lemma OAI.CKSRealizedRound.D_r_sin_sq line 737
  80. lemma OAI.CKSRealizedRound.D_D_r_sin_sq line 745
  81. theorem OAI.CKSRealizedRound.metricJet_eq_round line 756
  82. def OAI.CKSRealizedRound.radial line 795
  83. lemma OAI.CKSRealizedRound.contDiffAt_radial line 797
  84. lemma OAI.CKSRealizedRound.D_radial line 801
  85. lemma OAI.CKSRealizedRound.D_D_radial line 808
  86. def OAI.CKSRealizedRound.massJet line 827
  87. def OAI.CKSRealizedRound.radicand line 839
  88. def OAI.CKSRealizedRound.lapse line 842
  89. lemma OAI.CKSRealizedRound.contDiffAt_radicand line 845
  90. lemma OAI.CKSRealizedRound.contDiffAt_lapse line 851
  91. lemma OAI.CKSRealizedRound.lapse_pos line 856
  92. lemma OAI.CKSRealizedRound.lapse_sq line 859
  93. lemma OAI.CKSRealizedRound.D_radicand line 864
  94. lemma OAI.CKSRealizedRound.D_D_radicand line 879
  95. lemma OAI.CKSRealizedRound.D_lapse line 904
  96. lemma OAI.CKSRealizedRound.D_D_lapse line 910
  97. theorem OAI.CKSRealizedRound.lapseJet_eq_mass line 919
  98. theorem OAI.CKSRealizedRound.constructed_metricJet line 935
  99. def OAI.CKSRealizedRound.tensor line 955
  100. def OAI.CKSRealizedRound.tensorJet line 960
  101. def OAI.CKSRealizedRound.roundTensor line 964
  102. lemma OAI.CKSRealizedRound.D_normal_tensor line 980
  103. lemma OAI.CKSRealizedRound.D_radial_times_r line 989
  104. lemma OAI.CKSRealizedRound.D_tangential_tensor11 line 1000
  105. lemma OAI.CKSRealizedRound.D_tangential_tensor22 line 1010
  106. theorem OAI.CKSRealizedRound.tensorJet_eq_round line 1025
  107. abbrev OAI.CKSBending.Vec2 line 1054
  108. def OAI.CKSBending.tfApply line 1056
  109. lemma OAI.CKSBending.tfApply_norm_sq line 1059
  110. lemma OAI.CKSBending.tfApply_norm_le line 1064
  111. def OAI.CKSBending.A line 1071
  112. def OAI.CKSBending.Q line 1073
  113. def OAI.CKSBending.C line 1075
  114. def OAI.CKSBending.Z line 1081
  115. def OAI.CKSBending.energyError line 1086
  116. def OAI.CKSBending.momentumError line 1089
  117. lemma OAI.CKSBending.A_one_le line 1091
  118. lemma OAI.CKSBending.A_pos line 1092
  119. lemma OAI.CKSBending.lapse_comparison line 1094
  120. lemma OAI.CKSBending.reciprocal_difference line 1108
  121. lemma OAI.CKSBending.inv_u_sq_le line 1116
  122. lemma OAI.CKSBending.abs_reciprocal_difference line 1121
  123. lemma OAI.CKSBending.inv_A_le_one line 1138
  124. lemma OAI.CKSBending.inv_u_sq_le_two line 1142
  125. lemma OAI.CKSBending.beta_buffer line 1148
  126. lemma OAI.CKSBending.heat_switch_error line 1184
  127. lemma OAI.CKSBending.full_laplacian_gap line 1202
  128. lemma OAI.CKSBending.laplacian_term_bound line 1219
  129. lemma OAI.CKSBending.gradient_term_bound line 1239
  130. lemma OAI.CKSBending.tensor_energy_bound line 1250
  131. theorem OAI.CKSBending.energy_lower_bound line 1261
  132. theorem OAI.CKSBending.momentum_upper_bound line 1278
  133. lemma OAI.CKSBending.normalized_profile_bound line 1327
  134. theorem OAI.CKSBending.outer_DEC_of_source_data line 1348
  135. def OAI.CKSLocalBending.sphereGrad line 1394
  136. def OAI.CKSLocalBending.tangentialMomentum line 1397
  137. lemma OAI.CKSLocalBending.sphereGrad_sq line 1401
  138. lemma OAI.CKSLocalBending.physical_momentumSq line 1405
  139. lemma OAI.CKSLocalBending.computed_energy_eq_residual line 1422
  140. lemma OAI.CKSLocalBending.computed_tangential_eq_residual line 1443
  141. lemma OAI.CKSLocalBending.computed_normal_eq_residual line 1459
  142. theorem OAI.CKSLocalBending.computed_outer_DEC line 1470
  143. def OAI.CKSRealizedRound.normalEntry line 1507
  144. def OAI.CKSRealizedRound.correctionCoeff line 1509
  145. def OAI.CKSRealizedRound.correctedComponent line 1512
  146. lemma OAI.CKSRealizedRound.diffAt_deriv line 1515
  147. lemma OAI.CKSRealizedRound.diffAt_normalEntry line 1519
  148. lemma OAI.CKSRealizedRound.deriv_normalEntry line 1524
  149. lemma OAI.CKSRealizedRound.diffAt_correctionCoeff line 1537
  150. lemma OAI.CKSRealizedRound.D_correctedComponent line 1547
  151. lemma OAI.CKSRealizedRound.diffAt_correctedComponent line 1558
  152. theorem OAI.CKSRealizedRound.roundTensor_correction line 1563
  153. def OAI.CKSRealizedRound.outerMetric line 1582
  154. def OAI.CKSRealizedRound.outerTensor line 1583
  155. theorem OAI.CKSRealizedRound.smooth_outer_DEC line 1587