OAI/Analysis/HenonEmden/Cutoff.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HenonLaneEmden.Cutoff.posPow line 14

    Source documentation

    The positive-part powers used by the compact cutoff.

    def posPow (k : ℕ) (r : ℝ) : ℝ := (max r 0)^k

    Mentions: OAI.HenonLaneEmden.Cutoff.k

  2. lemma OAI.HenonLaneEmden.Cutoff.continuous_posPow line 15
  3. lemma OAI.HenonLaneEmden.Cutoff.hasDerivAt_posPow line 16
  4. def OAI.HenonLaneEmden.Cutoff.m line 42
  5. def OAI.HenonLaneEmden.Cutoff.k line 43
  6. def OAI.HenonLaneEmden.Cutoff.N line 44
  7. lemma OAI.HenonLaneEmden.Cutoff.N_ge_two line 45
  8. lemma OAI.HenonLaneEmden.Cutoff.N_ge_three line 46
  9. def OAI.HenonLaneEmden.Cutoff.gapProfile line 48
  10. def OAI.HenonLaneEmden.Cutoff.baseProfile line 49
  11. def OAI.HenonLaneEmden.Cutoff.etaProfile line 50
  12. def OAI.HenonLaneEmden.Cutoff.derivativeProfile line 51
  13. def OAI.HenonLaneEmden.Cutoff.wProfile line 53
  14. lemma OAI.HenonLaneEmden.Cutoff.continuous_gapProfile line 55
  15. lemma OAI.HenonLaneEmden.Cutoff.continuous_baseProfile line 56
  16. lemma OAI.HenonLaneEmden.Cutoff.continuous_etaProfile line 57
  17. lemma OAI.HenonLaneEmden.Cutoff.continuous_derivativeProfile line 59
  18. lemma OAI.HenonLaneEmden.Cutoff.continuous_wProfile line 61
  19. lemma OAI.HenonLaneEmden.Cutoff.hasDerivAt_etaProfile line 64
  20. lemma OAI.HenonLaneEmden.Cutoff.gapProfile_nonneg line 73
  21. lemma OAI.HenonLaneEmden.Cutoff.gapProfile_le_one line 75
  22. lemma OAI.HenonLaneEmden.Cutoff.baseProfile_nonneg line 76
  23. lemma OAI.HenonLaneEmden.Cutoff.baseProfile_le_one line 77
  24. lemma OAI.HenonLaneEmden.Cutoff.gapProfile_inner line 81
  25. lemma OAI.HenonLaneEmden.Cutoff.baseProfile_inner line 85
  26. lemma OAI.HenonLaneEmden.Cutoff.gapProfile_outer line 87
  27. lemma OAI.HenonLaneEmden.Cutoff.baseProfile_outer line 89
  28. lemma OAI.HenonLaneEmden.Cutoff.gapProfile_middle line 92
  29. lemma OAI.HenonLaneEmden.Cutoff.baseProfile_middle line 95
  30. lemma OAI.HenonLaneEmden.Cutoff.base_gap_bounds line 101
  31. lemma OAI.HenonLaneEmden.Cutoff.etaProfile_eq_power line 113
  32. lemma OAI.HenonLaneEmden.Cutoff.etaProfile_bounds line 114
  33. lemma OAI.HenonLaneEmden.Cutoff.derivativeProfile_inner line 119
  34. lemma OAI.HenonLaneEmden.Cutoff.derivativeProfile_outer line 121
  35. lemma OAI.HenonLaneEmden.Cutoff.derivativeProfile_nonpos line 123
  36. lemma OAI.HenonLaneEmden.Cutoff.wProfile_nonneg line 127
  37. lemma OAI.HenonLaneEmden.Cutoff.derivativeProfile_bound line 129
  38. lemma OAI.HenonLaneEmden.Cutoff.wProfile_bound line 146
  39. lemma OAI.HenonLaneEmden.Cutoff.gap_wProfile_bound line 158
  40. def OAI.HenonLaneEmden.Cutoff.secondProfile line 183
  41. lemma OAI.HenonLaneEmden.Cutoff.continuous_secondProfile line 187
  42. lemma OAI.HenonLaneEmden.Cutoff.hasDerivAt_derivativeProfile line 190
  43. lemma OAI.HenonLaneEmden.Cutoff.secondProfile_inner line 207
  44. lemma OAI.HenonLaneEmden.Cutoff.secondProfile_outer line 209
  45. lemma OAI.HenonLaneEmden.Cutoff.secondProfile_bound line 215
  46. lemma OAI.HenonLaneEmden.Cutoff.lipschitz_gapProfile line 251
  47. lemma OAI.HenonLaneEmden.Cutoff.gapProfile_oscillation line 259
  48. def OAI.HenonLaneEmden.Cutoff.derivativeConstant line 262
  49. def OAI.HenonLaneEmden.Cutoff.secondConstant line 263
  50. def OAI.HenonLaneEmden.Cutoff.wDerivativeConstant line 264
  51. def OAI.HenonLaneEmden.Cutoff.wDerivativeProfile line 266
  52. lemma OAI.HenonLaneEmden.Cutoff.hasDerivAt_wProfile line 268
  53. lemma OAI.HenonLaneEmden.Cutoff.constants_nonneg line 273
  54. lemma OAI.HenonLaneEmden.Cutoff.wDerivativeProfile_bound line 282
  55. lemma OAI.HenonLaneEmden.Cutoff.wProfile_oscillation line 303
  56. def OAI.HenonLaneEmden.Cutoff.d line 318
  57. def OAI.HenonLaneEmden.Cutoff.eta line 319
  58. def OAI.HenonLaneEmden.Cutoff.w line 320
  59. def OAI.HenonLaneEmden.Cutoff.X line 321
  60. lemma OAI.HenonLaneEmden.Cutoff.continuous_d line 324
  61. lemma OAI.HenonLaneEmden.Cutoff.continuous_eta line 326
  62. lemma OAI.HenonLaneEmden.Cutoff.eta_eq_one line 329
  63. lemma OAI.HenonLaneEmden.Cutoff.eta_eq_zero line 332
  64. lemma OAI.HenonLaneEmden.Cutoff.hasFDerivAt_eta line 338
  65. lemma OAI.HenonLaneEmden.Cutoff.w_eq_profile line 348
  66. lemma OAI.HenonLaneEmden.Cutoff.continuous_w line 356