OAI/Geometry/CubicTorus/Regularity/SurfaceH1Translation.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.translateNormal_measurePreserving line 13
  2. def OAI.CubicTorus.normalTranslationLp line 18
  3. lemma OAI.CubicTorus.normalTranslationLp_ae line 24
  4. def OAI.CubicTorus.smoothScalarTranslate line 30
  5. lemma OAI.CubicTorus.gradient_smoothScalarTranslate line 35
  6. lemma OAI.CubicTorus.smoothScalarTranslate_translate_value line 39
  7. lemma OAI.CubicTorus.smoothScalarTranslate_translate_gradient line 46
  8. def OAI.CubicTorus.surfaceJetPullTranslation line 59
  9. lemma OAI.CubicTorus.surfaceJetPullTranslation_smooth line 68
  10. lemma OAI.CubicTorus.smoothScalarTranslate_neg_cancel line 90
  11. lemma OAI.CubicTorus.surfaceH1_translation_pull line 97
  12. theorem OAI.CubicTorus.surfaceH1_translation_lift line 107
  13. lemma OAI.CubicTorus.normalProjection_translate line 132
  14. lemma OAI.CubicTorus.normalTranslationLp_multiplier line 138
  15. lemma OAI.CubicTorus.surfaceJacobiB_translation_pull line 155
  16. lemma OAI.CubicTorus.surfaceCurvatureLp_translation line 170
  17. theorem OAI.CubicTorus.surfaceH1_jacobi_translation_lift line 202
  18. lemma OAI.CubicTorus.surfaceH1_translation_value line 218
  19. theorem OAI.CubicTorus.isMinimizerAt_H1_jacobi_smooth line 250
  20. def OAI.CubicTorus.planeFrameOperator line 338
  21. lemma OAI.CubicTorus.smooth_line_deriv line 342
  22. lemma OAI.CubicTorus.smooth_line_second_deriv line 348
  23. lemma OAI.CubicTorus.plane_hessian_nonneg_of_local_min line 361
  24. lemma OAI.CubicTorus.planeFrameOperator_nonneg_of_local_min line 375
  25. lemma OAI.CubicTorus.planeFrameOperator_sub line 382
  26. lemma OAI.CubicTorus.planeFrameOperator_smul line 396
  27. theorem OAI.CubicTorus.planeFrameOperator_annulus_comparison line 408
  28. abbrev OAI.CubicTorus.PlaneSmooth line 461
  29. lemma OAI.CubicTorus.planeDivergence_sub line 463
  30. lemma OAI.CubicTorus.planeDivergence_contDiff line 470
  31. def OAI.CubicTorus.planeElliptic line 478
  32. def OAI.CubicTorus.planeDrift line 481
  33. lemma OAI.CubicTorus.planeElliptic_contDiff line 484
  34. lemma OAI.CubicTorus.planeDrift_contDiff line 488
  35. lemma OAI.CubicTorus.planeDrift_compact line 492
  36. lemma OAI.CubicTorus.planeDivergence_compact line 498
  37. lemma OAI.CubicTorus.planeElliptic_compact line 504
  38. lemma OAI.CubicTorus.planeDivergence_integral_zero line 511
  39. def OAI.CubicTorus.planeEnergy line 546
  40. lemma OAI.CubicTorus.planeEnergy_contDiff line 549
  41. lemma OAI.CubicTorus.planeEnergy_compact line 553
  42. lemma OAI.CubicTorus.planeEnergy_fderiv line 559
  43. lemma OAI.CubicTorus.planeDrift_fderiv line 573
  44. def OAI.CubicTorus.planeRellichFlux line 585
  45. lemma OAI.CubicTorus.planeRellichFlux_contDiff line 591
  46. lemma OAI.CubicTorus.planeRellichFlux_compact line 602
  47. theorem OAI.CubicTorus.planeRellichFlux_divergence line 612
  48. def OAI.CubicTorus.planeCarlemanS line 659
  49. def OAI.CubicTorus.planeCarlemanT line 662
  50. def OAI.CubicTorus.planeCarlemanP line 665
  51. def OAI.CubicTorus.planeCarlemanR line 669
  52. def OAI.CubicTorus.planeCarlemanFlux line 673
  53. lemma OAI.CubicTorus.planeCarlemanFlux_contDiff line 677
  54. lemma OAI.CubicTorus.planeCarlemanFlux_compact line 686
  55. lemma OAI.CubicTorus.planeCarlemanP_contDiff line 699
  56. lemma OAI.CubicTorus.planeCarlemanP_compact line 709
  57. theorem OAI.CubicTorus.planeCarleman_pointwise line 717
  58. theorem OAI.CubicTorus.planeCarleman_integral line 743
  59. lemma OAI.CubicTorus.carleman_scalar_coercivity line 777
  60. structure OAI.CubicTorus.PlaneCarlemanData line 814
  61. lemma OAI.CubicTorus.plane_energy_flux_divergence line 824
  62. theorem OAI.CubicTorus.planeCarleman_coercive line 831