OAI/Geometry/CubicTorus/Estimates/TubeCalibration.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.Periodic.isMinimizerAt_affine_volume_support line 14
  2. lemma OAI.CubicTorus.Reduction.second_deriv_nonneg_of_local_min line 38
  3. lemma OAI.CubicTorus.Reduction.second_deriv_sub line 51
  4. structure OAI.CubicTorus.Reduction.UpperSupport line 64
  5. lemma OAI.CubicTorus.Reduction.jet_comparison line 69
  6. def OAI.CubicTorus.Reduction.ode line 86
  7. lemma OAI.CubicTorus.Reduction.ode_comparison line 89
  8. theorem OAI.CubicTorus.Reduction.branch_comparison line 100
  9. theorem OAI.CubicTorus.Reduction.no_negative_support line 125
  10. lemma OAI.CubicTorus.Reduction.second_deriv_quadratic line 138
  11. theorem OAI.CubicTorus.Reduction.chord_below_of_upper_support line 152
  12. lemma OAI.CubicTorus.deriv_volume_reparam line 228
  13. lemma OAI.CubicTorus.second_deriv_volume_reparam line 239
  14. theorem OAI.CubicTorus.isoperimetricProfile_upper_support line 248
  15. theorem OAI.CubicTorus.Reduction.chord_below_of_lowerSemicontinuous_upper_support line 288
  16. theorem OAI.CubicTorus.isoperimetricProfile_chord line 366
  17. theorem OAI.CubicTorus.concaveOn_isoperimetricProfile line 374
  18. theorem OAI.CubicTorus.monotoneOn_isoperimetricProfile_half line 394
  19. theorem OAI.CubicTorus.antitoneOn_isoperimetricProfile_half line 407
  20. theorem OAI.CubicTorus.isMinimizerAt_CMC_upper_support line 429
  21. theorem OAI.CubicTorus.profile_upper_support_slope_nonneg line 462
  22. theorem OAI.CubicTorus.profile_upper_support_slope_nonpos line 476
  23. theorem OAI.CubicTorus.isMinimizerAt_CMC_sign line 490
  24. theorem OAI.CubicTorus.Periodic.profile_hessian_of_CMC line 522
  25. theorem OAI.CubicTorus.Periodic.isMinimizerAt_exact_profile_hessian line 601
  26. theorem OAI.CubicTorus.Periodic.isMinimizerAt_profile_power_jet line 633
  27. lemma OAI.CubicTorus.Reduction.second_deriv_three_halves line 678
  28. theorem OAI.CubicTorus.Reduction.UpperSupport.three_halves line 702
  29. lemma OAI.CubicTorus.candidateProfile_nonnegative line 726
  30. lemma OAI.CubicTorus.continuous_candidateProfile line 732
  31. lemma OAI.CubicTorus.candidateProfile_at_zero line 736
  32. lemma OAI.CubicTorus.candidateProfile_at_one line 739
  33. theorem OAI.CubicTorus.isoperimetricProfile_le_candidate line 742
  34. theorem OAI.CubicTorus.continuousOn_isoperimetricProfile line 755
  35. theorem OAI.CubicTorus.isoperimetricProfile_power_upper_support line 790
  36. theorem OAI.CubicTorus.concaveOn_isoperimetricProfile_three_halves line 801