OAI/InformationTheory/SoftChannel/Main.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SoftChannel204.production_eq line 15
  2. lemma OAI.SoftChannel204.S_eq_L line 31
  3. lemma OAI.SoftChannel204.reserve_eq line 40
  4. lemma OAI.SoftChannel204.softJoint_eq line 46
  5. theorem OAI.SoftChannel204.softContraction line 59
  6. theorem OAI.SoftChannel204.softAttainment line 63
  7. theorem OAI.SoftChannel204.softInformationIdentity line 67
  8. theorem OAI.SoftChannel204.refinedBoolean line 72
  9. theorem OAI.SoftChannel204.booleanAttainment line 85
  10. theorem OAI.SoftChannel204.bitsConversion line 93
  11. theorem OAI.SoftChannel204.sharpProduction line 104
  12. theorem OAI.SoftChannel204.fullMain line 113

    Distinct definitions of this name: ComparatorChallenges/SoftChannel204.lean:114 (same statement text; different proof or body). Qualify references as OAI.SoftChannel204.fullMain@path.