OAI/InformationTheory/BooleanNoise/InverseRegularity.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LeanBlast.CourtadeKumar.psi_pos_of_pos line 14
  2. theorem OAI.LeanBlast.CourtadeKumar.rDeriv_psi line 18
  3. theorem OAI.LeanBlast.CourtadeKumar.rSecondDeriv_psi line 23
  4. theorem OAI.LeanBlast.CourtadeKumar.hasDerivAt_rDerivativeFormula line 29
  5. theorem OAI.LeanBlast.CourtadeKumar.hasDerivAt_rDeriv line 43
  6. theorem OAI.LeanBlast.CourtadeKumar.continuousOn_rGap line 57
  7. theorem OAI.LeanBlast.CourtadeKumar.hasDerivAt_rGap line 60
  8. theorem OAI.LeanBlast.CourtadeKumar.L_ell_sub line 65
  9. theorem OAI.LeanBlast.CourtadeKumar.L_entropy line 72
  10. theorem OAI.LeanBlast.CourtadeKumar.LDeriv_entropy line 76
  11. theorem OAI.LeanBlast.CourtadeKumar.hasDerivAt_L_of_lt line 84
  12. theorem OAI.LeanBlast.CourtadeKumar.hasDerivAt_LDeriv_of_lt line 95
  13. theorem OAI.LeanBlast.CourtadeKumar.rDeriv_ge_two line 105
  14. theorem OAI.LeanBlast.CourtadeKumar.rSecondDeriv_pos line 118
  15. theorem OAI.LeanBlast.CourtadeKumar.rSecondDeriv_nonneg line 129
  16. theorem OAI.LeanBlast.CourtadeKumar.convexOn_r line 135
  17. theorem OAI.LeanBlast.CourtadeKumar.convexOn_rGap line 145
  18. theorem OAI.LeanBlast.CourtadeKumar.monotoneOn_rGap line 157
  19. theorem OAI.LeanBlast.CourtadeKumar.rGap_nonneg line 166
  20. theorem OAI.LeanBlast.CourtadeKumar.monotoneOn_rDeriv line 169
  21. theorem OAI.LeanBlast.CourtadeKumar.tendsto_psiInv_zero_right line 183
  22. theorem OAI.LeanBlast.CourtadeKumar.tendsto_rDeriv_zero_right line 191
  23. theorem OAI.LeanBlast.CourtadeKumar.tendsto_rSecondDeriv_zero_right line 196
  24. theorem OAI.LeanBlast.CourtadeKumar.continuousOn_rDeriv line 201
  25. theorem OAI.LeanBlast.CourtadeKumar.tendsto_r_div_zero_right line 213
  26. theorem OAI.LeanBlast.CourtadeKumar.hasDerivWithinAt_r_zero line 219
  27. theorem OAI.LeanBlast.CourtadeKumar.hasDerivWithinAt_rGap_zero line 227
  28. theorem OAI.LeanBlast.CourtadeKumar.monotoneOn_r line 232
  29. theorem OAI.LeanBlast.CourtadeKumar.hasDerivWithinAt_rDeriv_zero line 238