OAI/Computability/PerfectCompleteness/Foundations/SignedCostEnvelope.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.SignedCostEnvelope.payloadCoeff line 10
  2. def OAI.PerfectCompleteness.SignedCostEnvelope.streamCoeff line 13
  3. def OAI.PerfectCompleteness.SignedCostEnvelope.endpointBound line 15
  4. def OAI.PerfectCompleteness.SignedCostEnvelope.endpointCoeff line 21
  5. def OAI.PerfectCompleteness.SignedCostEnvelope.bodyBound line 25
  6. def OAI.PerfectCompleteness.SignedCostEnvelope.bodyCoeff line 29
  7. def OAI.PerfectCompleteness.SignedCostEnvelope.degree line 31
  8. theorem OAI.PerfectCompleteness.SignedCostEnvelope.le_scaled line 33
  9. theorem OAI.PerfectCompleteness.SignedCostEnvelope.one_le_envelope line 36
  10. theorem OAI.PerfectCompleteness.SignedCostEnvelope.input_le_envelope line 39
  11. theorem OAI.PerfectCompleteness.SignedCostEnvelope.streamPower_le_envelope line 42
  12. theorem OAI.PerfectCompleteness.SignedCostEnvelope.payloadBound_le line 46
  13. theorem OAI.PerfectCompleteness.SignedCostEnvelope.streamBound_le line 64
  14. theorem OAI.PerfectCompleteness.SignedCostEnvelope.endpointBound_le line 85
  15. theorem OAI.PerfectCompleteness.SignedCostEnvelope.bodyBound_le line 137