OAI/Geometry/CubicTorus/Profiles/NestingBaseline.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.isMinimizerAt_measurable_weighted_area_bound line 13
  2. lemma OAI.CubicTorus.isMinimizerAt_missing_neighbor_slice_empty line 82
  3. theorem OAI.CubicTorus.isMinimizerAt_missing_neighbor_area_flux line 97
  4. theorem OAI.CubicTorus.isMinimizerAt_sharp_section_weight_ae line 161
  5. theorem OAI.CubicTorus.isMinimizerAt_missing_neighbor_sharp_area_flux line 184
  6. theorem OAI.CubicTorus.isMinimizerAt_improved_section_weight_ae line 214
  7. theorem OAI.CubicTorus.isMinimizerAt_missing_neighbor_improved_area_flux line 259
  8. lemma OAI.CubicTorus.unitPlanarProfile_middle line 297
  9. lemma OAI.CubicTorus.sharpSectionWeight_middle line 312
  10. lemma OAI.CubicTorus.improvedSectionWeight_ge_sharp line 325
  11. lemma OAI.CubicTorus.sharpSectionWeight_mem line 343
  12. lemma OAI.CubicTorus.improvedSectionWeight_integrable line 350
  13. lemma OAI.CubicTorus.sharpSectionWeight_integrable line 356
  14. theorem OAI.CubicTorus.improvedSectionWeight_area_gain line 361
  15. theorem OAI.CubicTorus.isMinimizerAt_nesting_cubic_gain line 414
  16. def OAI.CubicTorus.nestingBaseline line 455
  17. def OAI.CubicTorus.nestingC0 line 458
  18. def OAI.CubicTorus.nestingP line 459
  19. def OAI.CubicTorus.nestingQ line 460
  20. def OAI.CubicTorus.nestingExcess line 461
  21. def OAI.CubicTorus.nestingGainInfimum line 464
  22. lemma OAI.CubicTorus.nestingExcess_nonneg line 466
  23. lemma OAI.CubicTorus.nestingGainInfimum_le line 471
  24. lemma OAI.CubicTorus.nestingExcess_at_sqrt line 475
  25. lemma OAI.CubicTorus.sharpSectionWeight_ge_ell line 483
  26. lemma OAI.CubicTorus.nestingBaseline_slack line 489
  27. lemma OAI.CubicTorus.nestingGainInfimum_actual_slack line 501
  28. theorem OAI.CubicTorus.isMinimizerAt_nesting_area_bound line 518
  29. lemma OAI.CubicTorus.axialSectionCorner_bottom_eq line 562
  30. lemma OAI.CubicTorus.axialSectionCorner_bottom_far line 574
  31. lemma OAI.CubicTorus.axialSectionCorner_bottom_axis line 582
  32. theorem OAI.CubicTorus.isMinimizerAt_three_vertex_bottom line 596
  33. def OAI.CubicTorus.phi line 632
  34. lemma OAI.CubicTorus.phi_deriv line 634
  35. lemma OAI.CubicTorus.phi_mono line 639
  36. lemma OAI.CubicTorus.phi_anti line 646
  37. theorem OAI.CubicTorus.three_vertex_parameter_algebra line 654
  38. lemma OAI.CubicTorus.isMinimizerAt_perimeter_half_le_one line 741
  39. theorem OAI.CubicTorus.isMinimizerAt_three_vertex_parameters line 750
  40. theorem OAI.CubicTorus.isMinimizerAt_nonstandard_integrated_flux line 802