OAI/Analysis/AllenCahn/Resolvent.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DeGiorgi.boundedAbove_quadratic_maximum line 15
  2. lemma OAI.DeGiorgi.boundedAbove_maximum_principle line 36
  3. lemma OAI.DeGiorgi.boundedAbove_elliptic_comparison line 63
  4. lemma OAI.DeGiorgi.polynomial_profile_iteratedDeriv line 75
  5. lemma OAI.DeGiorgi.profile_temperate line 91
  6. lemma OAI.DeGiorgi.profileWeight_temperate line 102
  7. lemma OAI.DeGiorgi.profileWeight_le_one line 105
  8. def OAI.DeGiorgi.realResolvent line 109
  9. lemma OAI.DeGiorgi.realResolvent_equation line 112
  10. lemma OAI.DeGiorgi.schwartz_bounded line 116
  11. lemma OAI.DeGiorgi.realResolvent_nonneg line 120
  12. lemma OAI.DeGiorgi.realResolvent_bound line 133
  13. lemma OAI.DeGiorgi.realResolvent_mono line 167
  14. lemma OAI.DeGiorgi.realResolvent_comparison line 179
  15. lemma OAI.DeGiorgi.realResolvent_isometry line 190
  16. lemma OAI.DeGiorgi.schwartz_coordinateJet line 211
  17. lemma OAI.DeGiorgi.schwartz_jets_bounded line 222
  18. lemma OAI.DeGiorgi.JetControl.reindex line 227
  19. def OAI.DeGiorgi.resolventIterate line 235
  20. lemma OAI.DeGiorgi.resolventIterate_equation line 239
  21. lemma OAI.DeGiorgi.resolventIterate_nonneg line 246
  22. lemma OAI.DeGiorgi.resolventIterate_comparison line 258
  23. lemma OAI.DeGiorgi.resolventIterate_mono_source line 272
  24. lemma OAI.DeGiorgi.resolventIterate_mono_index line 284
  25. lemma OAI.DeGiorgi.resolventIterate_isometry line 299