OAI/Analysis/AllenCahn/Modica.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DeGiorgi.two_point_gradient_bounds line 11
  2. lemma OAI.DeGiorgi.lipschitz_of_laplacian_monotonicity line 76
  3. def OAI.DeGiorgi.defectWeight line 134
  4. lemma OAI.DeGiorgi.hasDerivAt_artanh line 136
  5. def OAI.DeGiorgi.inverseProfile line 155
  6. def OAI.DeGiorgi.diffuseDefect line 158
  7. lemma OAI.DeGiorgi.profile_inverseProfile line 161
  8. lemma OAI.DeGiorgi.fderiv_inverseProfile line 168
  9. lemma OAI.DeGiorgi.gradient_inverseProfile line 177
  10. lemma OAI.DeGiorgi.inverseProfile_contDiff line 182
  11. lemma OAI.DeGiorgi.gradient_norm_sq line 196
  12. lemma OAI.DeGiorgi.coordDeriv_mul line 202
  13. lemma OAI.DeGiorgi.weight_pos line 208
  14. lemma OAI.DeGiorgi.coordDeriv_inverseProfile_coefficient line 211
  15. lemma OAI.DeGiorgi.laplacian_inverseProfile line 226
  16. lemma OAI.DeGiorgi.laplacian_regularized_inverse line 252
  17. lemma OAI.DeGiorgi.cube_div_weight_monotone line 278
  18. lemma OAI.DeGiorgi.inverseProfile_scalar_quantitative line 295
  19. lemma OAI.DeGiorgi.inverseProfile_scalar_bound line 321