OAI/Analysis/AllenCahn/DefectCalculus.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DeGiorgi.regularized_inverse_lipschitz_gt_one line 11
  2. lemma OAI.DeGiorgi.regularized_inverse_lipschitz line 58
  3. lemma OAI.DeGiorgi.regularized_inverse_gradient_bound line 80
  4. theorem OAI.DeGiorgi.modica_linear line 90
  5. theorem OAI.DeGiorgi.modica line 124
  6. theorem OAI.DeGiorgi.diffuseDefect_nonneg line 134
  7. lemma OAI.DeGiorgi.smooth_C2 line 157
  8. lemma OAI.DeGiorgi.coordDeriv_smooth line 160
  9. lemma OAI.DeGiorgi.coordDeriv_sum line 164
  10. lemma OAI.DeGiorgi.coordDeriv_comm line 169
  11. lemma OAI.DeGiorgi.laplacian_coordDeriv line 179
  12. lemma OAI.DeGiorgi.laplacian_sum line 192
  13. lemma OAI.DeGiorgi.laplacian_sq line 206
  14. lemma OAI.DeGiorgi.laplacian_gradient_norm_sq line 224
  15. lemma OAI.DeGiorgi.inverseProfile_smooth line 240
  16. lemma OAI.DeGiorgi.gradient_norm_sq_smooth line 254
  17. lemma OAI.DeGiorgi.diffuseDefect_smooth line 261
  18. lemma OAI.DeGiorgi.coordDeriv_profile line 265
  19. lemma OAI.DeGiorgi.inverseProfile_laplacian_eq line 275
  20. lemma OAI.DeGiorgi.inner_gradient_eq_sum line 290
  21. lemma OAI.DeGiorgi.diffuseDefect_laplacian line 296
  22. lemma OAI.DeGiorgi.inverseProfile_gradient_bound line 343
  23. lemma OAI.DeGiorgi.diffuseDrift_bound line 350