OAI/Analysis/AllenCahn/Barriers.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DeGiorgi.laplacian_exp line 10
  2. def OAI.DeGiorgi.smoothRadius line 18
  3. lemma OAI.DeGiorgi.smoothRadius_pos line 20
  4. lemma OAI.DeGiorgi.smoothRadius_sq line 23
  5. lemma OAI.DeGiorgi.norm_le_smoothRadius line 26
  6. lemma OAI.DeGiorgi.smoothRadius_le_norm_add_one line 29
  7. lemma OAI.DeGiorgi.smoothRadius_smooth line 32
  8. lemma OAI.DeGiorgi.fderiv_smoothRadius line 35
  9. lemma OAI.DeGiorgi.gradient_smoothRadius line 50
  10. lemma OAI.DeGiorgi.laplacian_smoothRadius line 56
  11. lemma OAI.DeGiorgi.exterior_comparison line 102
  12. def OAI.DeGiorgi.radialBarrier line 142
  13. lemma OAI.DeGiorgi.radialBarrier_pos line 145
  14. lemma OAI.DeGiorgi.radialBarrier_smooth line 147
  15. lemma OAI.DeGiorgi.radialBarrier_decay line 150
  16. lemma OAI.DeGiorgi.fderiv_radialBarrier line 158
  17. lemma OAI.DeGiorgi.laplacian_radialBarrier line 169
  18. lemma OAI.DeGiorgi.defectPotential_nonneg line 188
  19. lemma OAI.DeGiorgi.defectPotential_le line 195
  20. lemma OAI.DeGiorgi.diffuseDrift_bound_refined line 204
  21. lemma OAI.DeGiorgi.sharp_potential_drift_bound line 212
  22. lemma OAI.DeGiorgi.radialBarrier_fderiv_bound line 222
  23. def OAI.DeGiorgi.sharpDefectRadius line 232
  24. lemma OAI.DeGiorgi.sharpDefect_gap_pos line 235
  25. lemma OAI.DeGiorgi.sharpDefectRadius_pos line 240
  26. lemma OAI.DeGiorgi.radialBarrier_laplacian_strict line 247
  27. lemma OAI.DeGiorgi.radialBarrier_defect_subsolution line 284