OAI/Analysis/AllenCahn/Hessian.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DeGiorgi.diffuseDrift line 10
  2. def OAI.DeGiorgi.inverseHessian line 13
  3. def OAI.DeGiorgi.hessianSquare line 16
  4. lemma OAI.DeGiorgi.coordDeriv_sub line 19
  5. lemma OAI.DeGiorgi.coordDeriv_abs_le_gradient line 24
  6. lemma OAI.DeGiorgi.coordDeriv_diffuseDefect line 31
  7. lemma OAI.DeGiorgi.inverseGradient_drift_equation line 57
  8. lemma OAI.DeGiorgi.inverseGradient_uniform_bound line 78
  9. lemma OAI.DeGiorgi.hessianSquare_uniform_bound line 106
  10. lemma OAI.DeGiorgi.inverseHessian_smooth line 119
  11. lemma OAI.DeGiorgi.inverseHessian_symm line 124
  12. lemma OAI.DeGiorgi.hessianSquare_nonneg line 129
  13. lemma OAI.DeGiorgi.hessianSquare_eq_sum line 132
  14. lemma OAI.DeGiorgi.hessianSquare_smooth line 136
  15. lemma OAI.DeGiorgi.inverseHessian_sq_le line 144
  16. lemma OAI.DeGiorgi.inverseHessian_abs_le line 151
  17. lemma OAI.DeGiorgi.fderiv_diffuseDrift line 157
  18. lemma OAI.DeGiorgi.coordDeriv_diffuseDefect_sum line 163
  19. lemma OAI.DeGiorgi.coordDeriv_defectWeight line 172
  20. lemma OAI.DeGiorgi.inverseHessian_drift_system line 189
  21. lemma OAI.DeGiorgi.diffuseDefect_le_one line 258
  22. lemma OAI.DeGiorgi.inverseHessian_abs_le_sqrt line 263
  23. lemma OAI.DeGiorgi.coordDeriv_diffuseDefect_bound line 269
  24. lemma OAI.DeGiorgi.coordDeriv_diffuseDefect_uniform_bound line 287
  25. lemma OAI.DeGiorgi.gradient_norm_le_sum_abs line 305
  26. lemma OAI.DeGiorgi.diffuseDefect_gradient_uniform_bound line 316