OAI/Geometry/CubicTorus/Profiles/SmoothSeamProbability.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.exists_smooth_seam_probability line 13
  2. theorem OAI.CubicTorus.exists_smooth_saw_primitive line 90
  3. theorem OAI.CubicTorus.planarTorusPerimeter_ge_strip_calibration line 172
  4. lemma OAI.CubicTorus.strip_sqrt_polynomial_lower line 274
  5. lemma OAI.CubicTorus.strip_round_integral_lower line 282
  6. theorem OAI.CubicTorus.planarTorusPerimeter_ge_strip_gain line 313
  7. lemma OAI.CubicTorus.planar_radial_strip_gain_first line 345
  8. lemma OAI.CubicTorus.planar_radial_strip_gain_second line 362
  9. theorem OAI.CubicTorus.isMinimizerAt_section_strip_gain line 394
  10. lemma OAI.CubicTorus.strip_gain_dominates_shape line 470
  11. lemma OAI.CubicTorus.disk_gain_dominates_shape line 479
  12. lemma OAI.CubicTorus.complement_gain_dominates_shape line 491
  13. theorem OAI.CubicTorus.isMinimizerAt_section_improved_profile line 520
  14. lemma OAI.CubicTorus.isMinimizerAt_boundary_slice_null_ae line 619
  15. theorem OAI.CubicTorus.isMinimizerAt_planar_profile_ae line 626
  16. theorem OAI.CubicTorus.isMinimizerAt_nonstandard_planar_profile line 649
  17. lemma OAI.CubicTorus.octantHeight_surjective_half line 687
  18. theorem OAI.CubicTorus.isMinimizerAt_nesting_improved_profile_ae line 697
  19. lemma OAI.CubicTorus.axialSliceIntegral_measurable line 765
  20. lemma OAI.CubicTorus.axialTestPerimeter_countable line 770
  21. theorem OAI.CubicTorus.planarTorusPerimeter_slice_measurable line 800
  22. lemma OAI.CubicTorus.axisReflection_axialSplit line 822
  23. lemma OAI.CubicTorus.axialSlice_neg_of_reflection line 832