OAI/Geometry/CubicTorus/Profiles/SectionExtentBounds.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.isMinimizerAt_section_complement_both_extents line 13
  2. theorem OAI.CubicTorus.isMinimizerAt_bottom_both_extents line 62
  3. def OAI.CubicTorus.Nesting.lambda line 116
  4. def OAI.CubicTorus.Nesting.ell line 117
  5. def OAI.CubicTorus.Nesting.cutoff line 118
  6. def OAI.CubicTorus.Nesting.rawWeight line 119
  7. def OAI.CubicTorus.Nesting.weight line 120
  8. def OAI.CubicTorus.Nesting.fluxAux line 122
  9. def OAI.CubicTorus.Nesting.fluxAuxDeriv line 125
  10. def OAI.CubicTorus.Nesting.fluxAuxSecond line 128
  11. lemma OAI.CubicTorus.Nesting.sqrt_pos_of_mem_Ioo line 132
  12. lemma OAI.CubicTorus.Nesting.sqrt_square_of_mem_Ioo line 137
  13. lemma OAI.CubicTorus.Nesting.hasDerivAt_sqrt_one_sub_sq line 142
  14. lemma OAI.CubicTorus.Nesting.hasDerivAt_fluxAux line 152
  15. lemma OAI.CubicTorus.Nesting.hasDerivAt_fluxAuxDeriv line 166
  16. lemma OAI.CubicTorus.Nesting.fluxAuxSecond_nonneg line 181
  17. lemma OAI.CubicTorus.Nesting.continuousOn_fluxAux line 201
  18. lemma OAI.CubicTorus.Nesting.convexOn_fluxAux line 210
  19. lemma OAI.CubicTorus.Nesting.cutoff_pos line 224
  20. lemma OAI.CubicTorus.Nesting.cutoff_sq line 228
  21. lemma OAI.CubicTorus.Nesting.cutoff_lt_one line 231
  22. lemma OAI.CubicTorus.Nesting.sqrt_cutoff line 234
  23. lemma OAI.CubicTorus.Nesting.rawWeight_cutoff line 238
  24. lemma OAI.CubicTorus.Nesting.rawWeight_lower line 242
  25. lemma OAI.CubicTorus.Nesting.hasDerivAt_rawWeight line 250
  26. lemma OAI.CubicTorus.Nesting.continuousOn_rawWeight line 263
  27. lemma OAI.CubicTorus.Nesting.antitoneOn_rawWeight line 272
  28. lemma OAI.CubicTorus.Nesting.weight_mem line 287
  29. lemma OAI.CubicTorus.Nesting.antitoneOn_weight line 295
  30. lemma OAI.CubicTorus.Nesting.weight_le_rawWeight line 301
  31. lemma OAI.CubicTorus.Nesting.fluxAux_weight_nonneg line 307
  32. theorem OAI.CubicTorus.Nesting.integrated_flux_probability line 320
  33. lemma OAI.CubicTorus.Nesting.product_sqrt_le_half line 351
  34. lemma OAI.CubicTorus.Nesting.product_sqrt_le_of_lower line 356
  35. lemma OAI.CubicTorus.Nesting.weight_derivative_bound_of_row line 370
  36. theorem OAI.CubicTorus.Nesting.weight_derivative_bound line 387
  37. def OAI.CubicTorus.Nesting.squaredWeight line 418
  38. lemma OAI.CubicTorus.Nesting.hasDerivAt_squaredWeight line 420
  39. lemma OAI.CubicTorus.Nesting.squaredWeight_eq_rawWeight line 434
  40. lemma OAI.CubicTorus.Nesting.squaredWeight_difference line 438
  41. theorem OAI.CubicTorus.Nesting.pointwise_weight_gain line 467
  42. def OAI.CubicTorus.Shape.t line 501
  43. def OAI.CubicTorus.Shape.c line 502
  44. def OAI.CubicTorus.Shape.dm line 503
  45. def OAI.CubicTorus.Shape.u line 504
  46. def OAI.CubicTorus.Shape.theta line 505
  47. def OAI.CubicTorus.Shape.shape line 506
  48. def OAI.CubicTorus.Shape.moment line 507
  49. def OAI.CubicTorus.Shape.firstMoment line 508
  50. def OAI.CubicTorus.Shape.meanQ line 509
  51. def OAI.CubicTorus.Shape.pā‚‚ line 510
  52. lemma OAI.CubicTorus.Shape.positive_quadratic_root line 512
  53. lemma OAI.CubicTorus.Shape.t_spec line 528
  54. lemma OAI.CubicTorus.Shape.extent_lower_bound line 532
  55. lemma OAI.CubicTorus.Shape.endpoint_slack_bound line 548
  56. theorem OAI.CubicTorus.Shape.interval_placement line 576
  57. lemma OAI.CubicTorus.Shape.theta_spec line 611
  58. lemma OAI.CubicTorus.Shape.theta_bounds line 614
  59. lemma OAI.CubicTorus.Shape.shape_on_left line 630
  60. lemma OAI.CubicTorus.Shape.shape_on_right line 639
  61. lemma OAI.CubicTorus.Shape.shape_nonneg line 649
  62. lemma OAI.CubicTorus.Shape.shape_le_one line 653
  63. lemma OAI.CubicTorus.Shape.shape_max line 657
  64. lemma OAI.CubicTorus.Shape.continuous_shape line 667
  65. lemma OAI.CubicTorus.Shape.integral_eq_split line 671
  66. lemma OAI.CubicTorus.Shape.moment_eq line 700
  67. lemma OAI.CubicTorus.Shape.firstMoment_eq line 706
  68. lemma OAI.CubicTorus.Shape.moment_pos line 738
  69. lemma OAI.CubicTorus.Shape.meanQ_eq line 745
  70. lemma OAI.CubicTorus.Shape.meanQ_mem line 754
  71. theorem OAI.CubicTorus.Shape.moment_bounds line 765
  72. lemma OAI.CubicTorus.Shape.affine_shape_integral line 782
  73. lemma OAI.CubicTorus.Shape.cubic_shape_lower line 795
  74. lemma OAI.CubicTorus.Shape.cubic_shape_lower_dm line 826
  75. lemma OAI.CubicTorus.Shape.pā‚‚_pos line 840
  76. lemma OAI.CubicTorus.Shape.coefficient_lower line 844