OAI/Analysis/AllenCahn/ResolventJets.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DeGiorgi.resolventIterate_all_jets line 14
  2. def OAI.DeGiorgi.radialCutoffBase line 91
  3. lemma OAI.DeGiorgi.radialCutoffBase_smooth line 93
  4. lemma OAI.DeGiorgi.radialCutoffBase_compact line 96
  5. lemma OAI.DeGiorgi.coordinateJet_comp_smul line 102
  6. def OAI.DeGiorgi.radialCutoffScale line 122
  7. def OAI.DeGiorgi.radialCutoff line 124
  8. lemma OAI.DeGiorgi.radialCutoffScale_pos line 127
  9. lemma OAI.DeGiorgi.radialCutoffScale_le_one line 130
  10. lemma OAI.DeGiorgi.radialCutoff_smooth line 134
  11. lemma OAI.DeGiorgi.radialCutoff_bounds line 138
  12. lemma OAI.DeGiorgi.radialCutoff_compact line 142
  13. lemma OAI.DeGiorgi.radialCutoff_mono line 153
  14. lemma OAI.DeGiorgi.radialCutoff_eventually_one line 163
  15. lemma OAI.DeGiorgi.radialCutoff_isometry line 175
  16. lemma OAI.DeGiorgi.radialCutoff_jets line 179
  17. def OAI.DeGiorgi.cutSource line 192
  18. lemma OAI.DeGiorgi.cutSource_apply line 195
  19. lemma OAI.DeGiorgi.cutSource_nonneg line 198
  20. lemma OAI.DeGiorgi.cutSource_le line 201
  21. lemma OAI.DeGiorgi.cutSource_mono line 204
  22. lemma OAI.DeGiorgi.cutSource_tendsto line 209
  23. lemma OAI.DeGiorgi.cutSource_isometry line 215
  24. lemma OAI.DeGiorgi.cutSource_jets line 220
  25. theorem OAI.DeGiorgi.even_source_exhaustion line 237
  26. lemma OAI.DeGiorgi.SmallDefectConverges.relative_D_jets line 326
  27. lemma OAI.DeGiorgi.SmallDefectConverges.relative_T_jets line 339
  28. lemma OAI.DeGiorgi.profile_comp_inner_coord line 360
  29. lemma OAI.DeGiorgi.weight_comp_inner_coord line 370