OAI/Probability/SKSupport/Parabolic/ForwardConstruction.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ZeroTemperatureSK.Heat.SmoothForward line 12
  2. lemma OAI.ZeroTemperatureSK.Heat.scoreRate_affine line 18
  3. theorem OAI.ZeroTemperatureSK.Heat.forwardScore_smooth line 27
  4. lemma OAI.ZeroTemperatureSK.Heat.SmoothForward.jet_spatial line 39
  5. lemma OAI.ZeroTemperatureSK.Heat.SmoothForward.jet_continuous line 43
  6. lemma OAI.ZeroTemperatureSK.Heat.SmoothForward.jet_family line 47
  7. lemma OAI.ZeroTemperatureSK.Heat.SmoothForward.rate_deriv line 50
  8. lemma OAI.ZeroTemperatureSK.Heat.SmoothForward.rate_jet2 line 59
  9. lemma OAI.ZeroTemperatureSK.Heat.SmoothForward.second_odd line 70
  10. lemma OAI.ZeroTemperatureSK.Heat.forwardScore_odd line 78
  11. theorem OAI.ZeroTemperatureSK.Parabolic.second_derivative_nonnegative_at_min line 97
  12. theorem OAI.ZeroTemperatureSK.Parabolic.time_derivative_nonpositive line 120
  13. theorem OAI.ZeroTemperatureSK.Parabolic.nonnegative_of_parabolic_inequality line 145
  14. theorem OAI.ZeroTemperatureSK.Parabolic.exponential_lower_barrier line 204