OAI/Geometry/CubicTorus/Reflection/RevolutionTangents.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.first_transition_nonstandard_revolution line 13
  2. def OAI.CubicTorus.revolutionPoint line 49
  3. lemma OAI.CubicTorus.unitAngle_zero line 52
  4. lemma OAI.CubicTorus.revolutionPoint_meridian_deriv line 54
  5. lemma OAI.CubicTorus.revolutionPoint_angle_deriv line 60
  6. lemma OAI.CubicTorus.revolutionPoint_zero_meridian_deriv line 71
  7. lemma OAI.CubicTorus.revolutionPoint_zero_angle_deriv line 79
  8. theorem OAI.CubicTorus.isMinimizerAt_revolution_tangents line 86
  9. theorem OAI.CubicTorus.isMinimizerAt_revolution_meridian_normal line 111
  10. lemma OAI.CubicTorus.unitSquareScale_zero line 151
  11. lemma OAI.CubicTorus.coverCoordinateReflection_section_zero line 154
  12. lemma OAI.CubicTorus.TrueRadialTube.radius_eq_of_boundary line 159
  13. theorem OAI.CubicTorus.TrueRadialTube.axial_even line 170
  14. theorem OAI.CubicTorus.TrueRadialTube.deriv_negative_chamber line 184
  15. theorem OAI.CubicTorus.first_transition_nonstandard_monotone_revolution line 235
  16. lemma OAI.CubicTorus.revolution_normal_divergence line 277
  17. lemma OAI.CubicTorus.hasDerivAt_delaunay_first_integral line 374
  18. theorem OAI.CubicTorus.delaunay_first_integral line 392
  19. lemma OAI.CubicTorus.delaunay_first_integral_endpoints line 405
  20. lemma OAI.CubicTorus.delaunay_slope_product line 418
  21. lemma OAI.CubicTorus.hasDerivAt_delaunay_slope line 433
  22. lemma OAI.CubicTorus.continuous_const_of_sq_eq_one line 470
  23. theorem OAI.CubicTorus.revolution_classical_CMC line 486
  24. theorem OAI.CubicTorus.TrueRadialTube.exists_revolution_CMC line 537
  25. def OAI.CubicTorus.axisRadialField line 585
  26. lemma OAI.CubicTorus.axisRadialField_contDiff line 590
  27. lemma OAI.CubicTorus.axisRadialField_periodic line 600
  28. lemma OAI.CubicTorus.divergence_axisRadialField line 611
  29. lemma OAI.CubicTorus.axisRadialField_zero line 636
  30. lemma OAI.CubicTorus.axisRadialField_one line 638
  31. lemma OAI.CubicTorus.axisRadialField_two line 640
  32. lemma OAI.CubicTorus.TrueRadialTube.revolution_section line 655
  33. lemma OAI.CubicTorus.TrueRadialTube.revolution_section_volume line 666
  34. lemma OAI.CubicTorus.TrueRadialTube.revolution_radius_bound line 678
  35. theorem OAI.CubicTorus.TrueRadialTube.revolution_volume line 688
  36. theorem OAI.CubicTorus.isMinimizerAt_boundary_flux_le line 719
  37. lemma OAI.CubicTorus.TrueRadialTube.axisRadialField_boundary_bound line 755
  38. theorem OAI.CubicTorus.TrueRadialTube.axisRadialField_flux line 791