OAI/Geometry/ConjugatePoints/Index.lean

GitHub source file

94 declarations, 0 contain sorry, 0 declared as axioms

Index forms, cutoff fields, and assembly of local estimates.

  1. lemma OAI.ThreeManifold.IndexCutoff.transition_smooth line 18
  2. lemma OAI.ThreeManifold.IndexCutoff.transition_deriv_eq_zero line 20
  3. lemma OAI.ThreeManifold.IndexCutoff.transition_deriv_bounded line 33
  4. def OAI.ThreeManifold.IndexCutoff.cutoff line 44
  5. lemma OAI.ThreeManifold.IndexCutoff.cutoff_smooth line 47
  6. lemma OAI.ThreeManifold.IndexCutoff.cutoff_mem_Icc line 51
  7. lemma OAI.ThreeManifold.IndexCutoff.cutoff_eq_zero line 56
  8. lemma OAI.ThreeManifold.IndexCutoff.cutoff_eq_one line 65
  9. lemma OAI.ThreeManifold.IndexCutoff.cutoff_hasDerivAt line 70
  10. lemma OAI.ThreeManifold.IndexCutoff.contractive_smul line 83
  11. def OAI.ThreeManifold.IndexCutoff.field line 87
  12. lemma OAI.ThreeManifold.IndexCutoff.field_smooth line 89
  13. lemma OAI.ThreeManifold.IndexCutoff.field_tsupport line 92
  14. lemma OAI.ThreeManifold.IndexCutoff.field_compactSupport line 100
  15. lemma OAI.ThreeManifold.IndexCutoff.scaled_transition_bound line 104
  16. lemma OAI.ThreeManifold.IndexCutoff.field_deriv_bound line 121
  17. lemma OAI.ThreeManifold.IndexCutoff.field_eventuallyEq line 164
  18. lemma OAI.ThreeManifold.IndexCutoff.field_jet_eventuallyEq line 170
  19. def OAI.ThreeManifold.IndexForm.density line 189
  20. def OAI.ThreeManifold.IndexForm.B line 192
  21. def OAI.ThreeManifold.IndexForm.I line 194
  22. lemma OAI.ThreeManifold.IndexForm.density_continuous line 196
  23. lemma OAI.ThreeManifold.IndexForm.density_support_left line 201
  24. lemma OAI.ThreeManifold.IndexForm.density_compactSupport_left line 209
  25. lemma OAI.ThreeManifold.IndexForm.density_integrable line 213
  26. lemma OAI.ThreeManifold.IndexForm.density_symm line 218
  27. lemma OAI.ThreeManifold.IndexForm.density_quadratic line 224
  28. lemma OAI.ThreeManifold.IndexForm.index_quadratic line 238
  29. lemma OAI.ThreeManifold.IndexForm.index_cauchy_schwarz line 252
  30. lemma OAI.ThreeManifold.IndexForm.density_norm_bound line 276
  31. lemma OAI.ThreeManifold.IndexForm.bound_nonneg line 282
  32. lemma OAI.ThreeManifold.IndexForm.cutoff_integral_eq_Ioo line 287
  33. lemma OAI.ThreeManifold.IndexForm.cutoff_index_tendsto line 296
  34. lemma OAI.ThreeManifold.IndexForm.cutoff_B_tendsto line 335
  35. lemma OAI.ThreeManifold.IndexForm.jacobi_density_integral line 381
  36. lemma OAI.ThreeManifold.IndexForm.jacobi_mixed_integral_zero line 397
  37. lemma OAI.ThreeManifold.IndexForm.jacobi_initial_deriv_zero line 420
  38. lemma OAI.ThreeManifold.IndexForm.jacobi_rhs_lipschitz line 452
  39. lemma OAI.ThreeManifold.IndexForm.jacobi_zero_of_initial line 458
  40. lemma OAI.ThreeManifold.IndexForm.index_criterion line 489
  41. lemma OAI.ThreeManifold.IndexForm.interval_enlargement line 506
  42. lemma OAI.ThreeManifold.IndexForm.smooth_extension_near_interval line 515
  43. lemma OAI.ThreeManifold.IndexForm.jacobi_initial_deriv_zero_on line 533
  44. lemma OAI.ThreeManifold.IndexForm.jacobi_zero_of_initial_on line 550
  45. lemma OAI.ThreeManifold.IndexForm.index_criterion_on line 580
  46. def OAI.ThreeManifold.RiemannianCoordinates.indexPairDensity line 603
  47. def OAI.ThreeManifold.RiemannianCoordinates.indexPair line 608
  48. def OAI.ThreeManifold.RiemannianCoordinates.NonnegativeIndexOn line 611
  49. lemma OAI.ThreeManifold.RiemannianCoordinates.curvatureAlong_pairing_symm line 615
  50. lemma OAI.ThreeManifold.RiemannianCoordinates.indexPairDensity_symm line 627
  51. lemma OAI.ThreeManifold.RiemannianCoordinates.covariantDerivative_eq_zero_of_notMem_tsupport line 634
  52. lemma OAI.ThreeManifold.RiemannianCoordinates.curvatureAlong_eq_zero line 649
  53. lemma OAI.ThreeManifold.RiemannianCoordinates.indexPairDensity_support line 660
  54. lemma OAI.ThreeManifold.RiemannianCoordinates.indexPairDensity_smooth line 670
  55. lemma OAI.ThreeManifold.RiemannianCoordinates.indexPairDensity_continuous line 678
  56. lemma OAI.ThreeManifold.RiemannianCoordinates.indexPairDensity_integrable line 691
  57. lemma OAI.ThreeManifold.RiemannianCoordinates.indexPairDensity_quadratic line 699
  58. lemma OAI.ThreeManifold.RiemannianCoordinates.indexPair_quadratic line 717
  59. lemma OAI.ThreeManifold.RiemannianCoordinates.indexPair_polynomial_nonneg line 743
  60. lemma OAI.ThreeManifold.RiemannianCoordinates.indexPair_cauchy_schwarz line 759
  61. lemma OAI.ThreeManifold.RiemannianCoordinates.indexPairDensity_smul line 772
  62. lemma OAI.ThreeManifold.RiemannianCoordinates.indexDensity_smul line 783
  63. lemma OAI.ThreeManifold.RiemannianCoordinates.jacobi_indexPairDensity_hasDerivAt line 797
  64. lemma OAI.ThreeManifold.RiemannianCoordinates.jacobi_indexPair_integral line 808
  65. lemma OAI.ThreeManifold.IndexCutoff.endpoint_second_order_bound line 832
  66. lemma OAI.ThreeManifold.IndexCutoff.scaled_transition_square_bound line 857
  67. lemma OAI.ThreeManifold.IndexCutoff.cutoff_square_bound line 876
  68. lemma OAI.ThreeManifold.IndexCutoff.cutoff_deriv_mul_bound line 903
  69. lemma OAI.ThreeManifold.IndexCutoff.cutoff_jet_eventually line 928
  70. lemma OAI.ThreeManifold.IndexCutoff.cutoff_square_integral_tendsto_zero line 936
  71. lemma OAI.ThreeManifold.IndexCutoff.cutoff_mixed_integral_tendsto line 974
  72. lemma OAI.ThreeManifold.RiemannianCoordinates.cutoff_indexPair_eq_Ioo line 1017
  73. lemma OAI.ThreeManifold.RiemannianCoordinates.jacobi_cutoff_energy line 1027
  74. lemma OAI.ThreeManifold.RiemannianCoordinates.jacobi_cutoff_index_tendsto_zero line 1070
  75. lemma OAI.ThreeManifold.RiemannianCoordinates.cutoff_indexPair_tendsto line 1091
  76. def OAI.ThreeManifold.RiemannianCoordinates.chartConstantField line 1120
  77. lemma OAI.ThreeManifold.RiemannianCoordinates.chartConstantField_coordinates line 1123
  78. lemma OAI.ThreeManifold.RiemannianCoordinates.chartConstantField_smoothAt line 1129
  79. lemma OAI.ThreeManifold.RiemannianCoordinates.smooth_bump_field line 1146
  80. lemma OAI.ThreeManifold.RiemannianCoordinates.jacobi_indexPair_integral_zero line 1200
  81. lemma OAI.ThreeManifold.RiemannianCoordinates.jacobi_initial_covariantDerivative_zero line 1218
  82. theorem OAI.ThreeManifold.RiemannianCoordinates.intrinsic_index_criterion line 1231
  83. theorem OAI.ThreeManifold.RiemannianCoordinates.noConjugatePoints_of_intrinsic_index line 1240
  84. def OAI.ThreeManifold.GlobalAssembly.Passages line 1254
  85. lemma OAI.ThreeManifold.GlobalAssembly.passages_open line 1256
  86. lemma OAI.ThreeManifold.GlobalAssembly.passages_nonempty line 1261
  87. lemma OAI.ThreeManifold.GlobalAssembly.passages_connected line 1266
  88. lemma OAI.ThreeManifold.GlobalAssembly.passages_intervals line 1271
  89. lemma OAI.ThreeManifold.GlobalAssembly.passages_disjoint line 1274
  90. lemma OAI.ThreeManifold.GlobalAssembly.passages_countable line 1288
  91. lemma OAI.ThreeManifold.GlobalAssembly.passages_cover line 1291
  92. theorem OAI.ThreeManifold.GlobalAssembly.density_assembly line 1300
  93. theorem OAI.ThreeManifold.GlobalAssembly.integral_nonneg_of_passages line 1310
  94. theorem OAI.ThreeManifold.GlobalAssembly.compact_density_nonneg line 1327