OAI/InformationTheory/BooleanNoise/KRegularity.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LeanBlast.CourtadeKumar.hasDerivAt_tangent_extension line 17
  2. theorem OAI.LeanBlast.CourtadeKumar.clamp_nonexpansive line 40
  3. theorem OAI.LeanBlast.CourtadeKumar.K_eq_zero_of_nonpos line 46
  4. theorem OAI.LeanBlast.CourtadeKumar.KDeriv_eq_clamp line 48
  5. theorem OAI.LeanBlast.CourtadeKumar.K_eq_rGap_nonneg line 57
  6. theorem OAI.LeanBlast.CourtadeKumar.clamp_mem_inverse_domain line 62
  7. theorem OAI.LeanBlast.CourtadeKumar.hasDerivAt_K_pos line 65
  8. theorem OAI.LeanBlast.CourtadeKumar.hasDerivAt_K_zero_of_right_derivative line 98
  9. theorem OAI.LeanBlast.CourtadeKumar.KDeriv_monotone_of_rDeriv line 114
  10. theorem OAI.LeanBlast.CourtadeKumar.KDeriv_lipschitz_of_rDeriv line 122
  11. theorem OAI.LeanBlast.CourtadeKumar.rDeriv_increment_le_of_continuous line 136
  12. theorem OAI.LeanBlast.CourtadeKumar.rDeriv_lipschitz_of_continuous_monotone line 152
  13. theorem OAI.LeanBlast.CourtadeKumar.K_le_rGap_of_convex line 168
  14. theorem OAI.LeanBlast.CourtadeKumar.K_nonneg_of_rGap_nonneg line 180
  15. theorem OAI.LeanBlast.CourtadeKumar.convexOn_K_of_shape line 194
  16. theorem OAI.LeanBlast.CourtadeKumar.hasDerivAt_K line 212
  17. theorem OAI.LeanBlast.CourtadeKumar.continuousOn_K line 218
  18. theorem OAI.LeanBlast.CourtadeKumar.monotone_KDeriv line 221
  19. theorem OAI.LeanBlast.CourtadeKumar.KDeriv_nonneg line 224
  20. theorem OAI.LeanBlast.CourtadeKumar.monotoneOn_K line 229
  21. theorem OAI.LeanBlast.CourtadeKumar.convexOn_K line 237
  22. theorem OAI.LeanBlast.CourtadeKumar.K_nonneg line 240
  23. theorem OAI.LeanBlast.CourtadeKumar.K_le_rGap line 244
  24. theorem OAI.LeanBlast.CourtadeKumar.KDeriv_lipschitz line 247