OAI/Geometry/CubicTorus/Profiles/ProfileBounds.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ReusedScalar205.CubicTorus.Scalar.rho_rational line 20
  2. lemma OAI.ReusedScalar205.CubicTorus.Scalar.hasDerivAt_rhoRoot line 36
  3. lemma OAI.ReusedScalar205.CubicTorus.Scalar.hasDerivAt_rho line 43
  4. lemma OAI.ReusedScalar205.CubicTorus.Scalar.continuous_rho line 56
  5. lemma OAI.ReusedScalar205.CubicTorus.Scalar.contDiff_rho line 59
  6. lemma OAI.ReusedScalar205.CubicTorus.Scalar.antitoneOn_rhoSlope line 67
  7. lemma OAI.ReusedScalar205.CubicTorus.Scalar.deriv_rho_eq line 86
  8. lemma OAI.ReusedScalar205.CubicTorus.Scalar.concaveOn_rho line 88
  9. lemma OAI.ReusedScalar205.CubicTorus.Scalar.rhoSlope_nonneg line 94
  10. lemma OAI.ReusedScalar205.CubicTorus.Scalar.mul_rhoSlope_le line 98
  11. lemma OAI.ReusedScalar205.CubicTorus.Scalar.second_deriv_rho_nonpos line 106
  12. lemma OAI.ReusedScalar205.CubicTorus.Scalar.hasDerivAt_divParam line 112
  13. lemma OAI.ReusedScalar205.CubicTorus.Scalar.hasDerivAt_divParamSlope line 117
  14. lemma OAI.ReusedScalar205.CubicTorus.Scalar.second_deriv_comp_div line 124
  15. lemma OAI.ReusedScalar205.CubicTorus.Scalar.rho_comp_div_second_bound line 141
  16. lemma OAI.ReusedScalar205.CubicTorus.Reduction.second_deriv_nonneg_of_local_min line 160
  17. lemma OAI.ReusedScalar205.CubicTorus.Reduction.second_deriv_sub line 173
  18. structure OAI.ReusedScalar205.CubicTorus.Reduction.UpperSupport line 186
  19. lemma OAI.ReusedScalar205.CubicTorus.Reduction.jet_comparison line 191
  20. lemma OAI.ReusedScalar205.CubicTorus.Reduction.second_deriv_quadratic line 208
  21. theorem OAI.ReusedScalar205.CubicTorus.Reduction.chord_below_of_upper_support line 222
  22. theorem OAI.ReusedScalar205.CubicTorus.Reduction.concaveOn_of_upper_support line 292
  23. lemma OAI.ReusedScalar205.CubicTorus.Reduction.UpperSupport.sub_quadratic line 306
  24. lemma OAI.ReusedScalar205.CubicTorus.Reduction.second_deriv_half_quadratic line 314
  25. theorem OAI.ReusedScalar205.CubicTorus.Reduction.concaveOn_sub_quadratic_of_support line 318
  26. def OAI.ReusedScalar205.CubicTorus.Scalar.sectionLength line 336
  27. lemma OAI.ReusedScalar205.CubicTorus.Scalar.continuousOn_sectionLength_h line 339
  28. lemma OAI.ReusedScalar205.CubicTorus.Scalar.contDiffAt_rho_comp_div line 346
  29. lemma OAI.ReusedScalar205.CubicTorus.Scalar.second_deriv_quadratic_div line 350
  30. lemma OAI.ReusedScalar205.CubicTorus.Scalar.second_deriv_linear_div line 364
  31. lemma OAI.ReusedScalar205.CubicTorus.Scalar.sectionLength_upper_support line 372
  32. theorem OAI.ReusedScalar205.CubicTorus.Scalar.concaveOn_sectionLength_corrected line 415
  33. lemma OAI.ReusedScalar205.CubicTorus.Scalar.continuous_sectionLength_X line 427
  34. lemma OAI.ReusedScalar205.CubicTorus.Scalar.concaveOn_rho_div_corrected line 432
  35. lemma OAI.ReusedScalar205.CubicTorus.Scalar.baseline_layer_cake_set line 450
  36. theorem OAI.ReusedScalar205.CubicTorus.Scalar.concaveOn_baseline_corrected line 457
  37. def OAI.ReusedScalar205.CubicTorus.Scalar.R line 499
  38. def OAI.ReusedScalar205.CubicTorus.Scalar.RSlope line 501
  39. def OAI.ReusedScalar205.CubicTorus.Scalar.QRad line 503
  40. lemma OAI.ReusedScalar205.CubicTorus.Scalar.contDiff_t line 505
  41. lemma OAI.ReusedScalar205.CubicTorus.Scalar.deriv_t_eq line 511
  42. lemma OAI.ReusedScalar205.CubicTorus.Scalar.hasDerivAt_t line 532
  43. lemma OAI.ReusedScalar205.CubicTorus.Scalar.contDiff_R line 537
  44. lemma OAI.ReusedScalar205.CubicTorus.Scalar.hasDerivAt_R line 540
  45. lemma OAI.ReusedScalar205.CubicTorus.Scalar.monotoneOn_R line 549
  46. lemma OAI.ReusedScalar205.CubicTorus.Scalar.antitoneOn_RSlope line 554
  47. lemma OAI.ReusedScalar205.CubicTorus.Scalar.second_deriv_R_nonpos line 566
  48. lemma OAI.ReusedScalar205.CubicTorus.Scalar.lt_t_of_quadratic line 574
  49. lemma OAI.ReusedScalar205.CubicTorus.Scalar.t_lt_of_quadratic line 582
  50. lemma OAI.ReusedScalar205.CubicTorus.Scalar.gain_t_bounds line 590
  51. lemma OAI.ReusedScalar205.CubicTorus.Scalar.gain_R_bounds line 601
  52. lemma OAI.ReusedScalar205.CubicTorus.Scalar.t_positive line 630
  53. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Q_positive line 631
  54. lemma OAI.ReusedScalar205.CubicTorus.Scalar.QRad_positive line 632
  55. lemma OAI.ReusedScalar205.CubicTorus.Scalar.contDiff_Q line 634
  56. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Q_fourth line 643
  57. lemma OAI.ReusedScalar205.CubicTorus.Scalar.hasDerivAt_QRad line 659
  58. lemma OAI.ReusedScalar205.CubicTorus.Scalar.deriv_Q_eq line 664
  59. lemma OAI.ReusedScalar205.CubicTorus.Scalar.hasDerivAt_Q line 689
  60. lemma OAI.ReusedScalar205.CubicTorus.Scalar.hasDerivAt_QLogSlope line 694
  61. lemma OAI.ReusedScalar205.CubicTorus.Scalar.second_deriv_Q_eq line 700
  62. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Q_log_bounds line 710
  63. lemma OAI.ReusedScalar205.CubicTorus.Reduction.second_deriv_add line 728
  64. lemma OAI.ReusedScalar205.CubicTorus.Reduction.second_deriv_mul line 735
  65. lemma OAI.ReusedScalar205.CubicTorus.Reduction.second_deriv_cube line 753
  66. lemma OAI.ReusedScalar205.CubicTorus.Reduction.second_deriv_mul_cube line 767
  67. lemma OAI.ReusedScalar205.CubicTorus.Scalar.planar_switch_bound line 784
  68. lemma OAI.ReusedScalar205.CubicTorus.Scalar.u_upper_support line 788
  69. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cā‚€_upper_support line 815
  70. lemma OAI.ReusedScalar205.CubicTorus.Scalar.gain_cubic_jet_bound line 840
  71. lemma OAI.ReusedScalar205.CubicTorus.Scalar.gain_P_lt line 871
  72. lemma OAI.ReusedScalar205.CubicTorus.Scalar.gain_le_cappedEnergy line 879
  73. lemma OAI.ReusedScalar205.CubicTorus.Scalar.continuous_Cā‚€ line 888
  74. lemma OAI.ReusedScalar205.CubicTorus.Scalar.continuousOn_u line 890
  75. lemma OAI.ReusedScalar205.CubicTorus.Scalar.continuousOn_P line 894
  76. lemma OAI.ReusedScalar205.CubicTorus.Scalar.continuousOn_critical line 897