OAI/Geometry/CubicTorus/Profiles/NestingEndpointBound.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.Shape.uniform_coefficient line 16
  2. lemma OAI.CubicTorus.NestingGain.continuousOn_weight line 65
  3. lemma OAI.CubicTorus.NestingGain.nesting_parameters line 70
  4. lemma OAI.CubicTorus.NestingGain.pointwise_uniform_gain line 93
  5. theorem OAI.CubicTorus.NestingGain.integrated_uniform_gain line 115
  6. lemma OAI.CubicTorus.axialSectionCenter_complement line 173
  7. theorem OAI.CubicTorus.isMinimizerAt_nested_edge_bound line 185
  8. theorem OAI.CubicTorus.isMinimizerAt_bottom_nested_endpoint line 216
  9. def OAI.CubicTorus.nestingEndpointBound line 256
  10. def OAI.CubicTorus.nestingDelta line 259
  11. lemma OAI.CubicTorus.nestingDelta_mem line 261
  12. lemma OAI.CubicTorus.nestingDelta_gap line 264
  13. lemma OAI.CubicTorus.source_root_le_of_bottom line 278
  14. lemma OAI.CubicTorus.nestingEndpointBound_ge_exact line 287
  15. lemma OAI.CubicTorus.normal_graph_axis_boundary_isolated line 307
  16. lemma OAI.CubicTorus.axialSectionCorner_motion line 341
  17. lemma OAI.CubicTorus.octantHeight_endpoint_fixed line 348
  18. lemma OAI.CubicTorus.axialSectionCorner_fixed line 355
  19. theorem OAI.CubicTorus.isMinimizerAt_corner_boundary_heights_discrete line 367
  20. theorem OAI.CubicTorus.isMinimizerAt_corner_boundary_heights_null line 395
  21. def OAI.CubicTorus.unitPlanarProfile line 415
  22. lemma OAI.CubicTorus.unitPlanarProfile_zero line 418
  23. lemma OAI.CubicTorus.unitPlanarProfile_one line 421
  24. lemma OAI.CubicTorus.unitPlanarProfile_nonneg line 424
  25. lemma OAI.CubicTorus.open_outside_closure_of_not_frontier line 428
  26. theorem OAI.CubicTorus.isMinimizerAt_section_planar_profile line 433
  27. theorem OAI.CubicTorus.planarTorusPerimeter_ge_weighted_derivative_flux line 513
  28. theorem OAI.CubicTorus.planarTorusPerimeter_ge_open_derivative_flux line 647
  29. lemma OAI.CubicTorus.planar_closed_edge_collar line 701
  30. lemma OAI.CubicTorus.planar_seam_probability_bound line 722
  31. theorem OAI.CubicTorus.planarTorusPerimeter_ge_strip_seam_calibration line 772