OAI/Probability/RadialTransition/RadialKernel.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RadialTransition.rawBumpProfile line 12
  2. def OAI.RadialTransition.rawBump line 14
  3. theorem OAI.RadialTransition.rawBumpProfile_nonneg line 16
  4. theorem OAI.RadialTransition.rawBumpProfile_le_one line 19
  5. theorem OAI.RadialTransition.rawBumpProfile_zero line 22
  6. theorem OAI.RadialTransition.continuous_rawBumpProfile line 26
  7. theorem OAI.RadialTransition.contDiff_rawBump line 29
  8. theorem OAI.RadialTransition.compactSupport_rawBump line 33
  9. def OAI.RadialTransition.bumpIntegral line 40
  10. theorem OAI.RadialTransition.bumpIntegral_pos line 42
  11. def OAI.RadialTransition.bumpProfile line 47
  12. def OAI.RadialTransition.bump line 49
  13. theorem OAI.RadialTransition.bumpProfile_nonneg line 51
  14. theorem OAI.RadialTransition.bumpProfile_bound line 54
  15. theorem OAI.RadialTransition.bumpProfile_zero line 59
  16. theorem OAI.RadialTransition.continuous_bumpProfile line 62
  17. theorem OAI.RadialTransition.contDiff_bump line 65
  18. theorem OAI.RadialTransition.compactSupport_bump line 67
  19. theorem OAI.RadialTransition.integral_bump line 74