OAI/Analysis/AllenCahn/EndpointMaximum.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.EndpointSupport.DeGiorgi.Space line 16
  2. def OAI.EndpointSupport.DeGiorgi.potential line 18
  3. def OAI.EndpointSupport.DeGiorgi.profile line 20
  4. def OAI.EndpointSupport.DeGiorgi.surfaceTension line 22
  5. def OAI.EndpointSupport.DeGiorgi.AllenCahn line 24
  6. def OAI.EndpointSupport.DeGiorgi.SecondVariation line 27
  7. def OAI.EndpointSupport.DeGiorgi.Stable line 30
  8. def OAI.EndpointSupport.DeGiorgi.Energy line 34
  9. def OAI.EndpointSupport.DeGiorgi.unitBallVolume line 37
  10. def OAI.EndpointSupport.DeGiorgi.density line 40
  11. def OAI.EndpointSupport.DeGiorgi.densityAtInfinity line 43
  12. def OAI.EndpointSupport.DeGiorgi.Classified line 46
  13. def OAI.EndpointSupport.DeGiorgi.StableRigiditySeven line 50
  14. def OAI.EndpointSupport.DeGiorgi.MonotoneRigidityEight line 54
  15. def OAI.EndpointSupport.DeGiorgi.FiniteDensityRigidity line 61
  16. lemma OAI.EndpointSupport.DeGiorgi.second_deriv_nonneg_of_local_min line 81
  17. def OAI.EndpointSupport.DeGiorgi.basis line 94
  18. def OAI.EndpointSupport.DeGiorgi.coordDeriv line 96
  19. lemma OAI.EndpointSupport.DeGiorgi.coordDeriv_contDiff line 99
  20. lemma OAI.EndpointSupport.DeGiorgi.laplacian_eq_sum_coordDeriv line 103
  21. lemma OAI.EndpointSupport.DeGiorgi.deriv_line line 115
  22. lemma OAI.EndpointSupport.DeGiorgi.laplacian_nonneg_of_local_min line 122
  23. lemma OAI.EndpointSupport.DeGiorgi.compact_minimum_principle line 145
  24. def OAI.EndpointSupport.DeGiorgi.gaussian line 163
  25. lemma OAI.EndpointSupport.DeGiorgi.gaussian_contDiff line 166
  26. lemma OAI.EndpointSupport.DeGiorgi.fderiv_gaussian line 171
  27. lemma OAI.EndpointSupport.DeGiorgi.second_coord_gaussian line 179
  28. lemma OAI.EndpointSupport.DeGiorgi.laplacian_gaussian line 205
  29. def OAI.EndpointSupport.DeGiorgi.barrier line 215
  30. lemma OAI.EndpointSupport.DeGiorgi.barrier_contDiff line 218
  31. lemma OAI.EndpointSupport.DeGiorgi.laplacian_barrier line 221
  32. lemma OAI.EndpointSupport.DeGiorgi.barrier_le_one line 229
  33. lemma OAI.EndpointSupport.DeGiorgi.barrier_subsolution line 238
  34. lemma OAI.EndpointSupport.DeGiorgi.laplacian_sub_const_mul line 255
  35. lemma OAI.EndpointSupport.DeGiorgi.annulus_comparison line 265
  36. lemma OAI.EndpointSupport.DeGiorgi.fderiv_barrier line 312
  37. lemma OAI.EndpointSupport.DeGiorgi.nonneg_right_derivative line 320