OAI/Geometry/ConjugatePoints/Returning.lean

GitHub source file

155 declarations, 0 contain sorry, 0 declared as axioms

Returning neck geodesics, passage dynamics, and index bounds.

  1. lemma OAI.ThreeManifold.Neck.metric_smul_left line 19
  2. lemma OAI.ThreeManifold.Neck.gamma_add_right line 24
  3. lemma OAI.ThreeManifold.Neck.gamma_smul_right line 33
  4. lemma OAI.ThreeManifold.Neck.covariant_gauge line 41
  5. lemma OAI.ThreeManifold.Neck.curvature_contraction_gauge line 47
  6. def OAI.ThreeManifold.Neck.normalDensity line 60
  7. lemma OAI.ThreeManifold.Neck.normalDensity_gauge line 65
  8. lemma OAI.ThreeManifold.Neck.metric_compatibility_jet line 76
  9. lemma OAI.ThreeManifold.Neck.metric_hasDerivAt line 84
  10. lemma OAI.ThreeManifold.Neck.pairing_neg_right line 101
  11. lemma OAI.ThreeManifold.Neck.tangential_hasDerivAt line 105
  12. def OAI.ThreeManifold.Turning.beta line 126
  13. def OAI.ThreeManifold.Turning.aZero line 128
  14. lemma OAI.ThreeManifold.Turning.beta_pos line 130
  15. lemma OAI.ThreeManifold.Turning.beta_lt_one line 135
  16. lemma OAI.ThreeManifold.Turning.aZero_pos line 140
  17. def OAI.ThreeManifold.Turning.SmallParameter line 142
  18. lemma OAI.ThreeManifold.Turning.small_half line 146
  19. lemma OAI.ThreeManifold.Turning.small_gain line 152
  20. lemma OAI.ThreeManifold.Turning.mixed_square_lower line 158
  21. lemma OAI.ThreeManifold.Turning.endpoint_gain line 171
  22. lemma OAI.ThreeManifold.Turning.minimize_quadratic line 205
  23. theorem OAI.ThreeManifold.Turning.returning_quadratic_bound line 215
  24. lemma OAI.ThreeManifold.DirectTurning.two_energy_nonneg line 245
  25. lemma OAI.ThreeManifold.DirectTurning.dual_pairing line 256
  26. lemma OAI.ThreeManifold.DirectTurning.dual_pairing_self line 262
  27. lemma OAI.ThreeManifold.DirectTurning.direct_pointwise_quadratic line 267
  28. lemma OAI.ThreeManifold.DirectTurning.interval_cauchy_of_quadratic line 287
  29. lemma OAI.ThreeManifold.DirectTurning.pairing_quadratic line 312
  30. lemma OAI.ThreeManifold.DirectTurning.add_boundary_cauchy line 319
  31. lemma OAI.ThreeManifold.DirectTurning.dotProduct_hasDerivAt line 333
  32. lemma OAI.ThreeManifold.DirectTurning.direct_endpoint_functional line 341
  33. lemma OAI.ThreeManifold.DirectTurning.integral_direct_coefficient line 366
  34. lemma OAI.ThreeManifold.DirectTurning.continuousOn_dot_left line 395
  35. def OAI.ThreeManifold.DirectTurning.energyDensity line 401
  36. lemma OAI.ThreeManifold.DirectTurning.direct_endpoint_cauchy line 405
  37. theorem OAI.ThreeManifold.DirectTurning.returning_endpoint_bound line 455
  38. lemma OAI.ThreeManifold.ReturningTime.convex_chord line 491
  39. lemma OAI.ThreeManifold.ReturningTime.concave_chord line 501
  40. lemma OAI.ThreeManifold.ReturningTime.integral_chord_square line 510
  41. lemma OAI.ThreeManifold.ReturningTime.half_chord_integral line 523
  42. lemma OAI.ThreeManifold.ReturningTime.full_chord_integral line 538
  43. lemma OAI.ThreeManifold.ReturningTime.velocity_convex line 568
  44. lemma OAI.ThreeManifold.ReturningTime.height_concave line 585
  45. lemma OAI.ThreeManifold.ReturningTime.middle_height line 597
  46. lemma OAI.ThreeManifold.ReturningTime.integral_le_const line 616
  47. lemma OAI.ThreeManifold.ReturningTime.integral_quarter_bound line 623
  48. lemma OAI.ThreeManifold.ReturningTime.turning_time_margin line 644
  49. lemma OAI.ThreeManifold.ReturningCoefficients.constant_pairing_deriv line 681
  50. lemma OAI.ThreeManifold.ReturningCoefficients.psd_cauchy line 688
  51. lemma OAI.ThreeManifold.ReturningCoefficients.derivative_antitone line 703
  52. lemma OAI.ThreeManifold.ReturningCoefficients.derivative_difference_psd line 714
  53. lemma OAI.ThreeManifold.ReturningCoefficients.mixed_derivative_bound line 722
  54. lemma OAI.ThreeManifold.ReturningCoefficients.mixed_variation_bound line 748
  55. lemma OAI.ThreeManifold.ReturningCoefficients.mixed_integral_bound line 760
  56. lemma OAI.ThreeManifold.ReturningCoefficients.first_coefficient_bound line 774
  57. lemma OAI.ThreeManifold.ReturningCoefficients.second_coefficient_bound line 790
  58. lemma OAI.ThreeManifold.Cometric.coordinateCometric_smooth line 805
  59. lemma OAI.ThreeManifold.Cometric.coordinateCometric_transpose line 812
  60. lemma OAI.ThreeManifold.Cometric.symmetric_derivative line 820
  61. lemma OAI.ThreeManifold.Cometric.coordinateCometric_deriv_transpose line 831
  62. lemma OAI.ThreeManifold.Cometric.coordinateCometric_end line 836
  63. lemma OAI.ThreeManifold.Cometric.coordinateCometric_end_deriv line 842
  64. lemma OAI.ThreeManifold.Cometric.endpoint_pairing line 859
  65. lemma OAI.ThreeManifold.Cometric.endpoint_derivative_pairing line 864
  66. lemma OAI.ThreeManifold.Cometric.endpoint_derivative_qform line 869
  67. lemma OAI.ThreeManifold.Cometric.a_eighth line 877
  68. lemma OAI.ThreeManifold.Cometric.exact_timing_constant line 882
  69. def OAI.ThreeManifold.ReturningCoefficients.e line 896
  70. lemma OAI.ThreeManifold.ReturningCoefficients.sqnorm_e line 898
  71. lemma OAI.ThreeManifold.ReturningCoefficients.pairing_e_bound line 900
  72. lemma OAI.ThreeManifold.ReturningCoefficients.actual_mixed_bound line 908
  73. lemma OAI.ThreeManifold.ReturningCoefficients.actual_force_end_values line 965
  74. lemma OAI.ThreeManifold.PassageDynamics.smooth_autonomous_unique line 980
  75. def OAI.ThreeManifold.PassageDynamics.scalarVectorField line 995
  76. lemma OAI.ThreeManifold.PassageDynamics.scalarVectorField_smooth line 998
  77. lemma OAI.ThreeManifold.PassageDynamics.scalar_equations_unique line 1002
  78. lemma OAI.ThreeManifold.PassageDynamics.cannot_reach_equilibrium line 1018
  79. lemma OAI.ThreeManifold.PassageDynamics.scalar_reflection line 1031
  80. lemma OAI.ThreeManifold.PassageDynamics.positive_return_has_stationary_maximum line 1052
  81. lemma OAI.ThreeManifold.PassageDynamics.return_midpoint line 1073
  82. lemma OAI.ThreeManifold.PassageDynamics.actual_return_symmetry line 1098
  83. lemma OAI.ThreeManifold.PassageDynamics.force_nonneg_at_top line 1113
  84. lemma OAI.ThreeManifold.PassageDynamics.force_pos_at_top line 1141
  85. lemma OAI.ThreeManifold.PassageDynamics.return_velocity_strictAnti line 1156
  86. def OAI.ThreeManifold.ReturningPassage.potential line 1189
  87. def OAI.ThreeManifold.ReturningPassage.force line 1192
  88. def OAI.ThreeManifold.ReturningPassage.forceDerivative line 1195
  89. lemma OAI.ThreeManifold.ReturningPassage.contDiff_pairing_const line 1198
  90. lemma OAI.ThreeManifold.ReturningPassage.potential_smooth line 1203
  91. lemma OAI.ThreeManifold.ReturningPassage.force_smooth line 1207
  92. lemma OAI.ThreeManifold.ReturningPassage.potential_hasDerivAt line 1211
  93. lemma OAI.ThreeManifold.ReturningPassage.force_hasDerivAt line 1216
  94. lemma OAI.ThreeManifold.ReturningPassage.force_antitone line 1221
  95. theorem OAI.ThreeManifold.ReturningPassage.returning_dynamics line 1234
  96. lemma OAI.ThreeManifold.ReturningPassage.incidence_bound line 1284
  97. lemma OAI.ThreeManifold.ReturningPassage.actual_timing_margin line 1311
  98. lemma OAI.ThreeManifold.ReturningPassage.coordinateCometric_posDef line 1334
  99. lemma OAI.ThreeManifold.ReturningPassage.coordinateCometric_inv_continuousAt line 1345
  100. lemma OAI.ThreeManifold.ReturningPassage.coefficient_expansion line 1355
  101. lemma OAI.ThreeManifold.ReturningPassage.direct_coefficient_nonneg line 1389
  102. lemma OAI.ThreeManifold.ReturningPassage.energy_nonnegative line 1399
  103. def OAI.ThreeManifold.ReturningPassage.sourceMixed line 1411
  104. lemma OAI.ThreeManifold.ReturningPassage.sourceMixed_pos line 1413
  105. lemma OAI.ThreeManifold.ReturningPassage.e_dot line 1418
  106. theorem OAI.ThreeManifold.ReturningPassage.actual_returning_energy_bound line 1421
  107. theorem OAI.ThreeManifold.ReturningPassage.uniform_turning_parameters line 1558
  108. lemma OAI.ThreeManifold.Neck.contDiffOn_pairing line 1607
  109. lemma OAI.ThreeManifold.Neck.contDiffOn_metric line 1617
  110. def OAI.ThreeManifold.Neck.turningAffine line 1623
  111. def OAI.ThreeManifold.Neck.turningChange line 1628
  112. def OAI.ThreeManifold.Neck.turningField line 1631
  113. lemma OAI.ThreeManifold.Neck.turningAffine_zero line 1634
  114. lemma OAI.ThreeManifold.Neck.turningAffine_end line 1638
  115. lemma OAI.ThreeManifold.Neck.turningField_zero line 1642
  116. lemma OAI.ThreeManifold.Neck.turningField_end line 1650
  117. lemma OAI.ThreeManifold.Neck.turningField_tangential line 1658
  118. lemma OAI.ThreeManifold.Neck.turningField_smooth line 1664
  119. lemma OAI.ThreeManifold.Neck.turningAffine_hasDerivAt line 1673
  120. lemma OAI.ThreeManifold.Neck.gauge_hasDerivAt line 1683
  121. lemma OAI.ThreeManifold.Neck.normalDensity_deriv_gauge line 1691
  122. lemma OAI.ThreeManifold.Neck.turning_boundary_term line 1701
  123. lemma OAI.ThreeManifold.Neck.turning_boundary_reduction line 1708
  124. lemma OAI.ThreeManifold.Neck.contDiffAt_det_two line 1720
  125. lemma OAI.ThreeManifold.Neck.matrix_inverse_smoothAt line 1728
  126. lemma OAI.ThreeManifold.Neck.matrix_inverse_first_deriv line 1746
  127. lemma OAI.ThreeManifold.Neck.matrix_inverse_second_deriv line 1755
  128. lemma OAI.ThreeManifold.Neck.continuousOn_metric line 1780
  129. lemma OAI.ThreeManifold.Neck.derivative_transpose line 1786
  130. lemma OAI.ThreeManifold.Neck.gamma_momentum line 1797
  131. lemma OAI.ThreeManifold.Neck.normal_index_integral line 1816
  132. def OAI.ThreeManifold.ReturningPassage.metricInverse line 1903
  133. lemma OAI.ThreeManifold.ReturningPassage.metricInverse_transpose line 1905
  134. lemma OAI.ThreeManifold.ReturningPassage.symmetric_total_deriv line 1910
  135. lemma OAI.ThreeManifold.ReturningPassage.metricInverse_deriv_transpose line 1918
  136. lemma OAI.ThreeManifold.ReturningPassage.metricInverse_second_transpose line 1922
  137. lemma OAI.ThreeManifold.ReturningPassage.metricInverse_smoothAt line 1926
  138. lemma OAI.ThreeManifold.ReturningPassage.metricInverse_first line 1931
  139. lemma OAI.ThreeManifold.ReturningPassage.metricInverse_second line 1937
  140. lemma OAI.ThreeManifold.ReturningPassage.metricInverse_endpoint line 1945
  141. lemma OAI.ThreeManifold.ReturningPassage.metricInverse_endpoint_deriv line 1958
  142. def OAI.ThreeManifold.ReturningPassage.momentumVelocity line 1966
  143. lemma OAI.ThreeManifold.ReturningPassage.momentumVelocity_hasDerivAt line 1969
  144. lemma OAI.ThreeManifold.ReturningPassage.momentumVelocity_unit line 1995
  145. lemma OAI.ThreeManifold.ReturningPassage.momentumVelocity_pairing line 2007
  146. def OAI.ThreeManifold.ReturningPassage.returnNormalDensity line 2021
  147. lemma OAI.ThreeManifold.ReturningPassage.returning_normal_identity line 2027
  148. theorem OAI.ThreeManifold.ReturningPassage.returning_normal_nonnegative line 2156
  149. lemma OAI.ThreeManifold.Neck.contDiffAt_pairing line 2207
  150. lemma OAI.ThreeManifold.Neck.contDiffAt_metric line 2217
  151. lemma OAI.ThreeManifold.Neck.turningChange_smoothAt line 2223
  152. lemma OAI.ThreeManifold.Neck.turningField_smoothAt line 2229
  153. lemma OAI.ThreeManifold.Neck.turningField_tangential_derivative line 2234
  154. lemma OAI.ThreeManifold.ReturningPassage.momentumVelocity_smoothAt line 2255
  155. theorem OAI.ThreeManifold.ReturningPassage.returning_arbitrary_field_nonnegative line 2265