OAI/Geometry/CubicTorus/Estimates/RadialSectionArea.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicTorus.centeredPlaneSection line 13
  2. lemma OAI.CubicTorus.norm_smul_unitAngle_arg line 16
  3. lemma OAI.CubicTorus.radius_le_squareScale_of_gauge line 22
  4. lemma OAI.CubicTorus.planarRadialRegion_eq_actual_section line 31
  5. theorem OAI.CubicTorus.isMinimizerAt_actual_radial_section_area line 58
  6. lemma OAI.CubicTorus.axialNormalCalibration_eq_of_unit_axis_zero line 102
  7. lemma OAI.CubicTorus.isMinimizerAt_normal_corner_section_zero line 107
  8. theorem OAI.CubicTorus.isMinimizerAt_endpoint_radial_calibration_density line 127
  9. theorem OAI.CubicTorus.isMinimizerAt_endpoint_radial_green line 166
  10. lemma OAI.CubicTorus.coordinatePlaneProjection_axialTangent line 203
  11. lemma OAI.CubicTorus.coordinatePlaneProjection_norm_le line 207
  12. lemma OAI.CubicTorus.coordinatePlaneProjection_norm_tangent line 211
  13. lemma OAI.CubicTorus.axialTangentPart_smul line 217
  14. lemma OAI.CubicTorus.regularizedNormal_unit_of_large line 221
  15. lemma OAI.CubicTorus.scaled_axialCalibration_density line 226
  16. lemma OAI.CubicTorus.compact_positive_scale line 257
  17. lemma OAI.CubicTorus.periodic_integral_unit_translate line 282
  18. lemma OAI.CubicTorus.bounded_integrable_rectangle line 289
  19. lemma OAI.CubicTorus.bounded_integrable_unit_square line 298
  20. lemma OAI.CubicTorus.periodic_plane_integral_translate line 303
  21. lemma OAI.CubicTorus.axialSplit_zero_symm line 322
  22. lemma OAI.CubicTorus.tubeSplit_symm_one line 327
  23. lemma OAI.CubicTorus.tubeSplit_symm_two line 330
  24. lemma OAI.CubicTorus.coordinateSectionPoint_coordinates line 333
  25. lemma OAI.CubicTorus.centered_complex_integral_periodic line 340
  26. lemma OAI.CubicTorus.centeredPlaneSection_integral line 411
  27. lemma OAI.CubicTorus.axialSectionIntegral_one line 440
  28. lemma OAI.CubicTorus.centeredPlaneSection_real_volume line 451
  29. lemma OAI.CubicTorus.complexDet_le_norm_mul line 469
  30. lemma OAI.CubicTorus.radialVelocity_continuous line 473
  31. lemma OAI.CubicTorus.radialVelocity_norm line 478
  32. lemma OAI.CubicTorus.axialSectionIntegral_radial_green line 482
  33. lemma OAI.CubicTorus.axialSlicePerimeter_radial_le line 495
  34. lemma OAI.CubicTorus.axialSlicePerimeter_radial_eq_of_calibration line 520
  35. lemma OAI.CubicTorus.isMinimizerAt_radial_normal_positive line 553
  36. theorem OAI.CubicTorus.isMinimizerAt_radial_slice_calibration line 576
  37. theorem OAI.CubicTorus.isMinimizerAt_radial_slice_length line 624
  38. lemma OAI.CubicTorus.isMinimizerAt_centered_section_empty line 670
  39. theorem OAI.CubicTorus.isMinimizerAt_slice_isoperimetric line 703
  40. theorem OAI.CubicTorus.isMinimizerAt_slice_sqrt_isoperimetric line 731
  41. theorem OAI.CubicTorus.isMinimizerAt_smooth_radial_section_of_level_vertices line 767