OAI/Analysis/AllenCahn/TensorSources.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DeGiorgi.inverseJet_C1Bound line 10
  2. def OAI.DeGiorgi.tensorCoeffZero line 79
  3. def OAI.DeGiorgi.tensorCoeffSource line 82
  4. def OAI.DeGiorgi.tensorCoeffFirst line 86
  5. def OAI.DeGiorgi.tensorCoeffSecond line 89
  6. def OAI.DeGiorgi.driftCoeff line 92
  7. def OAI.DeGiorgi.tensorCoeffConstant line 95
  8. lemma OAI.DeGiorgi.tensorCoeffConstant_pos line 100
  9. lemma OAI.DeGiorgi.tensorCoeff_C1Bound line 104
  10. lemma OAI.DeGiorgi.tensorCoeff_smooth line 171
  11. def OAI.DeGiorgi.tensorSource line 187
  12. lemma OAI.DeGiorgi.inverseHessian_drift_factored line 193
  13. lemma OAI.DeGiorgi.tensorSource_smooth line 216
  14. def OAI.DeGiorgi.tensorDerivativeSquare line 226
  15. lemma OAI.DeGiorgi.tensorDerivativeSquare_nonneg line 229
  16. lemma OAI.DeGiorgi.tensorDerivativeSquare_smooth line 233
  17. lemma OAI.DeGiorgi.inverseHessian_deriv_abs_le_sqrt line 239
  18. lemma OAI.DeGiorgi.coordDeriv_mul_estimate line 250
  19. lemma OAI.DeGiorgi.coordDeriv_add line 263
  20. lemma OAI.DeGiorgi.tensorSource_coord_bound line 268
  21. lemma OAI.DeGiorgi.fderiv_diffuseDrift_sum line 329