OAI/Geometry/CubicTorus/Main.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.secondCorner_endpoint_contradiction line 12
  2. theorem OAI.CubicTorus.isMinimizerAt_second_transition_corner_excluded line 137
  3. theorem OAI.CubicTorus.isMinimizerAt_second_transition_standard line 160
  4. theorem OAI.CubicTorus.isoperimetricProfile_second_transition line 222
  5. def OAI.CubicTorus.cylinderRatio line 246
  6. lemma OAI.CubicTorus.profile_ge_second_chord line 248
  7. lemma OAI.CubicTorus.cylinder_contact_support_deriv line 262
  8. theorem OAI.CubicTorus.isMinimizerAt_cylinder_contact_multiplier line 282
  9. theorem OAI.CubicTorus.isMinimizerAt_cylinder_contact_bounds line 296
  10. def OAI.CubicTorus.criticalCorrection line 342
  11. lemma OAI.CubicTorus.criticalCorrection_convex line 344
  12. lemma OAI.CubicTorus.criticalCorrection_nonpos line 354
  13. lemma OAI.CubicTorus.criticalCorrection_rational_upper line 367
  14. lemma OAI.CubicTorus.criticalCorrection_162 line 378
  15. lemma OAI.CubicTorus.criticalCorrection_170 line 382
  16. lemma OAI.CubicTorus.criticalCorrection_190 line 386
  17. lemma OAI.CubicTorus.critical_baseline_chord line 391
  18. lemma OAI.CubicTorus.critical_baseline_positive line 411
  19. theorem OAI.CubicTorus.critical_nesting_contradiction line 430
  20. lemma OAI.CubicTorus.critical_three_vertex_parameters line 453
  21. lemma OAI.CubicTorus.critical_area_correction line 471
  22. theorem OAI.CubicTorus.isMinimizerAt_cylinder_contact_not_three_vertices line 483
  23. theorem OAI.CubicTorus.isMinimizerAt_cylinder_contact_nonstandard_star line 544
  24. theorem OAI.CubicTorus.fourCorner_normalized_contradiction line 619
  25. theorem OAI.CubicTorus.isMinimizerAt_cylinder_contact_corner_excluded line 750
  26. theorem OAI.CubicTorus.isMinimizerAt_cylinder_contact_standard line 786
  27. lemma OAI.CubicTorus.cylinder_interval_interior line 850
  28. lemma OAI.CubicTorus.profile_eq_tube_of_small_standard line 854
  29. lemma OAI.CubicTorus.cylinderRatio_eq_of_profile line 863
  30. lemma OAI.CubicTorus.cylinderRatio_first line 868
  31. lemma OAI.CubicTorus.cylinderRatio_second line 875
  32. lemma OAI.CubicTorus.cylinderRatio_contact line 882
  33. theorem OAI.CubicTorus.isoperimetricProfile_cylinder_interval line 889
  34. lemma OAI.CubicTorus.isoperimetricProfile_cylinder_contact line 918
  35. theorem OAI.CubicTorus.isMinimizerAt_cylinder_interval_standard line 926
  36. lemma OAI.CubicTorus.TwoVolume.sphereArea_three_halves line 949
  37. theorem OAI.CubicTorus.isoperimetricProfile_sphere_interval line 956
  38. theorem OAI.CubicTorus.isMinimizerAt_sphere_open_standard line 992
  39. theorem OAI.CubicTorus.isoperimetricProfile_slab_interval line 1026
  40. lemma OAI.CubicTorus.isoperimetricProfile_slab_local_min line 1041
  41. theorem OAI.CubicTorus.isMinimizerAt_small_slab_standard line 1047
  42. theorem OAI.CubicTorus.isMinimizerAt_small_volume_standard line 1071
  43. theorem OAI.CubicTorus.isMinimizerAt_all_volume_standard line 1079
  44. theorem OAI.CubicTorus.perimeter_eq_candidate_of_minimizer line 1088
  45. theorem OAI.CubicTorus.StandardRegionAt.isMinimizerAt line 1093
  46. theorem OAI.CubicTorus.unit_cubic_isoperimetric line 1103

    Distinct definitions of this name: ComparatorChallenges/CubicTorus.lean:88 (same statement text; different proof or body). Qualify references as OAI.CubicTorus.unit_cubic_isoperimetric@path.