OAI/Geometry/CubicTorus/Estimates/SurfaceJet.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.Periodic.isMinimizerAt_power_affine_standard_ball line 13
  2. abbrev OAI.CubicTorus.SurfaceJet line 33
  3. def OAI.CubicTorus.surfaceMultiplier line 36
  4. def OAI.CubicTorus.surfaceJacobiB line 45
  5. lemma OAI.CubicTorus.surfaceJacobiB_continuous line 49
  6. lemma OAI.CubicTorus.surfaceJacobiB_symm line 55
  7. lemma OAI.CubicTorus.surfaceJacobiB_add_left line 72
  8. lemma OAI.CubicTorus.surfaceJacobiB_smul_left line 78
  9. theorem OAI.CubicTorus.surfaceJacobi_zero_polarizes line 86
  10. def OAI.CubicTorus.smoothPeriodicScalars line 126
  11. def OAI.CubicTorus.smoothScalarValue line 136
  12. def OAI.CubicTorus.smoothScalarGradient line 139
  13. lemma OAI.CubicTorus.smoothScalarGradient_add line 146
  14. lemma OAI.CubicTorus.smoothScalarGradient_smul line 159
  15. def OAI.CubicTorus.surfaceSmoothJet line 170
  16. def OAI.CubicTorus.surfaceH1 line 189
  17. def OAI.CubicTorus.surfaceCurvatureLp line 192
  18. lemma OAI.CubicTorus.surfaceSmoothJet_jacobi line 198
  19. def OAI.CubicTorus.smoothScalarOne line 237
  20. def OAI.CubicTorus.surfaceOne line 239
  21. def OAI.CubicTorus.surfaceMean line 242
  22. lemma OAI.CubicTorus.surfaceMean_of_smooth line 245
  23. lemma OAI.CubicTorus.surfaceMean_one line 256
  24. lemma OAI.CubicTorus.surfaceOne_mem line 261
  25. def OAI.CubicTorus.surfaceCenter line 264
  26. lemma OAI.CubicTorus.continuous_surfaceCenter line 267
  27. lemma OAI.CubicTorus.surfaceMean_center line 271
  28. lemma OAI.CubicTorus.surfaceCenter_mem line 278
  29. lemma OAI.CubicTorus.surfaceCenter_of_smooth line 282
  30. lemma OAI.CubicTorus.surfaceCenter_eq_self line 288
  31. theorem OAI.CubicTorus.surfaceH1_stability_of_smooth line 303
  32. theorem OAI.CubicTorus.Periodic.isMinimizerAt_H1_trace_stability line 339
  33. def OAI.CubicTorus.surfaceH1ZeroMean line 371
  34. theorem OAI.CubicTorus.surfaceH1_zero_mode_constant line 374
  35. theorem OAI.CubicTorus.surfaceH1_zero_mode_homogeneous line 399
  36. theorem OAI.CubicTorus.isMinimizerAt_positive_patch_test line 428
  37. lemma OAI.CubicTorus.surfaceJacobiB_unused_patch line 451
  38. theorem OAI.CubicTorus.isMinimizerAt_H1_unused_patch_homogeneous line 488
  39. lemma OAI.CubicTorus.cover_gradient_mul line 520
  40. def OAI.CubicTorus.smoothScalarMul line 531
  41. lemma OAI.CubicTorus.smoothScalarGradient_mul line 535
  42. lemma OAI.CubicTorus.surfaceSmoothJet_bilinear line 546
  43. lemma OAI.CubicTorus.graph_shape_metric_symmetric line 591
  44. theorem OAI.CubicTorus.graph_normal_tangent_symmetric line 610
  45. theorem OAI.CubicTorus.isMinimizerAt_shape_tangent_symmetric line 660
  46. lemma OAI.CubicTorus.normal_tangent_trace_norm line 688
  47. lemma OAI.CubicTorus.gradient_normal_component line 754
  48. def OAI.CubicTorus.normalComponentScalar line 766
  49. lemma OAI.CubicTorus.normalComponentScalar_apply line 770
  50. lemma OAI.CubicTorus.normalComponentScalar_mean_zero line 775
  51. theorem OAI.CubicTorus.normalComponentScalar_energy_sum line 804