OAI/Combinatorics/HoneycombBridges/ExactLength.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Exact-length renewal coefficients and bridge probabilities.

  1. def OAI.HoneycombActual.irreducibleListLength line 14
  2. def OAI.HoneycombActual.irreducibleListWeight line 17
  3. def OAI.HoneycombActual.exactPieceMass line 20
  4. theorem OAI.HoneycombActual.discountedWeight_zero line 25
  5. theorem OAI.HoneycombActual.optionLength_irreducibleProduct_nat line 28
  6. theorem OAI.HoneycombActual.optionWeight_irreducibleProduct_zero line 32
  7. theorem OAI.HoneycombActual.lengthMass_eq_listMass line 36
  8. theorem OAI.HoneycombActual.lengthMass_eq_tsum_exactPieceMass line 56
  9. theorem OAI.HoneycombActual.exactPieceMass_zero_count line 64
  10. theorem OAI.HoneycombActual.exactLengthRenewalIdentity line 71
  11. theorem OAI.HoneycombActual.two_mul_pieceCount_le_length line 78
  12. theorem OAI.HoneycombActual.exactPieceMass_eq_zero_of_halfLength_lt line 88
  13. theorem OAI.HoneycombActual.exactLengthRenewalMass_pos_finite line 99
  14. theorem OAI.HoneycombActual.uniformLengthProbability_mem_unitInterval line 109
  15. theorem OAI.HoneycombActual.uniformLengthProbability_univ line 122