OAI/InformationTheory/SoftChannel/Thinning.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SoftChannel204.thinningPolynomial line 11
  2. theorem OAI.SoftChannel204.thinningPolynomial_pos line 16
  3. theorem OAI.SoftChannel204.thinning_cutoff_bound line 49
  4. def OAI.SoftChannel204.clipKernel line 92
  5. theorem OAI.SoftChannel204.clipKernel_nonneg line 94
  6. theorem OAI.SoftChannel204.clipKernel_of_le line 97
  7. theorem OAI.SoftChannel204.clipKernel_eq line 100
  8. theorem OAI.SoftChannel204.clipKernel_min line 104
  9. theorem OAI.SoftChannel204.thinning_endpoint_algebra line 129
  10. theorem OAI.SoftChannel204.thinning_hard_bound line 174
  11. theorem OAI.SoftChannel204.thinning_derivative_product line 233
  12. theorem OAI.SoftChannel204.continuousAt_clipKernel line 320
  13. theorem OAI.SoftChannel204.intervalIntegrable_clipKernel line 326
  14. def OAI.SoftChannel204.clipPrimitive line 333
  15. theorem OAI.SoftChannel204.hasDerivAt_clipPrimitive line 335
  16. theorem OAI.SoftChannel204.thinning_interval_aux line 343
  17. theorem OAI.SoftChannel204.thinning_interval line 435