OAI/Analysis/AllenCahn/Basic.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DeGiorgi.Space line 10
  2. def OAI.DeGiorgi.potential line 12
  3. def OAI.DeGiorgi.profile line 14
  4. def OAI.DeGiorgi.surfaceTension line 16
  5. def OAI.DeGiorgi.AllenCahn line 18
  6. def OAI.DeGiorgi.SecondVariation line 21
  7. def OAI.DeGiorgi.Stable line 24
  8. def OAI.DeGiorgi.Energy line 28
  9. def OAI.DeGiorgi.unitBallVolume line 31
  10. def OAI.DeGiorgi.density line 34
  11. def OAI.DeGiorgi.densityAtInfinity line 37
  12. def OAI.DeGiorgi.Classified line 40
  13. def OAI.DeGiorgi.StableRigiditySeven line 44
  14. def OAI.DeGiorgi.MonotoneRigidityEight line 48
  15. def OAI.DeGiorgi.FiniteDensityRigidity line 55
  16. lemma OAI.DeGiorgi.second_deriv_nonneg_of_local_min line 70
  17. def OAI.DeGiorgi.basis line 83
  18. def OAI.DeGiorgi.coordDeriv line 85
  19. lemma OAI.DeGiorgi.coordDeriv_contDiff line 88
  20. lemma OAI.DeGiorgi.laplacian_eq_sum_coordDeriv line 92
  21. lemma OAI.DeGiorgi.deriv_line line 104
  22. lemma OAI.DeGiorgi.laplacian_nonneg_of_local_min line 111
  23. lemma OAI.DeGiorgi.laplacian_nonpos_of_local_max line 134
  24. lemma OAI.DeGiorgi.coordDeriv_translate line 142
  25. lemma OAI.DeGiorgi.laplacian_translate line 151
  26. lemma OAI.DeGiorgi.laplacian_norm_sq line 164
  27. lemma OAI.DeGiorgi.hasFDerivAt_norm_nonzero line 184
  28. lemma OAI.DeGiorgi.two_point_maximum line 193
  29. lemma OAI.DeGiorgi.gradient_at_two_point_max_y line 227
  30. lemma OAI.DeGiorgi.laplacian_fun_sub line 259
  31. lemma OAI.DeGiorgi.laplacian_fun_add line 266
  32. lemma OAI.DeGiorgi.laplacian_fun_const_mul line 273
  33. lemma OAI.DeGiorgi.laplacian_at_two_point_max line 279
  34. lemma OAI.DeGiorgi.sq_norm_error line 323