OAI/Geometry/CubicTorus/Profiles/NodalTorusScalar.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.positiveNodalPiece_continuousOn line 13
  2. lemma OAI.CubicTorus.CenteredJacobiChart.scalar_representative_ae line 48
  3. theorem OAI.CubicTorus.CenteredJacobiChart.boundary_continuous_C1 line 70
  4. def OAI.CubicTorus.nodalTorusScalar line 91
  5. lemma OAI.CubicTorus.nodalTorusScalar_measurable line 94
  6. lemma OAI.CubicTorus.nodalSurfaceJet_scalar_ae line 98
  7. lemma OAI.CubicTorus.surfaceNodalBalance_scalar_ae line 112
  8. lemma OAI.CubicTorus.localMin_second_derivative_nonneg line 144
  9. lemma OAI.CubicTorus.plane_localMin_hessian_nonneg line 158
  10. lemma OAI.CubicTorus.planeTrace_smul line 194
  11. lemma OAI.CubicTorus.planeTrace_cmc_nonneg line 198
  12. lemma OAI.CubicTorus.plane_gradient_eq_zero_of_localMin line 221
  13. lemma OAI.CubicTorus.cmc_divergence_nonneg_at_localMin line 225
  14. lemma OAI.CubicTorus.cmc_strict_minimum_principle line 236
  15. def OAI.CubicTorus.planeRadialExp line 265
  16. lemma OAI.CubicTorus.planeRadialExp_contDiff line 268
  17. lemma OAI.CubicTorus.planeRadialExp_pos line 273
  18. lemma OAI.CubicTorus.planeRadialExp_gradient line 276
  19. lemma OAI.CubicTorus.planeDivergence_const_smul line 288
  20. lemma OAI.CubicTorus.sibling_planeDivergence_contDiff line 293
  21. lemma OAI.CubicTorus.planeRadialExp_cmc_divergence line 301
  22. lemma OAI.CubicTorus.planeRadialExp_cmc_positive line 323
  23. lemma OAI.CubicTorus.plane_gradient_linear line 351
  24. lemma OAI.CubicTorus.cmc_divergence_linear line 360
  25. theorem OAI.CubicTorus.cmc_annulus_barrier line 380
  26. lemma OAI.CubicTorus.plane_annulus_radial_tangent line 472
  27. lemma OAI.CubicTorus.radial_barrier_inward_derivative line 487
  28. theorem OAI.CubicTorus.cmc_hopf_inward_derivative line 523
  29. lemma OAI.CubicTorus.CenteredJacobiChart.smooth_scalar_ae line 546
  30. theorem OAI.CubicTorus.CenteredJacobiChart.classical_ground_state line 564
  31. lemma OAI.CubicTorus.positiveNodalPiece_subset line 620
  32. lemma OAI.CubicTorus.positiveNodalPiece_boundary_zero line 626
  33. lemma OAI.CubicTorus.positiveNodalPiece_boundary_nonempty line 645
  34. lemma OAI.CubicTorus.CenteredJacobiChart.parameter_zero line 665
  35. lemma OAI.CubicTorus.CenteredJacobiChart.closure_pullback line 672
  36. lemma OAI.CubicTorus.CenteredJacobiChart.positive_piece_pullback_open line 706
  37. def OAI.CubicTorus.sibling_planeElliptic line 738
  38. lemma OAI.CubicTorus.sibling_planeElliptic_contDiff line 741
  39. lemma OAI.CubicTorus.compact_inner_left line 746
  40. lemma OAI.CubicTorus.compact_inner_right line 754
  41. lemma OAI.CubicTorus.compact_clm_apply line 758
  42. lemma OAI.CubicTorus.sibling_planeDivergence_compact line 766
  43. lemma OAI.CubicTorus.sibling_planeElliptic_compact line 774
  44. lemma OAI.CubicTorus.planeElliptic_ibp line 778
  45. lemma OAI.CubicTorus.plane_inner_fderiv line 787
  46. lemma OAI.CubicTorus.plane_clm_fderiv line 795
  47. lemma OAI.CubicTorus.plane_energy_fderiv line 802
  48. lemma OAI.CubicTorus.plane_transport_gradient line 815
  49. def OAI.CubicTorus.planeTransport line 837
  50. lemma OAI.CubicTorus.planeTransport_contDiff line 840
  51. lemma OAI.CubicTorus.planeTransport_compact line 846