OAI/Analysis/AllenCahn/Eikonal.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.EikonalSupport.DeGiorgi.Space line 16
  2. def OAI.EikonalSupport.DeGiorgi.potential line 18
  3. def OAI.EikonalSupport.DeGiorgi.profile line 20
  4. def OAI.EikonalSupport.DeGiorgi.surfaceTension line 22
  5. def OAI.EikonalSupport.DeGiorgi.AllenCahn line 24
  6. def OAI.EikonalSupport.DeGiorgi.SecondVariation line 27
  7. def OAI.EikonalSupport.DeGiorgi.Stable line 30
  8. def OAI.EikonalSupport.DeGiorgi.Energy line 34
  9. def OAI.EikonalSupport.DeGiorgi.unitBallVolume line 37
  10. def OAI.EikonalSupport.DeGiorgi.density line 40
  11. def OAI.EikonalSupport.DeGiorgi.densityAtInfinity line 43
  12. def OAI.EikonalSupport.DeGiorgi.Classified line 46
  13. def OAI.EikonalSupport.DeGiorgi.StableRigiditySeven line 50
  14. def OAI.EikonalSupport.DeGiorgi.MonotoneRigidityEight line 54
  15. def OAI.EikonalSupport.DeGiorgi.FiniteDensityRigidity line 61
  16. lemma OAI.EikonalSupport.DeGiorgi.gradient_contDiff line 82
  17. lemma OAI.EikonalSupport.DeGiorgi.inner_fderiv_gradient line 86
  18. lemma OAI.EikonalSupport.DeGiorgi.fderiv_gradient_symmetric line 96
  19. lemma OAI.EikonalSupport.DeGiorgi.eikonal_acceleration_zero line 102
  20. lemma OAI.EikonalSupport.DeGiorgi.eikonal_gradient_on_line line 119
  21. lemma OAI.EikonalSupport.DeGiorgi.eikonal_value_on_line line 152
  22. lemma OAI.EikonalSupport.DeGiorgi.eikonal_lipschitz line 170
  23. lemma OAI.EikonalSupport.DeGiorgi.eikonal_gradient_constant line 179
  24. lemma OAI.EikonalSupport.DeGiorgi.eikonal_affine line 216
  25. def OAI.EikonalSupport.DeGiorgi.inverseProfile line 252
  26. def OAI.EikonalSupport.DeGiorgi.diffuseDefect line 255
  27. lemma OAI.EikonalSupport.DeGiorgi.inverseProfile_contDiff line 258
  28. lemma OAI.EikonalSupport.DeGiorgi.profile_inverseProfile line 272
  29. theorem OAI.EikonalSupport.DeGiorgi.classified_of_zero_defect line 279