OAI/Analysis/AllenCahn/DefectLimits.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DeGiorgi.SmallDefectConverges.D_over_root_vanishes line 12
  2. lemma OAI.DeGiorgi.profile_contDiff line 27
  3. lemma OAI.DeGiorgi.SmallDefectConverges.v_limit line 33
  4. theorem OAI.DeGiorgi.SmallDefectConverges.tensor_tangential line 46
  5. lemma OAI.DeGiorgi.inverseHessian_transport line 66
  6. theorem OAI.DeGiorgi.SmallDefectConverges.tensor_transport line 94
  7. lemma OAI.DeGiorgi.SmallDefectConverges.D_vanishes line 119
  8. lemma OAI.DeGiorgi.SmallDefectConverges.positive line 131
  9. lemma OAI.DeGiorgi.SmallDefectConverges.tensor_trace line 138
  10. lemma OAI.DeGiorgi.SmallDefectConverges.controlled_over_root_vanishes line 156
  11. theorem OAI.DeGiorgi.SmallDefectConverges.tensor_harmonic line 173
  12. lemma OAI.DeGiorgi.normalized_defect_equation line 208
  13. theorem OAI.DeGiorgi.SmallDefectConverges.defect_equation line 237
  14. def OAI.DeGiorgi.profileWeight line 271
  15. lemma OAI.DeGiorgi.profile_hasDerivAt line 273
  16. lemma OAI.DeGiorgi.profileWeight_contDiff line 288
  17. lemma OAI.DeGiorgi.profileWeight_pos line 291
  18. lemma OAI.DeGiorgi.profileWeight_hasDerivAt line 295
  19. lemma OAI.DeGiorgi.profileWeight_hasDerivAt_twice line 309
  20. lemma OAI.DeGiorgi.gradient_comp_inner line 328
  21. lemma OAI.DeGiorgi.gradient_inner line 338
  22. lemma OAI.DeGiorgi.laplacian_inner line 342