OAI/InformationTheory/BooleanNoise/FiniteDistribution.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LeanBlast.CourtadeKumar.signProbability line 14
  2. theorem OAI.LeanBlast.CourtadeKumar.sum_signProbability line 17
  3. theorem OAI.LeanBlast.CourtadeKumar.signProbability_signEncoding line 21
  4. theorem OAI.LeanBlast.CourtadeKumar.noiseOperator_signProbability line 25
  5. theorem OAI.LeanBlast.CourtadeKumar.cubeAverage_signProbability line 42
  6. theorem OAI.LeanBlast.CourtadeKumar.bitFlipKernel_eq_noiseKernel line 58
  7. theorem OAI.LeanBlast.CourtadeKumar.bitFlipKernel_nonneg line 65
  8. theorem OAI.LeanBlast.CourtadeKumar.jointProbability_eq_posterior line 70
  9. theorem OAI.LeanBlast.CourtadeKumar.functionMarginal_eq_signProbability line 87
  10. theorem OAI.LeanBlast.CourtadeKumar.observationMarginal_eq_uniform line 95
  11. theorem OAI.LeanBlast.CourtadeKumar.observationMarginal_pos line 101
  12. theorem OAI.LeanBlast.CourtadeKumar.conditionalProbability_eq_signProbability line 106
  13. theorem OAI.LeanBlast.CourtadeKumar.jointProbability_nonneg line 113
  14. theorem OAI.LeanBlast.CourtadeKumar.jointProbability_sum line 122