OAI/Geometry/WeakMTW/Support/FirstCutSupport.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.WeakMTWGlobalSupport.FirstCut.incompatible_pole_bounds line 14
  2. theorem OAI.WeakMTWGlobalSupport.FirstCut.radial_hessian_identity line 42
  3. theorem OAI.WeakMTWGlobalSupport.FirstCut.concave_linear_lower line 58
  4. theorem OAI.WeakMTWGlobalSupport.FirstCut.incompatible_transverse_pole line 77
  5. def OAI.WeakMTWGlobalSupport.FirstCut.HasTrialPole line 98
  6. theorem OAI.WeakMTWGlobalSupport.FirstCut.transverse_pairing_zero line 103
  7. theorem OAI.WeakMTWGlobalSupport.FirstCut.parallel_of_transverse_pairing_zero line 134
  8. theorem OAI.WeakMTWGlobalSupport.FirstCut.no_first_cut_kernel line 153
  9. theorem OAI.WeakMTWGlobalSupport.FirstCut.index_trial_bound line 234
  10. theorem OAI.WeakMTWGlobalSupport.FirstCut.scalar_trial_bound line 249
  11. theorem OAI.WeakMTWGlobalSupport.FirstCut.quadratic_upper_of_local_min line 258
  12. theorem OAI.WeakMTWGlobalSupport.FirstCut.two_parameter_quadratic_upper line 297
  13. theorem OAI.WeakMTWGlobalSupport.FirstCut.pole_of_smooth_index_coefficients line 331
  14. def OAI.WeakMTWGlobalSupport.JacobiIndex.integrand line 384
  15. def OAI.WeakMTWGlobalSupport.JacobiIndex.indexForm line 387
  16. theorem OAI.WeakMTWGlobalSupport.JacobiIndex.indexForm_symm line 390
  17. theorem OAI.WeakMTWGlobalSupport.JacobiIndex.continuous_integrand line 400
  18. theorem OAI.WeakMTWGlobalSupport.JacobiIndex.indexForm_jacobi line 406
  19. theorem OAI.WeakMTWGlobalSupport.JacobiIndex.indexForm_null_pairing line 429
  20. theorem OAI.WeakMTWGlobalSupport.JacobiIndex.indexForm_null_energy line 438
  21. theorem OAI.WeakMTWGlobalSupport.JacobiIndex.indexForm_trial_expansion line 448
  22. theorem OAI.WeakMTWGlobalSupport.JacobiIndex.initial_derivative_perp_radial line 474
  23. theorem OAI.WeakMTWGlobalSupport.JacobiIndex.jacobi_minimizes_index line 501
  24. def OAI.WeakMTWGlobalSupport.JacobiIndex.parameterDerivative line 535
  25. theorem OAI.WeakMTWGlobalSupport.JacobiIndex.contDiff_parameterDerivative line 539
  26. theorem OAI.WeakMTWGlobalSupport.JacobiIndex.continuous_parameterIntegral line 550
  27. theorem OAI.WeakMTWGlobalSupport.JacobiIndex.hasFDerivAt_parameterIntegral line 559
  28. theorem OAI.WeakMTWGlobalSupport.JacobiIndex.contDiff_parameterIntegral line 595
  29. theorem OAI.WeakMTWGlobalSupport.JacobiIndex.contDiff_indexForm line 617
  30. theorem OAI.WeakMTWGlobalSupport.JacobiIndex.trial_pole_from_index line 631
  31. theorem OAI.WeakMTWGlobalSupport.JacobiIndex.jacobi_eq_zero_of_initial_data line 676
  32. theorem OAI.WeakMTWGlobalSupport.FirstCut.no_first_cut_null_field line 726