OAI/InformationTheory/BooleanNoise/InverseScalars.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LeanBlast.CourtadeKumar.psiInv line 16
  2. def OAI.LeanBlast.CourtadeKumar.r line 18
  3. def OAI.LeanBlast.CourtadeKumar.rDeriv line 20
  4. def OAI.LeanBlast.CourtadeKumar.rSecondDeriv line 24
  5. def OAI.LeanBlast.CourtadeKumar.rGap line 29
  6. def OAI.LeanBlast.CourtadeKumar.L line 31
  7. def OAI.LeanBlast.CourtadeKumar.LDeriv line 34
  8. def OAI.LeanBlast.CourtadeKumar.s0 line 37
  9. def OAI.LeanBlast.CourtadeKumar.K line 39
  10. def OAI.LeanBlast.CourtadeKumar.KDeriv line 43
  11. theorem OAI.LeanBlast.CourtadeKumar.psiInv_mem_of_mem_image line 47
  12. theorem OAI.LeanBlast.CourtadeKumar.psi_psiInv_of_mem_image line 51
  13. theorem OAI.LeanBlast.CourtadeKumar.rDeriv_zero line 55
  14. theorem OAI.LeanBlast.CourtadeKumar.rSecondDeriv_zero line 56
  15. theorem OAI.LeanBlast.CourtadeKumar.K_zero line 57
  16. theorem OAI.LeanBlast.CourtadeKumar.KDeriv_zero line 58
  17. theorem OAI.LeanBlast.CourtadeKumar.L_eq_zero_of_ell_le line 60
  18. theorem OAI.LeanBlast.CourtadeKumar.L_eq_rGap line 63
  19. theorem OAI.LeanBlast.CourtadeKumar.K_eq_rGap line 66
  20. theorem OAI.LeanBlast.CourtadeKumar.K_eq_tangent line 69
  21. theorem OAI.LeanBlast.CourtadeKumar.image_psi_Icc line 75
  22. theorem OAI.LeanBlast.CourtadeKumar.psiInv_mem_Icc line 80
  23. theorem OAI.LeanBlast.CourtadeKumar.psi_psiInv_Icc line 83
  24. theorem OAI.LeanBlast.CourtadeKumar.psiInv_psi line 86
  25. theorem OAI.LeanBlast.CourtadeKumar.psiInv_zero line 89
  26. theorem OAI.LeanBlast.CourtadeKumar.psiInv_ell line 92
  27. theorem OAI.LeanBlast.CourtadeKumar.r_zero line 95
  28. theorem OAI.LeanBlast.CourtadeKumar.rGap_zero line 96
  29. theorem OAI.LeanBlast.CourtadeKumar.psi_psiInv line 98
  30. theorem OAI.LeanBlast.CourtadeKumar.psiInv_mem_Ico line 101
  31. theorem OAI.LeanBlast.CourtadeKumar.psiInv_mem_Ioo line 111
  32. def OAI.LeanBlast.CourtadeKumar.psiOrderIso line 120
  33. theorem OAI.LeanBlast.CourtadeKumar.continuousOn_psiInv line 129
  34. theorem OAI.LeanBlast.CourtadeKumar.continuousAt_psiInv line 133
  35. theorem OAI.LeanBlast.CourtadeKumar.r_psi_nonneg line 136
  36. theorem OAI.LeanBlast.CourtadeKumar.r_psi line 139
  37. theorem OAI.LeanBlast.CourtadeKumar.s0_pos line 153
  38. theorem OAI.LeanBlast.CourtadeKumar.s0_lt_ell line 158
  39. theorem OAI.LeanBlast.CourtadeKumar.hasDerivAt_psiInv line 160
  40. theorem OAI.LeanBlast.CourtadeKumar.continuousOn_r line 168
  41. theorem OAI.LeanBlast.CourtadeKumar.hasDerivAt_r line 177