OAI/Analysis/AllenCahn/Cutoffs.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DeGiorgi.coordinate_polynomial_profile line 15
  2. lemma OAI.DeGiorgi.weight_polynomial_jets line 32
  3. lemma OAI.DeGiorgi.profileWeight_relative_jets line 54
  4. lemma OAI.DeGiorgi.relative_jets_carrier line 65
  5. def OAI.DeGiorgi.normalReflection line 94
  6. lemma OAI.DeGiorgi.normalReflection_apply line 97
  7. lemma OAI.DeGiorgi.normalReflection_inner line 103
  8. lemma OAI.DeGiorgi.profileWeight_neg line 108
  9. lemma OAI.DeGiorgi.SmallDefectConverges.tensor_normal_translate line 111
  10. lemma OAI.DeGiorgi.limit_source_relative_jets line 134
  11. theorem OAI.DeGiorgi.SmallDefectConverges.even_source_removed line 190
  12. def OAI.DeGiorgi.unitCutoff line 231
  13. lemma OAI.DeGiorgi.unitCutoff_smooth line 233
  14. lemma OAI.DeGiorgi.fderiv_unitCutoff line 236
  15. lemma OAI.DeGiorgi.gradient_unitCutoff line 248
  16. lemma OAI.DeGiorgi.laplacian_unitCutoff line 254
  17. lemma OAI.DeGiorgi.gradient_fun_square line 268
  18. lemma OAI.DeGiorgi.cutoff_max_calculus line 274
  19. lemma OAI.DeGiorgi.quartic_cubic_bound line 299
  20. lemma OAI.DeGiorgi.cutoff_bernstein_algebra line 311