OAI/Geometry/CubicTorus/Profiles/NormalTransverseLength.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.isMinimizerAt_nonstandard_missing_neighbor_flux line 13
  2. lemma OAI.CubicTorus.isMinimizerAt_missing_neighbor_top_empty line 61
  3. theorem OAI.CubicTorus.isMinimizerAt_missing_neighbor_projection line 76
  4. theorem OAI.CubicTorus.isMinimizerAt_no_face_pattern line 127
  5. def OAI.CubicTorus.normalTransverseLength line 206
  6. lemma OAI.CubicTorus.normalTransverseLength_continuous line 209
  7. lemma OAI.CubicTorus.normalTransverseLength_nonneg line 212
  8. lemma OAI.CubicTorus.normalTransverseLength_sq line 215
  9. lemma OAI.CubicTorus.normalTransverseLength_le_one line 220
  10. def OAI.CubicTorus.axialPerimeterMarginal line 225
  11. lemma OAI.CubicTorus.axialPerimeterMarginal_absolutelyContinuous line 232
  12. def OAI.CubicTorus.axialPerimeterDensity line 242
  13. lemma OAI.CubicTorus.axialPerimeterDensity_nonneg line 245
  14. lemma OAI.CubicTorus.axialPerimeterDensity_integrable line 248
  15. lemma OAI.CubicTorus.axialPerimeterDensity_measurable line 251
  16. lemma OAI.CubicTorus.axialPerimeterDensity_pairing_bounded line 254
  17. lemma OAI.CubicTorus.bounded_real_locallyIntegrable line 283
  18. lemma OAI.CubicTorus.circleSmoothApprox_bounded_contDiff line 288
  19. lemma OAI.CubicTorus.circleSmoothApprox_nonneg line 294
  20. lemma OAI.CubicTorus.circleSmoothApprox_bounded_ae_tendsto line 299
  21. lemma OAI.CubicTorus.circleSmoothApprox_lift_ae_tendsto line 306
  22. theorem OAI.CubicTorus.integrable_circle_nonneg_of_smooth_pairing line 322
  23. def OAI.CubicTorus.axialSliceIntegral line 370
  24. lemma OAI.CubicTorus.axialSliceIntegral_indicator line 373
  25. lemma OAI.CubicTorus.axialSliceIntegral_integrable line 379
  26. lemma OAI.CubicTorus.axialSliceIntegral_pairing line 385
  27. lemma OAI.CubicTorus.normal_transverse_inner_bound line 402
  28. lemma OAI.CubicTorus.axialPerimeterDensity_pairing_continuous line 422
  29. lemma OAI.CubicTorus.axial_weight_divergence line 451
  30. theorem OAI.CubicTorus.axialSliceIntegral_weighted_le line 461
  31. theorem OAI.CubicTorus.axialSliceIntegral_ae_le line 501
  32. lemma OAI.CubicTorus.axialSection_integrable line 533
  33. def OAI.CubicTorus.axialSliceFunctional line 541
  34. def OAI.CubicTorus.axialDivergenceClass line 559
  35. theorem OAI.CubicTorus.axialSliceIntegral_ae_all_le line 564
  36. def OAI.CubicTorus.axialTestPerimeter line 584
  37. theorem OAI.CubicTorus.axialTestPerimeter_ae_le line 588
  38. def OAI.CubicTorus.planeAxisEmbedding line 607
  39. def OAI.CubicTorus.planeAxisProjection line 617
  40. lemma OAI.CubicTorus.planeAxisEmbedding_same line 623
  41. lemma OAI.CubicTorus.planeAxisEmbedding_succAbove line 627
  42. lemma OAI.CubicTorus.planeAxisProjection_apply line 631
  43. lemma OAI.CubicTorus.planeAxisEmbedding_norm line 634
  44. lemma OAI.CubicTorus.planeAxisProjection_norm_le line 639
  45. lemma OAI.CubicTorus.planeAxisProjection_embedding line 646
  46. lemma OAI.CubicTorus.planeAxisProjection_single_same line 649
  47. lemma OAI.CubicTorus.planeAxisProjection_single_succAbove line 654
  48. def OAI.CubicTorus.PlanarAdmissibleField line 659
  49. def OAI.CubicTorus.liftPlanarField line 664
  50. lemma OAI.CubicTorus.liftPlanarField_admissible line 667
  51. lemma OAI.CubicTorus.liftPlanarField_same line 678
  52. lemma OAI.CubicTorus.divergence_liftPlanarField line 681
  53. lemma OAI.CubicTorus.planeAxisEmbedding_single line 703
  54. def OAI.CubicTorus.planeAxisAt line 710
  55. lemma OAI.CubicTorus.planeAxisAt_same line 713
  56. lemma OAI.CubicTorus.planeAxisAt_succAbove line 715
  57. lemma OAI.CubicTorus.planeAxisAt_contDiff line 719
  58. lemma OAI.CubicTorus.planeAxisAt_hasFDerivAt line 722
  59. def OAI.CubicTorus.tracePlanarField line 726
  60. lemma OAI.CubicTorus.tracePlanarField_admissible line 729
  61. lemma OAI.CubicTorus.planeDivergence_tracePlanarField line 743
  62. def OAI.CubicTorus.planarRepresentative line 757
  63. lemma OAI.CubicTorus.planeAxisProjection_representative line 760
  64. lemma OAI.CubicTorus.representative_axialSplit line 765
  65. def OAI.CubicTorus.planarTorusPerimeter line 772
  66. theorem OAI.CubicTorus.axialTestPerimeter_eq_planar line 776
  67. theorem OAI.CubicTorus.planarTorusPerimeter_slice_ae_le line 807
  68. def OAI.CubicTorus.planarAxialField line 825