OAI/Analysis/AllenCahn/TensorBounds.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DeGiorgi.hessianSquare_drift_identity line 10
  2. def OAI.DeGiorgi.tensorSystemConstant line 36
  3. def OAI.DeGiorgi.tensorBernsteinConstant line 39
  4. lemma OAI.DeGiorgi.hessianSquare_drift_lower line 41
  5. lemma OAI.DeGiorgi.diffuseDefect_drift_upper line 82
  6. theorem OAI.DeGiorgi.hessianSquare_le_defect line 100
  7. lemma OAI.DeGiorgi.quotient_bernstein_linear line 118
  8. def OAI.DeGiorgi.C1Bound line 193
  9. lemma OAI.DeGiorgi.C1Bound.mono line 196
  10. lemma OAI.DeGiorgi.C1Bound.const line 200
  11. lemma OAI.DeGiorgi.C1Bound.neg line 205
  12. lemma OAI.DeGiorgi.C1Bound.mul line 214
  13. lemma OAI.DeGiorgi.C1Bound.const_mul line 233
  14. lemma OAI.DeGiorgi.inverseHessian_gradient_uniform_bound line 245
  15. def OAI.DeGiorgi.inverseJetConstant line 271
  16. lemma OAI.DeGiorgi.inverseJetConstant_one_le line 278