OAI/Analysis/AllenCahn/DriftMaximum.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DriftSupport.DeGiorgi.Space line 16
  2. def OAI.DriftSupport.DeGiorgi.potential line 18
  3. def OAI.DriftSupport.DeGiorgi.profile line 20
  4. def OAI.DriftSupport.DeGiorgi.surfaceTension line 22
  5. def OAI.DriftSupport.DeGiorgi.AllenCahn line 24
  6. def OAI.DriftSupport.DeGiorgi.SecondVariation line 27
  7. def OAI.DriftSupport.DeGiorgi.Stable line 30
  8. def OAI.DriftSupport.DeGiorgi.Energy line 34
  9. def OAI.DriftSupport.DeGiorgi.unitBallVolume line 37
  10. def OAI.DriftSupport.DeGiorgi.density line 40
  11. def OAI.DriftSupport.DeGiorgi.densityAtInfinity line 43
  12. def OAI.DriftSupport.DeGiorgi.Classified line 46
  13. def OAI.DriftSupport.DeGiorgi.StableRigiditySeven line 50
  14. def OAI.DriftSupport.DeGiorgi.MonotoneRigidityEight line 54
  15. def OAI.DriftSupport.DeGiorgi.FiniteDensityRigidity line 61
  16. lemma OAI.DriftSupport.DeGiorgi.second_deriv_nonneg_of_local_min line 81
  17. def OAI.DriftSupport.DeGiorgi.basis line 94
  18. def OAI.DriftSupport.DeGiorgi.coordDeriv line 96
  19. lemma OAI.DriftSupport.DeGiorgi.coordDeriv_contDiff line 99
  20. lemma OAI.DriftSupport.DeGiorgi.laplacian_eq_sum_coordDeriv line 103
  21. lemma OAI.DriftSupport.DeGiorgi.deriv_line line 115
  22. lemma OAI.DriftSupport.DeGiorgi.laplacian_nonneg_of_local_min line 122
  23. lemma OAI.DriftSupport.DeGiorgi.compact_minimum_principle_drift line 145
  24. def OAI.DriftSupport.DeGiorgi.gaussian line 167
  25. lemma OAI.DriftSupport.DeGiorgi.gaussian_contDiff line 170
  26. lemma OAI.DriftSupport.DeGiorgi.fderiv_gaussian line 175
  27. lemma OAI.DriftSupport.DeGiorgi.second_coord_gaussian line 183
  28. lemma OAI.DriftSupport.DeGiorgi.laplacian_gaussian line 209
  29. def OAI.DriftSupport.DeGiorgi.barrier line 219
  30. lemma OAI.DriftSupport.DeGiorgi.barrier_contDiff line 222
  31. lemma OAI.DriftSupport.DeGiorgi.laplacian_barrier line 225
  32. lemma OAI.DriftSupport.DeGiorgi.barrier_le_one line 233
  33. lemma OAI.DriftSupport.DeGiorgi.fderiv_barrier line 242
  34. lemma OAI.DriftSupport.DeGiorgi.barrier_subsolution_drift line 250
  35. lemma OAI.DriftSupport.DeGiorgi.laplacian_sub_const_mul line 277
  36. lemma OAI.DriftSupport.DeGiorgi.annulus_comparison_drift line 287
  37. lemma OAI.DriftSupport.DeGiorgi.nonneg_right_derivative line 340