OAI/Analysis/AllenCahn/SechSpectrum.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DeGiorgi.positive_sech_ode_spectral line 14
  2. lemma OAI.DeGiorgi.positive_sech_ode_endpoint line 61
  3. lemma OAI.DeGiorgi.wronskian_eq_initial line 103
  4. lemma OAI.DeGiorgi.ode_basis_expansion line 123
  5. lemma OAI.DeGiorgi.contDiff_tanh line 142
  6. lemma OAI.DeGiorgi.tanh_hasDerivAt line 147
  7. lemma OAI.DeGiorgi.sech_sq_tanh line 157
  8. def OAI.DeGiorgi.jost line 163
  9. lemma OAI.DeGiorgi.contDiff_jost line 165
  10. lemma OAI.DeGiorgi.jost_hasDerivAt line 168
  11. lemma OAI.DeGiorgi.jost_deriv line 176
  12. lemma OAI.DeGiorgi.sech_hasDerivAt' line 179
  13. lemma OAI.DeGiorgi.jost_hasDerivAt_twice line 187
  14. def OAI.DeGiorgi.jostReflected line 200
  15. lemma OAI.DeGiorgi.jost_neg_parameter line 202
  16. lemma OAI.DeGiorgi.jost_reflection line 205
  17. lemma OAI.DeGiorgi.contDiff_jostReflected line 209
  18. lemma OAI.DeGiorgi.jostReflected_deriv line 213
  19. lemma OAI.DeGiorgi.jost_ode line 217
  20. lemma OAI.DeGiorgi.jostReflected_ode line 220
  21. lemma OAI.DeGiorgi.jost_pos line 226
  22. lemma OAI.DeGiorgi.jostReflected_pos line 229
  23. lemma OAI.DeGiorgi.jost_at_zero line 232
  24. lemma OAI.DeGiorgi.jostReflected_at_zero line 234
  25. lemma OAI.DeGiorgi.jost_deriv_at_zero line 236
  26. lemma OAI.DeGiorgi.jostReflected_deriv_at_zero line 239
  27. lemma OAI.DeGiorgi.jost_scale line 242
  28. lemma OAI.DeGiorgi.jostReflected_scale line 248
  29. lemma OAI.DeGiorgi.positive_jost_combination_first_nonneg line 255
  30. lemma OAI.DeGiorgi.positive_sech_ode_classification line 283
  31. lemma OAI.DeGiorgi.laplacian_separated line 327
  32. def OAI.DeGiorgi.conePotential line 344
  33. lemma OAI.DeGiorgi.conePotential_smooth line 347
  34. lemma OAI.DeGiorgi.conePotential_bounds line 350