OAI/Geometry/CubicTorus/Profiles/AtanPoly.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.isMinimizerAt_nonstandard_sharp_flux line 13
  2. theorem OAI.CubicTorus.isMinimizerAt_nonstandard_three_vertex_nesting line 69
  3. def OAI.ReusedScalar205.CubicTorus.Arithmetic.atanPoly line 143
  4. lemma OAI.ReusedScalar205.CubicTorus.Arithmetic.atan_terms_antitone line 146
  5. lemma OAI.ReusedScalar205.CubicTorus.Arithmetic.atanPoly_bounds line 155
  6. def OAI.ReusedScalar205.CubicTorus.Arithmetic.atanHalf line 169
  7. lemma OAI.ReusedScalar205.CubicTorus.Arithmetic.atanHalf_spec line 171
  8. def OAI.ReusedScalar205.CubicTorus.Arithmetic.asinQuarterArg line 190
  9. lemma OAI.ReusedScalar205.CubicTorus.Arithmetic.arcsin_quarter line 193
  10. lemma OAI.ReusedScalar205.CubicTorus.Arithmetic.arcsin_enclosure line 218
  11. def OAI.ReusedScalar205.CubicTorus.Arithmetic.Encl line 231
  12. lemma OAI.ReusedScalar205.CubicTorus.Arithmetic.Encl.exact line 233
  13. lemma OAI.ReusedScalar205.CubicTorus.Arithmetic.Encl.widen line 235
  14. lemma OAI.ReusedScalar205.CubicTorus.Arithmetic.Encl.neg line 238
  15. lemma OAI.ReusedScalar205.CubicTorus.Arithmetic.Encl.add line 241
  16. lemma OAI.ReusedScalar205.CubicTorus.Arithmetic.Encl.sub line 245
  17. lemma OAI.ReusedScalar205.CubicTorus.Arithmetic.Encl.mul_nonneg line 249
  18. lemma OAI.ReusedScalar205.CubicTorus.Arithmetic.Encl.square line 254
  19. lemma OAI.ReusedScalar205.CubicTorus.Arithmetic.Encl.div_nonneg line 258
  20. lemma OAI.ReusedScalar205.CubicTorus.Arithmetic.Encl.sqrt line 270
  21. lemma OAI.ReusedScalar205.CubicTorus.Arithmetic.Encl.min line 275
  22. lemma OAI.ReusedScalar205.CubicTorus.Arithmetic.Encl.arcsin line 279
  23. lemma OAI.ReusedScalar205.CubicTorus.Arithmetic.Encl.mul_nonpos_nonneg line 290
  24. lemma OAI.ReusedScalar205.CubicTorus.Arithmetic.Encl.mul_nonneg_nonpos line 297
  25. lemma OAI.ReusedScalar205.CubicTorus.Arithmetic.Encl.mul_nonpos line 302
  26. lemma OAI.ReusedScalar205.CubicTorus.Arithmetic.Encl.div_nonpos line 309
  27. lemma OAI.ReusedScalar205.CubicTorus.Arithmetic.Encl.pow line 319
  28. def OAI.ReusedScalar205.CubicTorus.Nesting.lambda line 330
  29. def OAI.ReusedScalar205.CubicTorus.Nesting.ell line 331
  30. def OAI.ReusedScalar205.CubicTorus.Nesting.cutoff line 332
  31. def OAI.ReusedScalar205.CubicTorus.Nesting.rawWeight line 333
  32. def OAI.ReusedScalar205.CubicTorus.Nesting.weight line 334
  33. def OAI.ReusedScalar205.CubicTorus.Nesting.fluxAux line 336
  34. def OAI.ReusedScalar205.CubicTorus.Nesting.fluxAuxDeriv line 339
  35. def OAI.ReusedScalar205.CubicTorus.Nesting.fluxAuxSecond line 342
  36. lemma OAI.ReusedScalar205.CubicTorus.Nesting.sqrt_pos_of_mem_Ioo line 346
  37. lemma OAI.ReusedScalar205.CubicTorus.Nesting.sqrt_square_of_mem_Ioo line 351
  38. lemma OAI.ReusedScalar205.CubicTorus.Nesting.hasDerivAt_sqrt_one_sub_sq line 356
  39. lemma OAI.ReusedScalar205.CubicTorus.Nesting.hasDerivAt_fluxAux line 366
  40. lemma OAI.ReusedScalar205.CubicTorus.Nesting.hasDerivAt_fluxAuxDeriv line 380
  41. lemma OAI.ReusedScalar205.CubicTorus.Nesting.fluxAuxSecond_nonneg line 395
  42. lemma OAI.ReusedScalar205.CubicTorus.Nesting.continuousOn_fluxAux line 415
  43. lemma OAI.ReusedScalar205.CubicTorus.Nesting.convexOn_fluxAux line 424
  44. lemma OAI.ReusedScalar205.CubicTorus.Nesting.cutoff_pos line 438
  45. lemma OAI.ReusedScalar205.CubicTorus.Nesting.cutoff_sq line 442
  46. lemma OAI.ReusedScalar205.CubicTorus.Nesting.cutoff_lt_one line 445
  47. lemma OAI.ReusedScalar205.CubicTorus.Nesting.sqrt_cutoff line 448
  48. lemma OAI.ReusedScalar205.CubicTorus.Nesting.rawWeight_cutoff line 452
  49. lemma OAI.ReusedScalar205.CubicTorus.Nesting.rawWeight_lower line 456
  50. lemma OAI.ReusedScalar205.CubicTorus.Nesting.hasDerivAt_rawWeight line 464
  51. lemma OAI.ReusedScalar205.CubicTorus.Nesting.continuousOn_rawWeight line 477
  52. lemma OAI.ReusedScalar205.CubicTorus.Nesting.antitoneOn_rawWeight line 486
  53. lemma OAI.ReusedScalar205.CubicTorus.Nesting.weight_mem line 501
  54. lemma OAI.ReusedScalar205.CubicTorus.Nesting.antitoneOn_weight line 509
  55. lemma OAI.ReusedScalar205.CubicTorus.Nesting.weight_le_rawWeight line 515
  56. lemma OAI.ReusedScalar205.CubicTorus.Nesting.fluxAux_weight_nonneg line 521
  57. theorem OAI.ReusedScalar205.CubicTorus.Nesting.integrated_flux_probability line 534
  58. lemma OAI.ReusedScalar205.CubicTorus.Nesting.product_sqrt_le_half line 565
  59. lemma OAI.ReusedScalar205.CubicTorus.Nesting.product_sqrt_le_of_lower line 570
  60. lemma OAI.ReusedScalar205.CubicTorus.Nesting.weight_derivative_bound_of_row line 584
  61. theorem OAI.ReusedScalar205.CubicTorus.Nesting.weight_derivative_bound line 601
  62. def OAI.ReusedScalar205.CubicTorus.Nesting.squaredWeight line 632
  63. lemma OAI.ReusedScalar205.CubicTorus.Nesting.hasDerivAt_squaredWeight line 634
  64. lemma OAI.ReusedScalar205.CubicTorus.Nesting.squaredWeight_eq_rawWeight line 648
  65. lemma OAI.ReusedScalar205.CubicTorus.Nesting.squaredWeight_difference line 652
  66. theorem OAI.ReusedScalar205.CubicTorus.Nesting.pointwise_weight_gain line 681
  67. def OAI.ReusedScalar205.CubicTorus.Shape.t line 715
  68. def OAI.ReusedScalar205.CubicTorus.Shape.c line 716
  69. def OAI.ReusedScalar205.CubicTorus.Shape.dm line 717
  70. def OAI.ReusedScalar205.CubicTorus.Shape.u line 718
  71. def OAI.ReusedScalar205.CubicTorus.Shape.theta line 719
  72. def OAI.ReusedScalar205.CubicTorus.Shape.shape line 720
  73. def OAI.ReusedScalar205.CubicTorus.Shape.moment line 721
  74. def OAI.ReusedScalar205.CubicTorus.Shape.firstMoment line 722
  75. def OAI.ReusedScalar205.CubicTorus.Shape.meanQ line 723
  76. def OAI.ReusedScalar205.CubicTorus.Shape.pā‚‚ line 724
  77. lemma OAI.ReusedScalar205.CubicTorus.Shape.positive_quadratic_root line 726
  78. lemma OAI.ReusedScalar205.CubicTorus.Shape.t_spec line 742
  79. lemma OAI.ReusedScalar205.CubicTorus.Shape.extent_lower_bound line 746
  80. lemma OAI.ReusedScalar205.CubicTorus.Shape.endpoint_slack_bound line 762
  81. theorem OAI.ReusedScalar205.CubicTorus.Shape.interval_placement line 790
  82. lemma OAI.ReusedScalar205.CubicTorus.Shape.theta_spec line 825
  83. lemma OAI.ReusedScalar205.CubicTorus.Shape.theta_bounds line 828
  84. lemma OAI.ReusedScalar205.CubicTorus.Shape.shape_on_left line 844
  85. lemma OAI.ReusedScalar205.CubicTorus.Shape.shape_on_right line 853