OAI/InformationTheory/BooleanNoise/Basic.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LeanBlast.CourtadeKumar.noiseKernel line 11
  2. def OAI.LeanBlast.CourtadeKumar.noiseOperator line 14
  3. abbrev OAI.LeanBlast.CourtadeKumar.flip line 17
  4. def OAI.LeanBlast.CourtadeKumar.cubeDerivative line 20
  5. def OAI.LeanBlast.CourtadeKumar.psi line 23
  6. def OAI.LeanBlast.CourtadeKumar.entropy line 26
  7. def OAI.LeanBlast.CourtadeKumar.entropyAverage line 28
  8. def OAI.LeanBlast.CourtadeKumar.informationDeficit line 31
  9. def OAI.LeanBlast.CourtadeKumar.meanVariance line 34
  10. def OAI.LeanBlast.CourtadeKumar.dissipation line 37
  11. def OAI.LeanBlast.CourtadeKumar.IsInterior line 40
  12. def OAI.LeanBlast.CourtadeKumar.IsSignValued line 43
  13. def OAI.LeanBlast.CourtadeKumar.IsIncreasing line 46
  14. def OAI.LeanBlast.CourtadeKumar.signEncoding line 49
  15. def OAI.LeanBlast.CourtadeKumar.restrict line 52
  16. def OAI.LeanBlast.CourtadeKumar.pairMean line 55
  17. def OAI.LeanBlast.CourtadeKumar.pairHalfDifference line 58
  18. def OAI.LeanBlast.CourtadeKumar.pairEntropyGap line 61
  19. def OAI.LeanBlast.CourtadeKumar.pairDissipation line 64