OAI/Analysis/AllenCahn/LogGradient.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DeGiorgi.bounded_log_gradient line 10
  2. lemma OAI.DeGiorgi.coordDeriv_div line 89
  3. lemma OAI.DeGiorgi.coordDeriv_log line 101
  4. lemma OAI.DeGiorgi.gradient_log line 107
  5. lemma OAI.DeGiorgi.laplacian_log line 112
  6. lemma OAI.DeGiorgi.drift_log line 126
  7. lemma OAI.DeGiorgi.gradient_add_const line 137
  8. lemma OAI.DeGiorgi.coordDeriv_add_const line 141
  9. lemma OAI.DeGiorgi.regularized_defect_log_bounds line 146
  10. def OAI.DeGiorgi.relativeDefectConstant line 215
  11. lemma OAI.DeGiorgi.relativeDefectConstant_pos line 220
  12. lemma OAI.DeGiorgi.regularized_defect_gradient_bound line 225
  13. theorem OAI.DeGiorgi.diffuseDefect_relative_gradient_bound line 270
  14. lemma OAI.DeGiorgi.diffuseDefect_log_lipschitz line 286
  15. lemma OAI.DeGiorgi.diffuseDefect_exp_comparison_crude line 310
  16. lemma OAI.DeGiorgi.coordDeriv_comp_scalar line 319
  17. lemma OAI.DeGiorgi.laplacian_comp_scalar line 327