OAI/Probability/ClassicalON/SmoothProfiles.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ClassicalON.thetaBump line 11
  2. def OAI.ClassicalON.outerBump line 12
  3. def OAI.ClassicalON.innerBump line 13
  4. def OAI.ClassicalON.squareTheta line 15
  5. def OAI.ClassicalON.squareCutoff line 17
  6. def OAI.ClassicalON.squareGradient line 20
  7. def OAI.ClassicalON.squareProfile line 23
  8. theorem OAI.ClassicalON.thetaBump_one line 27
  9. theorem OAI.ClassicalON.thetaBump_zero line 31
  10. theorem OAI.ClassicalON.thetaBump_deriv_zero_inner line 35
  11. theorem OAI.ClassicalON.thetaBump_deriv_zero_outer line 42
  12. theorem OAI.ClassicalON.outerBump_one line 49
  13. theorem OAI.ClassicalON.outerBump_zero line 53
  14. theorem OAI.ClassicalON.innerBump_one line 57
  15. theorem OAI.ClassicalON.innerBump_zero line 61
  16. theorem OAI.ClassicalON.squareTheta_one line 65
  17. theorem OAI.ClassicalON.squareTheta_zero line 69
  18. theorem OAI.ClassicalON.squareCutoff_gradient line 75
  19. theorem OAI.ClassicalON.squareProfile_squares line 103
  20. theorem OAI.ClassicalON.squareProfile_zero_inner line 109
  21. theorem OAI.ClassicalON.squareProfile_zero_outer line 120
  22. theorem OAI.ClassicalON.squareTheta_contDiff line 136
  23. theorem OAI.ClassicalON.squareCutoff_contDiff line 139
  24. theorem OAI.ClassicalON.squareGradient_contDiff line 143
  25. theorem OAI.ClassicalON.squareProfile_contDiff line 149
  26. theorem OAI.ClassicalON.squareProfile_compact line 154