OAI/Probability/SKValue/Evolution/HeatTransform.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKValue.heatDen line 11
  2. def OAI.SKValue.heatScale line 12
  3. def OAI.SKValue.heatTime line 13
  4. lemma OAI.SKValue.heatDen_pos line 15
  5. lemma OAI.SKValue.heatDen_of_nonneg line 17
  6. lemma OAI.SKValue.heatScale_mem line 19
  7. lemma OAI.SKValue.heatTime_pos line 23
  8. lemma OAI.SKValue.heatDen_continuous line 28
  9. lemma OAI.SKValue.heatScale_continuous line 29
  10. lemma OAI.SKValue.heatTime_continuous line 31
  11. lemma OAI.SKValue.heatDen_hasDerivAt line 33
  12. lemma OAI.SKValue.heatScale_hasDerivAt line 37
  13. lemma OAI.SKValue.heatTime_hasDerivAt line 41
  14. lemma OAI.SKValue.scaledHeatJet_moving line 47
  15. def OAI.SKValue.forwardJet line 68
  16. lemma OAI.SKValue.forwardJet_zero line 71
  17. lemma OAI.SKValue.forwardJet_one line 74
  18. lemma OAI.SKValue.forwardJet_succ_succ line 77
  19. lemma OAI.SKValue.forwardJet_continuous line 80
  20. lemma OAI.SKValue.forwardJet_space line 88
  21. lemma OAI.SKValue.abs_sub_upper line 113
  22. lemma OAI.SKValue.heatDen_inv_hasDerivAt line 115
  23. lemma OAI.SKValue.forwardJet_time0 line 121
  24. lemma OAI.SKValue.forwardJet_time1 line 145
  25. lemma OAI.SKValue.forwardJet_time2 line 165
  26. lemma OAI.SKValue.heatDen_inv_bound line 190
  27. lemma OAI.SKValue.forwardJet_bound line 195
  28. lemma OAI.SKValue.forwardJet_growth line 215
  29. def OAI.SKValue.SmoothTerminal.forwardBurgers line 235