OAI/Analysis/AllenCahn/SmallDefect.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DeGiorgi.coherentJets_identify line 14
  2. theorem OAI.DeGiorgi.all_jet_subsequence line 23
  3. def OAI.DeGiorgi.smallDefectEntry line 61
  4. def OAI.DeGiorgi.smallDefectScale line 68
  5. lemma OAI.DeGiorgi.smallDefectEntry_smooth line 75
  6. lemma OAI.DeGiorgi.smallDefectScale_pos line 83
  7. lemma OAI.DeGiorgi.defectRoot_ball_comparison line 91
  8. lemma OAI.DeGiorgi.inverseProfile_zero line 112
  9. lemma OAI.DeGiorgi.inverseProfile_local_bound line 115
  10. lemma OAI.DeGiorgi.smallDefect_normalized_local_bounds line 125
  11. theorem OAI.DeGiorgi.smallDefect_smooth_compactness line 171
  12. abbrev OAI.DeGiorgi.SmallDefectIndex line 195
  13. def OAI.DeGiorgi.normalizedSmallJet line 197
  14. def OAI.DeGiorgi.SmallDefectConverges line 201
  15. lemma OAI.DeGiorgi.SmallDefectConverges.at line 206
  16. lemma OAI.DeGiorgi.smallDefect_compactness line 212
  17. lemma OAI.DeGiorgi.smallDefect_root_tendsto line 226
  18. lemma OAI.DeGiorgi.SmallDefectConverges.tensor_vanishes line 236
  19. lemma OAI.DeGiorgi.fderiv_eq_zero_of_coordDeriv_eq_zero line 250
  20. lemma OAI.DeGiorgi.fderiv_eq_of_coordDeriv_eq line 256
  21. lemma OAI.DeGiorgi.coordDeriv_as_inner line 263
  22. theorem OAI.DeGiorgi.SmallDefectConverges.profile_limit line 268
  23. lemma OAI.DeGiorgi.normalized_defect_limit_positive line 310
  24. lemma OAI.DeGiorgi.SmallDefectConverges.at_U line 341
  25. lemma OAI.DeGiorgi.SmallDefectConverges.at_D line 348
  26. lemma OAI.DeGiorgi.SmallDefectConverges.at_T line 354