OAI/Analysis/AllenCahn/Bernstein.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DeGiorgi.diffuse_drift_commute line 10
  2. lemma OAI.DeGiorgi.inverseHessian_deriv_drift_bound line 39
  3. lemma OAI.DeGiorgi.drift_sum_identity line 70
  4. lemma OAI.DeGiorgi.tensorDerivativeSquare_eq_sum line 79
  5. lemma OAI.DeGiorgi.tensorDerivativeSquare_uniform line 84
  6. lemma OAI.DeGiorgi.tensorDerivativeSquare_drift_identity line 97
  7. def OAI.DeGiorgi.tensorSecondBernsteinConstant line 118
  8. lemma OAI.DeGiorgi.tensorSecondBernsteinConstant_pos line 121
  9. lemma OAI.DeGiorgi.tensorDerivativeSquare_drift_lower line 124
  10. lemma OAI.DeGiorgi.hessianSquare_drift_lower_refined line 182
  11. def OAI.DeGiorgi.carrierScale line 225
  12. def OAI.DeGiorgi.defectCarrier line 227
  13. lemma OAI.DeGiorgi.carrierScale_pos line 230
  14. lemma OAI.DeGiorgi.defectCarrier_smooth line 233
  15. lemma OAI.DeGiorgi.defectCarrier_bounds line 238
  16. lemma OAI.DeGiorgi.drift_const_mul line 252
  17. lemma OAI.DeGiorgi.drift_sub line 260
  18. lemma OAI.DeGiorgi.defectCarrier_drift_upper line 269
  19. lemma OAI.DeGiorgi.C1Bound.sub line 300
  20. lemma OAI.DeGiorgi.C1Bound.sum line 310
  21. lemma OAI.DeGiorgi.C1Bound.gradient_bound line 319
  22. lemma OAI.DeGiorgi.hessianSquare_C1Bound line 324
  23. lemma OAI.DeGiorgi.defectCarrier_gradient_bound line 340