OAI/Analysis/AllenCahn/StrongMaximum.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PositiveMaximum.Space line 12
  2. lemma OAI.PositiveMaximum.second_deriv_nonneg_of_local_min line 25
  3. def OAI.PositiveMaximum.basis line 38
  4. def OAI.PositiveMaximum.coordDeriv line 40
  5. lemma OAI.PositiveMaximum.coordDeriv_contDiff line 43
  6. lemma OAI.PositiveMaximum.laplacian_eq_sum_coordDeriv line 47
  7. lemma OAI.PositiveMaximum.deriv_line line 59
  8. lemma OAI.PositiveMaximum.laplacian_nonneg_of_local_min line 66
  9. lemma OAI.PositiveMaximum.compact_minimum_principle line 89
  10. def OAI.PositiveMaximum.gaussian line 107
  11. lemma OAI.PositiveMaximum.gaussian_contDiff line 110
  12. lemma OAI.PositiveMaximum.fderiv_gaussian line 115
  13. lemma OAI.PositiveMaximum.second_coord_gaussian line 123
  14. lemma OAI.PositiveMaximum.laplacian_gaussian line 149
  15. def OAI.PositiveMaximum.barrier line 159
  16. lemma OAI.PositiveMaximum.barrier_contDiff line 162
  17. lemma OAI.PositiveMaximum.laplacian_barrier line 165
  18. lemma OAI.PositiveMaximum.barrier_le_one line 173
  19. lemma OAI.PositiveMaximum.barrier_subsolution line 182
  20. lemma OAI.PositiveMaximum.laplacian_sub_const_mul line 199
  21. lemma OAI.PositiveMaximum.annulus_comparison line 209
  22. lemma OAI.PositiveMaximum.fderiv_barrier line 256
  23. lemma OAI.PositiveMaximum.nonneg_right_derivative line 264
  24. lemma OAI.PositiveMaximum.no_tangent_zero line 271
  25. lemma OAI.PositiveMaximum.nonnegative_supersolution_eq_zero line 338