OAI/Geometry/CubicTorus/Reflection/AxialNormalCalibration.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.regularizedNormal_norm_le line 13
  2. def OAI.CubicTorus.axialTangentPart line 20
  3. lemma OAI.CubicTorus.axialTangentPart_axis line 22
  4. lemma OAI.CubicTorus.axialTangentPart_norm_sq line 25
  5. lemma OAI.CubicTorus.inner_axialTangentPart line 33
  6. lemma OAI.CubicTorus.axialTangentPart_contDiff line 39
  7. def OAI.CubicTorus.axialNormalCalibration line 43
  8. lemma OAI.CubicTorus.axialNormalCalibration_admissible line 46
  9. lemma OAI.CubicTorus.axialNormalCalibration_axis line 55
  10. lemma OAI.CubicTorus.axialNormalCalibration_quadratic_lower line 59
  11. theorem OAI.CubicTorus.axial_slice_endpoint_calibration line 100
  12. theorem OAI.CubicTorus.isMinimizerAt_axial_endpoint_calibration line 178
  13. def OAI.CubicTorus.axialSlicePerimeter line 227
  14. lemma OAI.CubicTorus.axialSlicePerimeter_le line 231
  15. lemma OAI.CubicTorus.axialSlicePerimeter_ge line 243
  16. theorem OAI.CubicTorus.isMinimizerAt_axial_endpoint_perimeter line 248
  17. lemma OAI.CubicTorus.axialSlicePerimeter_periodic line 270
  18. def OAI.CubicTorus.axialTangentialSpeed line 294
  19. lemma OAI.CubicTorus.continuous_axialTangentialSpeed line 297
  20. lemma OAI.CubicTorus.axialTangentialSpeed_sq line 301
  21. lemma OAI.CubicTorus.normal_tangent_bound line 306
  22. def OAI.CubicTorus.axialCircleFlux line 317
  23. lemma OAI.CubicTorus.axialCircleFlux_coe line 321
  24. lemma OAI.CubicTorus.continuous_axialCircleFlux line 325
  25. lemma OAI.CubicTorus.axialCircleFlux_moment line 331
  26. lemma OAI.CubicTorus.axialCircleFlux_le_density_ae line 343
  27. def OAI.CubicTorus.axialScaledCalibration line 372
  28. lemma OAI.CubicTorus.axialScaledCalibration_admissible line 375
  29. lemma OAI.CubicTorus.axialScaledCalibration_axis line 384
  30. lemma OAI.CubicTorus.axialScaledCalibration_error line 388
  31. theorem OAI.CubicTorus.ae_iSup_le_of_lowerSemicontinuous line 435
  32. def OAI.CubicTorus.axialCirclePerimeter line 469
  33. lemma OAI.CubicTorus.axialCirclePerimeter_coe line 472
  34. lemma OAI.CubicTorus.axialCirclePerimeter_eq_iSup line 476
  35. lemma OAI.CubicTorus.lowerSemicontinuous_axialCirclePerimeter line 483
  36. theorem OAI.CubicTorus.axialCirclePerimeter_le_density_ae line 495
  37. lemma OAI.CubicTorus.axialScaledCalibration_integral_error line 537
  38. lemma OAI.CubicTorus.axialCircleFlux_integral line 563
  39. lemma OAI.CubicTorus.axialCircleFlux_le_toReal_ae line 574
  40. theorem OAI.CubicTorus.axial_bv_coarea line 596
  41. def OAI.CubicTorus.CircleSmoothDensity line 670
  42. lemma OAI.CubicTorus.CircleSmoothDensity.const_mul line 679
  43. lemma OAI.CubicTorus.CircleSmoothDensity.add line 687
  44. lemma OAI.CubicTorus.CircleSmoothDensity.ae_le line 705
  45. lemma OAI.CubicTorus.ae_forall_of_closed_parameters line 711
  46. def OAI.CubicTorus.sliceHalfAngle line 730
  47. def OAI.CubicTorus.sliceHalfAngleSlope line 731
  48. lemma OAI.CubicTorus.sqrt_one_sub_sq_pos line 734
  49. lemma OAI.CubicTorus.hasDerivAt_sliceHalfAngle line 739
  50. lemma OAI.CubicTorus.continuous_sliceHalfAngle line 752
  51. lemma OAI.CubicTorus.convexOn_sliceHalfAngle line 757
  52. lemma OAI.CubicTorus.sliceHalfAngle_support line 770
  53. lemma OAI.CubicTorus.mul_sliceHalfAngle line 787
  54. def OAI.CubicTorus.sliceSupportC line 794
  55. def OAI.CubicTorus.sliceSupportD line 796
  56. theorem OAI.CubicTorus.slice_jensen_support line 798
  57. lemma OAI.CubicTorus.slice_support_contact line 817