OAI/Analysis/AllenCahn/PoissonMaximum.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PoissonSupport.DeGiorgi.Space line 10
  2. def OAI.PoissonSupport.DeGiorgi.potential line 12
  3. def OAI.PoissonSupport.DeGiorgi.profile line 14
  4. def OAI.PoissonSupport.DeGiorgi.surfaceTension line 16
  5. def OAI.PoissonSupport.DeGiorgi.AllenCahn line 18
  6. def OAI.PoissonSupport.DeGiorgi.SecondVariation line 21
  7. def OAI.PoissonSupport.DeGiorgi.Stable line 24
  8. def OAI.PoissonSupport.DeGiorgi.Energy line 28
  9. def OAI.PoissonSupport.DeGiorgi.unitBallVolume line 31
  10. def OAI.PoissonSupport.DeGiorgi.density line 34
  11. def OAI.PoissonSupport.DeGiorgi.densityAtInfinity line 37
  12. def OAI.PoissonSupport.DeGiorgi.Classified line 40
  13. def OAI.PoissonSupport.DeGiorgi.StableRigiditySeven line 44
  14. def OAI.PoissonSupport.DeGiorgi.MonotoneRigidityEight line 48
  15. def OAI.PoissonSupport.DeGiorgi.FiniteDensityRigidity line 55
  16. lemma OAI.PoissonSupport.DeGiorgi.second_deriv_nonneg_of_local_min line 70
  17. def OAI.PoissonSupport.DeGiorgi.basis line 83
  18. def OAI.PoissonSupport.DeGiorgi.coordDeriv line 85
  19. lemma OAI.PoissonSupport.DeGiorgi.coordDeriv_contDiff line 88
  20. lemma OAI.PoissonSupport.DeGiorgi.laplacian_eq_sum_coordDeriv line 92
  21. lemma OAI.PoissonSupport.DeGiorgi.deriv_line line 104
  22. lemma OAI.PoissonSupport.DeGiorgi.laplacian_nonneg_of_local_min line 111
  23. lemma OAI.PoissonSupport.DeGiorgi.laplacian_nonpos_of_local_max line 134
  24. lemma OAI.PoissonSupport.DeGiorgi.coordDeriv_translate line 142
  25. lemma OAI.PoissonSupport.DeGiorgi.laplacian_translate line 151
  26. lemma OAI.PoissonSupport.DeGiorgi.laplacian_norm_sq line 164
  27. lemma OAI.PoissonSupport.DeGiorgi.hasFDerivAt_norm_nonzero line 184
  28. lemma OAI.PoissonSupport.DeGiorgi.laplacian_fun_sub line 193
  29. lemma OAI.PoissonSupport.DeGiorgi.laplacian_fun_add line 200
  30. lemma OAI.PoissonSupport.DeGiorgi.laplacian_fun_const_mul line 207
  31. lemma OAI.PoissonSupport.DeGiorgi.laplacian_comp_isometry line 213
  32. def OAI.PoissonSupport.DeGiorgi.reflect line 228
  33. lemma OAI.PoissonSupport.DeGiorgi.reflect_apply line 231
  34. def OAI.PoissonSupport.DeGiorgi.poissonPenalty line 239
  35. lemma OAI.PoissonSupport.DeGiorgi.poissonPenalty_of_le line 241
  36. lemma OAI.PoissonSupport.DeGiorgi.poissonPenalty_of_ge line 246
  37. lemma OAI.PoissonSupport.DeGiorgi.poissonPenalty_nonneg line 250
  38. lemma OAI.PoissonSupport.DeGiorgi.poissonPenalty_le_linear line 259
  39. lemma OAI.PoissonSupport.DeGiorgi.poisson_maximum line 267
  40. lemma OAI.PoissonSupport.DeGiorgi.coordDeriv_affine line 303
  41. lemma OAI.PoissonSupport.DeGiorgi.laplacian_affine line 309
  42. lemma OAI.PoissonSupport.DeGiorgi.laplacian_affine_sq line 318