OAI/Geometry/CubicTorus/Profiles/FourStarScalarGrid.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.isMinimizerAt_no_monotone_revolution line 13
  2. theorem OAI.CubicTorus.isMinimizerAt_strict_two_vertices_impossible line 77
  3. lemma OAI.CubicTorus.secondTransition_mem_Ioo_half line 116
  4. theorem OAI.CubicTorus.isMinimizerAt_second_transition_nonstandard_star line 119
  5. lemma OAI.CubicTorus.Reduction.UpperSupport.deriv_le_left_secant line 189
  6. lemma OAI.CubicTorus.Reduction.UpperSupport.power_three_halves_contact line 212
  7. theorem OAI.CubicTorus.profile_upper_support_power_secant line 222
  8. theorem OAI.CubicTorus.isoperimetricProfile_first_transition line 247
  9. lemma OAI.CubicTorus.first_transition_power_gt line 275
  10. lemma OAI.CubicTorus.transition_gap_gt line 293
  11. theorem OAI.CubicTorus.second_endpoint_support_curvature line 302
  12. theorem OAI.CubicTorus.isMinimizerAt_second_endpoint_curvature line 341
  13. theorem OAI.CubicTorus.second_endpoint_support_linear_bound line 366
  14. theorem OAI.CubicTorus.isMinimizerAt_second_endpoint_linear_bound line 400
  15. lemma OAI.CubicTorus.corner_root_basic_bound line 429
  16. lemma OAI.CubicTorus.corner_root_d_bound line 436
  17. lemma OAI.CubicTorus.corner_root_interval_bound line 443
  18. lemma OAI.CubicTorus.corner_root_simple_bound line 458
  19. lemma OAI.CubicTorus.corner_box_strict line 466
  20. lemma OAI.CubicTorus.corner_box_root_impossible line 484
  21. structure OAI.CubicTorus.CornerRootData line 510
  22. lemma OAI.CubicTorus.CornerRootData.dbound line 520
  23. lemma OAI.CubicTorus.corner_grid_0 line 524
  24. lemma OAI.CubicTorus.corner_grid_1 line 531
  25. lemma OAI.CubicTorus.corner_grid_2 line 538
  26. lemma OAI.CubicTorus.corner_grid_3 line 545
  27. lemma OAI.CubicTorus.corner_grid_4 line 552
  28. lemma OAI.CubicTorus.corner_grid_5 line 559
  29. lemma OAI.CubicTorus.corner_grid_6 line 566
  30. lemma OAI.CubicTorus.corner_grid_7 line 573
  31. lemma OAI.CubicTorus.corner_grid_8 line 580
  32. lemma OAI.CubicTorus.corner_grid_9 line 588
  33. lemma OAI.CubicTorus.corner_grid_10 line 596
  34. lemma OAI.CubicTorus.corner_grid_11 line 604
  35. lemma OAI.CubicTorus.corner_grid_12 line 612
  36. lemma OAI.CubicTorus.corner_grid_13 line 620
  37. lemma OAI.CubicTorus.corner_grid_14 line 628
  38. lemma OAI.CubicTorus.corner_grid_15 line 636
  39. lemma OAI.CubicTorus.corner_grid_16 line 643
  40. lemma OAI.CubicTorus.corner_grid_17 line 651
  41. lemma OAI.CubicTorus.corner_grid_18 line 659
  42. lemma OAI.CubicTorus.corner_grid_19 line 667
  43. lemma OAI.CubicTorus.corner_grid_20 line 675
  44. lemma OAI.CubicTorus.corner_grid_21 line 683
  45. lemma OAI.CubicTorus.corner_grid_22 line 691
  46. lemma OAI.CubicTorus.corner_grid_23 line 699
  47. lemma OAI.CubicTorus.corner_grid_24 line 707
  48. lemma OAI.CubicTorus.corner_grid_25 line 714
  49. lemma OAI.CubicTorus.corner_grid_26 line 722
  50. lemma OAI.CubicTorus.corner_grid_27 line 730
  51. lemma OAI.CubicTorus.corner_grid_28 line 738
  52. lemma OAI.CubicTorus.corner_grid_29 line 746
  53. lemma OAI.CubicTorus.corner_grid_30 line 754
  54. lemma OAI.CubicTorus.corner_grid_31 line 762
  55. lemma OAI.CubicTorus.corner_grid_32 line 770
  56. lemma OAI.CubicTorus.corner_grid_33 line 778
  57. lemma OAI.CubicTorus.corner_grid_34 line 786
  58. lemma OAI.CubicTorus.corner_grid_35 line 794
  59. lemma OAI.CubicTorus.corner_grid_36 line 802
  60. lemma OAI.CubicTorus.corner_grid_37 line 810
  61. lemma OAI.CubicTorus.corner_grid_38 line 818
  62. lemma OAI.CubicTorus.corner_grid_39 line 826
  63. lemma OAI.CubicTorus.corner_grid_40 line 834
  64. lemma OAI.CubicTorus.corner_grid_41 line 842