OAI/Geometry/CubicTorus/Regularity/FiberPoint.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.coordinatePullback_norm_le line 14
  2. def OAI.CubicTorus.fiberPoint line 40
  3. lemma OAI.CubicTorus.fiberPoint_self line 43
  4. lemma OAI.CubicTorus.fiberPoint_apply_same line 46
  5. lemma OAI.CubicTorus.fiberPoint_apply_ne line 49
  6. lemma OAI.CubicTorus.norm_fiberPoint_sub line 53
  7. lemma OAI.CubicTorus.coordinateMove_fiber_strictMono line 62
  8. lemma OAI.CubicTorus.coordinateMove_mapsTo_cube line 76
  9. lemma OAI.CubicTorus.coordinateMove_image_cube line 101
  10. lemma OAI.CubicTorus.representative_quotientMap_of_mem line 151
  11. def OAI.CubicTorus.coordinateRegion line 157
  12. lemma OAI.CubicTorus.measurableSet_coordinateRegion line 160
  13. lemma OAI.CubicTorus.coordinateRegion_lift line 170
  14. lemma OAI.CubicTorus.integral_coordinateRegion line 191
  15. lemma OAI.CubicTorus.perimeter_coordinateRegion_le line 208
  16. lemma OAI.CubicTorus.finitePerimeter_coordinateRegion line 234
  17. lemma OAI.CubicTorus.realVolume_lift line 249
  18. lemma OAI.CubicTorus.volume_coordinateRegion line 255
  19. theorem OAI.CubicTorus.coordinate_variation line 278
  20. def OAI.CubicTorus.coordinateCofactor line 305
  21. lemma OAI.CubicTorus.inner_coordinatePullback line 309
  22. lemma OAI.CubicTorus.continuous_coordinateCofactor line 317
  23. theorem OAI.CubicTorus.perimeter_coordinateRegion_le_normalArea line 328
  24. def OAI.CubicTorus.coordinateNormalVelocity line 365
  25. lemma OAI.CubicTorus.coordinateCofactor_eq line 369
  26. lemma OAI.CubicTorus.continuous_coordinateNormalVelocity line 374
  27. lemma OAI.CubicTorus.hasDerivAt_norm_unit_line line 384
  28. lemma OAI.CubicTorus.lipschitz_norm_line line 392
  29. lemma OAI.CubicTorus.hasDerivAt_integral_unit_line line 402
  30. lemma OAI.CubicTorus.continuous_normalUnit line 421
  31. lemma OAI.CubicTorus.continuous_normalLine line 424
  32. theorem OAI.CubicTorus.hasDerivAt_normalArea line 432
  33. lemma OAI.CubicTorus.normalArea_zero line 450
  34. theorem OAI.CubicTorus.isMinimizerAt_coordinate_stationary line 456
  35. def OAI.CubicTorus.directionalFlux line 492
  36. lemma OAI.CubicTorus.integrableOn_directionalDeriv line 496
  37. lemma OAI.CubicTorus.directionalFlux_add line 508
  38. structure OAI.CubicTorus.WallVariation line 519
  39. lemma OAI.CubicTorus.exists_wallVariation_of_function line 528
  40. lemma OAI.CubicTorus.coordinatePullback_smul line 544
  41. lemma OAI.CubicTorus.coordinatePullback_norm_le_mul line 550
  42. def OAI.CubicTorus.doubleRegion line 568
  43. def OAI.CubicTorus.doubleCofactor line 571
  44. lemma OAI.CubicTorus.continuous_doubleCofactor line 575
  45. theorem OAI.CubicTorus.perimeter_doubleRegion_le_normalArea line 585
  46. lemma OAI.CubicTorus.directionalDeriv_norm_le line 639
  47. lemma OAI.CubicTorus.gradient_norm_le line 646
  48. lemma OAI.CubicTorus.coordinateNormalVelocity_norm_le line 652
  49. def OAI.CubicTorus.transportedFlux line 668
  50. lemma OAI.CubicTorus.transportedFlux_zero line 674
  51. lemma OAI.CubicTorus.continuousAt_transportedFlux line 679
  52. lemma OAI.CubicTorus.volume_doubleRegion line 715
  53. lemma OAI.CubicTorus.continuous_coordinateNormalVelocity_pair line 735
  54. def OAI.CubicTorus.doubleVelocityCoefficient line 744
  55. lemma OAI.CubicTorus.doubleCofactor_eq line 750
  56. lemma OAI.CubicTorus.continuous_doubleVelocityCoefficient line 755
  57. lemma OAI.CubicTorus.continuous_velocityAlong line 770
  58. lemma OAI.CubicTorus.continuousAt_doubleVelocityCoefficient line 781
  59. lemma OAI.CubicTorus.doubleVelocityCoefficient_norm_le line 786
  60. lemma OAI.CubicTorus.hasDerivAt_smul_continuous_zero line 823
  61. lemma OAI.CubicTorus.hasDerivAt_norm_unit_perturbation line 832
  62. lemma OAI.CubicTorus.norm_slope_unit_perturbation_le line 842
  63. lemma OAI.CubicTorus.hasDerivAt_integral_norm_perturbation line 856