OAI/Geometry/CubicTorus/Estimates/SmoothScalarSeparatedTrunc.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicTorus.smoothScalarSeparatedTrunc line 13
  2. lemma OAI.CubicTorus.gradient_separatedPositiveTrunc line 17
  3. lemma OAI.CubicTorus.smoothScalarGradient_separatedPositiveTrunc line 29
  4. def OAI.CubicTorus.nodalSurfaceValue line 51
  5. def OAI.CubicTorus.nodalSurfaceGradient line 53
  6. lemma OAI.CubicTorus.nodalSurfaceValue_memLp line 56
  7. lemma OAI.CubicTorus.nodalSurfaceGradient_memLp line 60
  8. def OAI.CubicTorus.nodalSurfaceJet line 65
  9. lemma OAI.CubicTorus.smoothScalarGradient_of_constant_germ line 70
  10. theorem OAI.CubicTorus.nodal_restriction_smooth_approximants line 78
  11. lemma OAI.CubicTorus.surfaceL2_continuous_bounded_convergence_ae line 137
  12. theorem OAI.CubicTorus.nodalSurfaceJet_mem_surfaceH1 line 154
  13. def OAI.CubicTorus.IsPositiveNodalPiece line 246
  14. lemma OAI.CubicTorus.positiveNodalPiece_superlevels line 250
  15. theorem OAI.CubicTorus.isMinimizerAt_positive_nodal_piece_H1 line 297
  16. lemma OAI.CubicTorus.surfaceJacobiB_nodal_restriction line 320
  17. lemma OAI.CubicTorus.surfaceJacobiB_disjoint_nodal line 352
  18. lemma OAI.CubicTorus.nodalSurfaceJet_null line 388
  19. theorem OAI.CubicTorus.Periodic.isMinimizerAt_translation_selected_nodal line 398
  20. lemma OAI.CubicTorus.surfaceMean_nodal line 433
  21. theorem OAI.CubicTorus.isMinimizerAt_nodal_mean_pos line 447
  22. def OAI.CubicTorus.surfaceNodalBalance line 513
  23. lemma OAI.CubicTorus.surfaceNodalBalance_mean line 516
  24. lemma OAI.CubicTorus.surfaceNodalBalance_mem line 521
  25. lemma OAI.CubicTorus.surfaceNodalBalance_null line 525
  26. lemma OAI.CubicTorus.nodalSurfaceJet_value_orthogonal line 539
  27. lemma OAI.CubicTorus.surfaceNodalBalance_ne_zero line 556
  28. lemma OAI.CubicTorus.nodalSurfaceJet_zero_outside line 572
  29. lemma OAI.CubicTorus.surfaceNodalBalance_zero_patch line 585
  30. theorem OAI.CubicTorus.Periodic.isMinimizerAt_two_nodal_balance line 619
  31. def OAI.CubicTorus.positiveBoundaryLocus line 677
  32. def OAI.CubicTorus.positiveBoundaryDomain line 680
  33. lemma OAI.CubicTorus.isOpen_positiveBoundaryLocus line 684
  34. lemma OAI.CubicTorus.positiveBoundaryDomain_nonempty line 689
  35. lemma OAI.CubicTorus.positiveBoundaryDomain_isPositiveNodalPiece line 693
  36. theorem OAI.CubicTorus.isMinimizerAt_actual_nodal_piece line 717
  37. theorem OAI.CubicTorus.Periodic.isMinimizerAt_actual_translation_nodal_domains line 739
  38. lemma OAI.CubicTorus.positiveNodalPiece_open_patch line 778
  39. lemma OAI.CubicTorus.positiveNodalPiece_unused_patch line 793
  40. theorem OAI.CubicTorus.Periodic.isMinimizerAt_three_nodal_weak_obstruction line 821
  41. def OAI.CubicTorus.surfaceVectorMultiplier line 872
  42. def OAI.CubicTorus.surfaceGradientMultiplier line 881
  43. def OAI.CubicTorus.surfaceCutoffJet line 890
  44. lemma OAI.CubicTorus.surfaceCutoffJet_continuous line 896
  45. lemma OAI.CubicTorus.surfaceCutoffJet_smooth line 901
  46. lemma OAI.CubicTorus.surfaceCutoffJet_ae line 937
  47. theorem OAI.CubicTorus.surfaceCutoffJet_mem_surfaceH1 line 962