OAI/Analysis/AllenCahn/RelativeDerivatives.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DeGiorgi.derivativeDefectConstant line 10
  2. lemma OAI.DeGiorgi.derivativeDefectConstant_pos line 14
  3. theorem OAI.DeGiorgi.tensorDerivativeSquare_le_defect line 20
  4. lemma OAI.DeGiorgi.coordDeriv_square line 73
  5. lemma OAI.DeGiorgi.coordDeriv_hessianSquare line 78
  6. lemma OAI.DeGiorgi.coordDeriv_hessianSquare_bound line 91
  7. def OAI.DeGiorgi.defectPotential line 114
  8. def OAI.DeGiorgi.defectSource line 117
  9. def OAI.DeGiorgi.defectPotentialConstant line 120
  10. def OAI.DeGiorgi.defectSourceConstant line 122
  11. lemma OAI.DeGiorgi.defectPotentialConstant_nonneg line 125
  12. lemma OAI.DeGiorgi.defectSourceConstant_pos line 129
  13. lemma OAI.DeGiorgi.defectPotential_smooth line 135
  14. lemma OAI.DeGiorgi.defectSource_smooth line 140
  15. lemma OAI.DeGiorgi.defectPotential_C1Bound line 146
  16. lemma OAI.DeGiorgi.diffuseDefect_drift_eq_source line 162
  17. lemma OAI.DeGiorgi.defectSource_bounds line 171
  18. lemma OAI.DeGiorgi.drift_log_bochner line 217
  19. lemma OAI.DeGiorgi.laplacian_sq_le_hessian line 252
  20. lemma OAI.DeGiorgi.log_bochner_lower line 266
  21. lemma OAI.DeGiorgi.bounded_drift_logistic_scaled line 302