OAI/Geometry/CubicTorus/Regularity/TranslateNormal.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.normalGraph_metric line 13
  2. lemma OAI.CubicTorus.normalGraph_projection_differential line 38
  3. lemma OAI.CubicTorus.graphUnitNormalExtension_fderiv line 48
  4. theorem OAI.CubicTorus.graphUnitNormalExtension_curvature line 66
  5. lemma OAI.CubicTorus.planeDivergence_eq_trace line 101
  6. lemma OAI.CubicTorus.cmcFlux_gradient_fderiv line 105
  7. theorem OAI.CubicTorus.graphUnitNormalExtension_divergence line 111
  8. lemma OAI.CubicTorus.planeTrace_comp_comm line 135
  9. lemma OAI.CubicTorus.planeTraceSquare_comp_comm line 145
  10. lemma OAI.CubicTorus.planeTraceSquare_symmetric line 154
  11. theorem OAI.CubicTorus.graph_curvature_nonnegative line 167
  12. lemma OAI.CubicTorus.planeTraceSquare_symmetric_eq_zero line 210
  13. theorem OAI.CubicTorus.graph_curvature_zero_fderiv_gradient line 225
  14. theorem OAI.CubicTorus.graph_curvature_zero_affine line 258
  15. theorem OAI.CubicTorus.normalMeasure_graph_normal_ae line 294
  16. def OAI.CubicTorus.translateNormal line 340
  17. lemma OAI.CubicTorus.measurable_translateNormal line 343
  18. lemma OAI.CubicTorus.translateNormal_periodic_eval line 347
  19. theorem OAI.CubicTorus.isNormalMeasure_translation line 354
  20. def OAI.CubicTorus.cmcGraphJacobi line 390
  21. lemma OAI.CubicTorus.cmcGraphJacobi_div_transform line 394
  22. theorem OAI.CubicTorus.LinearCMCEquation.normal_jacobi line 416
  23. theorem OAI.CubicTorus.cmcGraphJacobi_vertical line 432
  24. lemma OAI.CubicTorus.smooth_graph_extension line 451
  25. theorem OAI.CubicTorus.WeakCMCGraph.coordinate_jacobi_chart line 464
  26. theorem OAI.CubicTorus.actual_centered_normal_patch line 520
  27. def OAI.CubicTorus.cofactorOperator line 639
  28. lemma OAI.CubicTorus.cofactorOperator_apply line 645
  29. lemma OAI.CubicTorus.cofactorLinear_smul line 648
  30. lemma OAI.CubicTorus.cofactorLinear_inner line 654
  31. lemma OAI.CubicTorus.cofactorQuadratic_smulRight line 660
  32. lemma OAI.CubicTorus.cofactorLinear_coordinate line 676
  33. lemma OAI.CubicTorus.cofactor_field_derivative line 691
  34. lemma OAI.CubicTorus.derivative_transport line 710
  35. def OAI.CubicTorus.Periodic.variationField line 737
  36. lemma OAI.CubicTorus.Periodic.variationField_smooth line 740
  37. lemma OAI.CubicTorus.Periodic.variationField_periodic line 743
  38. lemma OAI.CubicTorus.Periodic.chainVelocity_append line 747
  39. lemma OAI.CubicTorus.Periodic.chainVelocity_smooth line 752
  40. lemma OAI.CubicTorus.Periodic.chainVelocity_periodic line 757
  41. def OAI.CubicTorus.Periodic.motionJet line 765
  42. lemma OAI.CubicTorus.Periodic.motionJet_append line 769
  43. lemma OAI.CubicTorus.Periodic.motionJet_first line 774
  44. lemma OAI.CubicTorus.Periodic.motionJet_smooth line 779
  45. lemma OAI.CubicTorus.Periodic.motionJet_periodic line 789
  46. lemma OAI.CubicTorus.Periodic.simultaneousMove_second_deriv line 797
  47. lemma OAI.CubicTorus.Periodic.chainNormalVelocity_eq_cofactor line 819
  48. def OAI.CubicTorus.volumeQuadratic line 846
  49. lemma OAI.CubicTorus.volumeQuadratic_add line 849