OAI/Analysis/AllenCahn/RegularityModel.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.RegularitySupport.DeGiorgi.Space line 16
  2. def OAI.RegularitySupport.DeGiorgi.potential line 18
  3. def OAI.RegularitySupport.DeGiorgi.profile line 20
  4. def OAI.RegularitySupport.DeGiorgi.surfaceTension line 22
  5. def OAI.RegularitySupport.DeGiorgi.AllenCahn line 24
  6. def OAI.RegularitySupport.DeGiorgi.SecondVariation line 27
  7. def OAI.RegularitySupport.DeGiorgi.Stable line 30
  8. def OAI.RegularitySupport.DeGiorgi.Energy line 34
  9. def OAI.RegularitySupport.DeGiorgi.unitBallVolume line 37
  10. def OAI.RegularitySupport.DeGiorgi.density line 40
  11. def OAI.RegularitySupport.DeGiorgi.densityAtInfinity line 43
  12. def OAI.RegularitySupport.DeGiorgi.Classified line 46
  13. def OAI.RegularitySupport.DeGiorgi.StableRigiditySeven line 50
  14. def OAI.RegularitySupport.DeGiorgi.MonotoneRigidityEight line 54
  15. def OAI.RegularitySupport.DeGiorgi.FiniteDensityRigidity line 61
  16. lemma OAI.RegularitySupport.DeGiorgi.second_deriv_nonneg_of_local_min line 81
  17. def OAI.RegularitySupport.DeGiorgi.basis line 94
  18. def OAI.RegularitySupport.DeGiorgi.coordDeriv line 96
  19. lemma OAI.RegularitySupport.DeGiorgi.coordDeriv_contDiff line 99
  20. lemma OAI.RegularitySupport.DeGiorgi.laplacian_eq_sum_coordDeriv line 103
  21. lemma OAI.RegularitySupport.DeGiorgi.deriv_line line 115
  22. lemma OAI.RegularitySupport.DeGiorgi.laplacian_nonneg_of_local_min line 122
  23. lemma OAI.RegularitySupport.DeGiorgi.laplacian_nonpos_of_local_max line 145
  24. lemma OAI.RegularitySupport.DeGiorgi.coordDeriv_translate line 153
  25. lemma OAI.RegularitySupport.DeGiorgi.laplacian_translate line 162
  26. lemma OAI.RegularitySupport.DeGiorgi.laplacian_norm_sq line 175
  27. lemma OAI.RegularitySupport.DeGiorgi.hasFDerivAt_norm_nonzero line 195
  28. lemma OAI.RegularitySupport.DeGiorgi.laplacian_fun_sub line 204
  29. lemma OAI.RegularitySupport.DeGiorgi.laplacian_fun_add line 211
  30. lemma OAI.RegularitySupport.DeGiorgi.laplacian_fun_const_mul line 218
  31. lemma OAI.RegularitySupport.DeGiorgi.laplacian_comp_isometry line 224
  32. def OAI.RegularitySupport.DeGiorgi.reflect line 239
  33. lemma OAI.RegularitySupport.DeGiorgi.reflect_apply line 242
  34. def OAI.RegularitySupport.DeGiorgi.poissonPenalty line 250
  35. lemma OAI.RegularitySupport.DeGiorgi.poissonPenalty_of_le line 252
  36. lemma OAI.RegularitySupport.DeGiorgi.poissonPenalty_of_ge line 257
  37. lemma OAI.RegularitySupport.DeGiorgi.poissonPenalty_nonneg line 261
  38. lemma OAI.RegularitySupport.DeGiorgi.poissonPenalty_le_linear line 270
  39. lemma OAI.RegularitySupport.DeGiorgi.poisson_maximum line 278
  40. lemma OAI.RegularitySupport.DeGiorgi.coordDeriv_affine line 314
  41. lemma OAI.RegularitySupport.DeGiorgi.laplacian_affine line 320
  42. lemma OAI.RegularitySupport.DeGiorgi.laplacian_affine_sq line 329